Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dia2dimlem1 Structured version   Visualization version   GIF version

Theorem dia2dimlem1 36874
Description: Lemma for dia2dim 36887. Show properties of the auxiliary atom 𝑄. Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem1.l = (le‘𝐾)
dia2dimlem1.j = (join‘𝐾)
dia2dimlem1.m = (meet‘𝐾)
dia2dimlem1.a 𝐴 = (Atoms‘𝐾)
dia2dimlem1.h 𝐻 = (LHyp‘𝐾)
dia2dimlem1.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dia2dimlem1.r 𝑅 = ((trL‘𝐾)‘𝑊)
dia2dimlem1.q 𝑄 = ((𝑃 𝑈) ((𝐹𝑃) 𝑉))
dia2dimlem1.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
dia2dimlem1.u (𝜑 → (𝑈𝐴𝑈 𝑊))
dia2dimlem1.v (𝜑 → (𝑉𝐴𝑉 𝑊))
dia2dimlem1.p (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
dia2dimlem1.f (𝜑 → (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃))
dia2dimlem1.rf (𝜑 → (𝑅𝐹) (𝑈 𝑉))
dia2dimlem1.uv (𝜑𝑈𝑉)
dia2dimlem1.ru (𝜑 → (𝑅𝐹) ≠ 𝑈)
Assertion
Ref Expression
dia2dimlem1 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))

Proof of Theorem dia2dimlem1
StepHypRef Expression
1 dia2dimlem1.q . . 3 𝑄 = ((𝑃 𝑈) ((𝐹𝑃) 𝑉))
2 dia2dimlem1.k . . . . 5 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
32simpld 482 . . . 4 (𝜑𝐾 ∈ HL)
4 dia2dimlem1.p . . . . 5 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
54simpld 482 . . . 4 (𝜑𝑃𝐴)
6 dia2dimlem1.f . . . . 5 (𝜑 → (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃))
7 dia2dimlem1.l . . . . . 6 = (le‘𝐾)
8 dia2dimlem1.a . . . . . 6 𝐴 = (Atoms‘𝐾)
9 dia2dimlem1.h . . . . . 6 𝐻 = (LHyp‘𝐾)
10 dia2dimlem1.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
11 dia2dimlem1.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
127, 8, 9, 10, 11trlat 35979 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
132, 4, 6, 12syl3anc 1476 . . . 4 (𝜑 → (𝑅𝐹) ∈ 𝐴)
14 dia2dimlem1.u . . . . 5 (𝜑 → (𝑈𝐴𝑈 𝑊))
1514simpld 482 . . . 4 (𝜑𝑈𝐴)
166simpld 482 . . . . . 6 (𝜑𝐹𝑇)
177, 8, 9, 10ltrnel 35948 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
182, 16, 4, 17syl3anc 1476 . . . . 5 (𝜑 → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
1918simpld 482 . . . 4 (𝜑 → (𝐹𝑃) ∈ 𝐴)
20 dia2dimlem1.v . . . . 5 (𝜑 → (𝑉𝐴𝑉 𝑊))
2120simpld 482 . . . 4 (𝜑𝑉𝐴)
224simprd 483 . . . . . 6 (𝜑 → ¬ 𝑃 𝑊)
237, 9, 10, 11trlle 35994 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) 𝑊)
242, 16, 23syl2anc 573 . . . . . . . 8 (𝜑 → (𝑅𝐹) 𝑊)
2514simprd 483 . . . . . . . 8 (𝜑𝑈 𝑊)
263hllatd 35173 . . . . . . . . 9 (𝜑𝐾 ∈ Lat)
27 eqid 2771 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
2827, 8atbase 35098 . . . . . . . . . 10 ((𝑅𝐹) ∈ 𝐴 → (𝑅𝐹) ∈ (Base‘𝐾))
2913, 28syl 17 . . . . . . . . 9 (𝜑 → (𝑅𝐹) ∈ (Base‘𝐾))
3027, 8atbase 35098 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
3115, 30syl 17 . . . . . . . . 9 (𝜑𝑈 ∈ (Base‘𝐾))
322simprd 483 . . . . . . . . . 10 (𝜑𝑊𝐻)
3327, 9lhpbase 35807 . . . . . . . . . 10 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3432, 33syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ (Base‘𝐾))
35 dia2dimlem1.j . . . . . . . . . 10 = (join‘𝐾)
3627, 7, 35latjle12 17270 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑅𝐹) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3726, 29, 31, 34, 36syl13anc 1478 . . . . . . . 8 (𝜑 → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3824, 25, 37mpbi2and 691 . . . . . . 7 (𝜑 → ((𝑅𝐹) 𝑈) 𝑊)
3927, 8atbase 35098 . . . . . . . . 9 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
405, 39syl 17 . . . . . . . 8 (𝜑𝑃 ∈ (Base‘𝐾))
4127, 35, 8hlatjcl 35176 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑅𝐹) ∈ 𝐴𝑈𝐴) → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
423, 13, 15, 41syl3anc 1476 . . . . . . . 8 (𝜑 → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
4327, 7lattr 17264 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4426, 40, 42, 34, 43syl13anc 1478 . . . . . . 7 (𝜑 → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4538, 44mpan2d 674 . . . . . 6 (𝜑 → (𝑃 ((𝑅𝐹) 𝑈) → 𝑃 𝑊))
4622, 45mtod 189 . . . . 5 (𝜑 → ¬ 𝑃 ((𝑅𝐹) 𝑈))
4720simprd 483 . . . . . . 7 (𝜑𝑉 𝑊)
4818simprd 483 . . . . . . 7 (𝜑 → ¬ (𝐹𝑃) 𝑊)
49 nbrne2 4807 . . . . . . 7 ((𝑉 𝑊 ∧ ¬ (𝐹𝑃) 𝑊) → 𝑉 ≠ (𝐹𝑃))
5047, 48, 49syl2anc 573 . . . . . 6 (𝜑𝑉 ≠ (𝐹𝑃))
5150necomd 2998 . . . . 5 (𝜑 → (𝐹𝑃) ≠ 𝑉)
5246, 51jca 501 . . . 4 (𝜑 → (¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉))
5326adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝐾 ∈ Lat)
5440adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
5527, 35, 8hlatjcl 35176 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑉𝐴𝑈𝐴) → (𝑉 𝑈) ∈ (Base‘𝐾))
563, 21, 15, 55syl3anc 1476 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) ∈ (Base‘𝐾))
5756adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) ∈ (Base‘𝐾))
5834adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑊 ∈ (Base‘𝐾))
597, 35, 8hlatlej2 35185 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → 𝑉 ((𝐹𝑃) 𝑉))
603, 19, 21, 59syl3anc 1476 . . . . . . . . . . 11 (𝜑𝑉 ((𝐹𝑃) 𝑉))
6160adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 ((𝐹𝑃) 𝑉))
62 simpr 471 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑃 𝑈) = ((𝐹𝑃) 𝑉))
6361, 62breqtrrd 4815 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 (𝑃 𝑈))
64 dia2dimlem1.uv . . . . . . . . . . . 12 (𝜑𝑈𝑉)
6564necomd 2998 . . . . . . . . . . 11 (𝜑𝑉𝑈)
667, 35, 8hlatexch2 35205 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴𝑃𝐴𝑈𝐴) ∧ 𝑉𝑈) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
673, 21, 5, 15, 65, 66syl131anc 1489 . . . . . . . . . 10 (𝜑 → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6867adantr 466 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6963, 68mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 (𝑉 𝑈))
7027, 8atbase 35098 . . . . . . . . . . . 12 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
7121, 70syl 17 . . . . . . . . . . 11 (𝜑𝑉 ∈ (Base‘𝐾))
7227, 7, 35latjle12 17270 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7326, 71, 31, 34, 72syl13anc 1478 . . . . . . . . . 10 (𝜑 → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7447, 25, 73mpbi2and 691 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) 𝑊)
7574adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) 𝑊)
7627, 7, 53, 54, 57, 58, 69, 75lattrd 17266 . . . . . . 7 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 𝑊)
7776ex 397 . . . . . 6 (𝜑 → ((𝑃 𝑈) = ((𝐹𝑃) 𝑉) → 𝑃 𝑊))
7877necon3bd 2957 . . . . 5 (𝜑 → (¬ 𝑃 𝑊 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉)))
7922, 78mpd 15 . . . 4 (𝜑 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉))
807, 35, 8hlatlej2 35185 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝐹𝑃) (𝑃 (𝐹𝑃)))
813, 5, 19, 80syl3anc 1476 . . . . . 6 (𝜑 → (𝐹𝑃) (𝑃 (𝐹𝑃)))
82 dia2dimlem1.m . . . . . . . . . 10 = (meet‘𝐾)
837, 35, 82, 8, 9, 10, 11trlval2 35973 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
842, 16, 4, 83syl3anc 1476 . . . . . . . 8 (𝜑 → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
8584oveq2d 6812 . . . . . . 7 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)))
8627, 35, 8hlatjcl 35176 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
873, 5, 19, 86syl3anc 1476 . . . . . . . . 9 (𝜑 → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
887, 35, 8hlatlej1 35184 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → 𝑃 (𝑃 (𝐹𝑃)))
893, 5, 19, 88syl3anc 1476 . . . . . . . . 9 (𝜑𝑃 (𝑃 (𝐹𝑃)))
9027, 7, 35, 82, 8atmod3i1 35673 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 (𝐹𝑃))) → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
913, 5, 87, 34, 89, 90syl131anc 1489 . . . . . . . 8 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
92 eqid 2771 . . . . . . . . . . . 12 (1.‘𝐾) = (1.‘𝐾)
937, 35, 92, 8, 9lhpjat2 35830 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
942, 4, 93syl2anc 573 . . . . . . . . . 10 (𝜑 → (𝑃 𝑊) = (1.‘𝐾))
9594oveq2d 6812 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = ((𝑃 (𝐹𝑃)) (1.‘𝐾)))
96 hlol 35170 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
973, 96syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ OL)
9827, 82, 92olm11 35036 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
9997, 87, 98syl2anc 573 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
10095, 99eqtrd 2805 . . . . . . . 8 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = (𝑃 (𝐹𝑃)))
10191, 100eqtrd 2805 . . . . . . 7 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = (𝑃 (𝐹𝑃)))
10285, 101eqtrd 2805 . . . . . 6 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 (𝐹𝑃)))
10381, 102breqtrrd 4815 . . . . 5 (𝜑 → (𝐹𝑃) (𝑃 (𝑅𝐹)))
104 dia2dimlem1.rf . . . . . . 7 (𝜑 → (𝑅𝐹) (𝑈 𝑉))
10535, 8hlatjcom 35177 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) = (𝑉 𝑈))
1063, 15, 21, 105syl3anc 1476 . . . . . . 7 (𝜑 → (𝑈 𝑉) = (𝑉 𝑈))
107104, 106breqtrd 4813 . . . . . 6 (𝜑 → (𝑅𝐹) (𝑉 𝑈))
108 dia2dimlem1.ru . . . . . . 7 (𝜑 → (𝑅𝐹) ≠ 𝑈)
1097, 35, 8hlatexch2 35205 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑉𝐴𝑈𝐴) ∧ (𝑅𝐹) ≠ 𝑈) → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
1103, 13, 21, 15, 108, 109syl131anc 1489 . . . . . 6 (𝜑 → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
111107, 110mpd 15 . . . . 5 (𝜑𝑉 ((𝑅𝐹) 𝑈))
112103, 111jca 501 . . . 4 (𝜑 → ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))
1137, 35, 82, 8ps-2c 35337 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝐹) ∈ 𝐴) ∧ (𝑈𝐴 ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) ∧ ((¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉) ∧ (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉) ∧ ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1143, 5, 13, 15, 19, 21, 52, 79, 112, 113syl333anc 1508 . . 3 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1151, 114syl5eqel 2854 . 2 (𝜑𝑄𝐴)
11627, 35, 8hlatjcl 35176 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
1173, 5, 15, 116syl3anc 1476 . . . . . . . . . . . 12 (𝜑 → (𝑃 𝑈) ∈ (Base‘𝐾))
11827, 35, 8hlatjcl 35176 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
1193, 19, 21, 118syl3anc 1476 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
12027, 7, 82latmle1 17284 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
12126, 117, 119, 120syl3anc 1476 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
1221, 121syl5eqbr 4822 . . . . . . . . . 10 (𝜑𝑄 (𝑃 𝑈))
12327, 8atbase 35098 . . . . . . . . . . . . 13 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
124115, 123syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (Base‘𝐾))
12527, 7, 82latlem12 17286 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
12626, 124, 117, 34, 125syl13anc 1478 . . . . . . . . . . 11 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
127126biimpd 219 . . . . . . . . . 10 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊)))
128122, 127mpand 675 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 ((𝑃 𝑈) 𝑊)))
129128imp 393 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊))
130 eqid 2771 . . . . . . . . . . . . 13 (0.‘𝐾) = (0.‘𝐾)
1317, 82, 130, 8, 9lhpmat 35839 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (0.‘𝐾))
1322, 4, 131syl2anc 573 . . . . . . . . . . 11 (𝜑 → (𝑃 𝑊) = (0.‘𝐾))
133132oveq1d 6811 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((0.‘𝐾) 𝑈))
13427, 7, 35, 82, 8atmod4i1 35675 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 𝑊) → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
1353, 15, 40, 34, 25, 134syl131anc 1489 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
13627, 35, 130olj02 35035 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑈 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑈) = 𝑈)
13797, 31, 136syl2anc 573 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑈) = 𝑈)
138133, 135, 1373eqtr3d 2813 . . . . . . . . 9 (𝜑 → ((𝑃 𝑈) 𝑊) = 𝑈)
139138adantr 466 . . . . . . . 8 ((𝜑𝑄 𝑊) → ((𝑃 𝑈) 𝑊) = 𝑈)
140129, 139breqtrd 4813 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑈)
141 hlatl 35169 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
1423, 141syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ AtLat)
143142adantr 466 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝐾 ∈ AtLat)
144115adantr 466 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄𝐴)
14515adantr 466 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑈𝐴)
1467, 8atcmp 35120 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑈𝐴) → (𝑄 𝑈𝑄 = 𝑈))
147143, 144, 145, 146syl3anc 1476 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑈𝑄 = 𝑈))
148140, 147mpbid 222 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑈)
14927, 7, 82latmle2 17285 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
15026, 117, 119, 149syl3anc 1476 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
1511, 150syl5eqbr 4822 . . . . . . . . . 10 (𝜑𝑄 ((𝐹𝑃) 𝑉))
15227, 7, 82latlem12 17286 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
15326, 124, 119, 34, 152syl13anc 1478 . . . . . . . . . . 11 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
154153biimpd 219 . . . . . . . . . 10 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
155151, 154mpand 675 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
156155imp 393 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊))
1577, 82, 130, 8, 9lhpmat 35839 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊)) → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
1582, 18, 157syl2anc 573 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
159158oveq1d 6811 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = ((0.‘𝐾) 𝑉))
16027, 8atbase 35098 . . . . . . . . . . . 12 ((𝐹𝑃) ∈ 𝐴 → (𝐹𝑃) ∈ (Base‘𝐾))
16119, 160syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) ∈ (Base‘𝐾))
16227, 7, 35, 82, 8atmod4i1 35675 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴 ∧ (𝐹𝑃) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 𝑊) → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
1633, 21, 161, 34, 47, 162syl131anc 1489 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
16427, 35, 130olj02 35035 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑉 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑉) = 𝑉)
16597, 71, 164syl2anc 573 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑉) = 𝑉)
166159, 163, 1653eqtr3d 2813 . . . . . . . . 9 (𝜑 → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
167166adantr 466 . . . . . . . 8 ((𝜑𝑄 𝑊) → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
168156, 167breqtrd 4813 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑉)
16921adantr 466 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑉𝐴)
1707, 8atcmp 35120 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑉𝐴) → (𝑄 𝑉𝑄 = 𝑉))
171143, 144, 169, 170syl3anc 1476 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑉𝑄 = 𝑉))
172168, 171mpbid 222 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑉)
173148, 172eqtr3d 2807 . . . . 5 ((𝜑𝑄 𝑊) → 𝑈 = 𝑉)
174173ex 397 . . . 4 (𝜑 → (𝑄 𝑊𝑈 = 𝑉))
175174necon3ad 2956 . . 3 (𝜑 → (𝑈𝑉 → ¬ 𝑄 𝑊))
17664, 175mpd 15 . 2 (𝜑 → ¬ 𝑄 𝑊)
177115, 176jca 501 1 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943   class class class wbr 4787  cfv 6030  (class class class)co 6796  Basecbs 16064  lecple 16156  joincjn 17152  meetcmee 17153  0.cp0 17245  1.cp1 17246  Latclat 17253  OLcol 34983  Atomscatm 35072  AtLatcal 35073  HLchlt 35159  LHypclh 35793  LTrncltrn 35910  trLctrl 35968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7100
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6757  df-ov 6799  df-oprab 6800  df-mpt2 6801  df-1st 7319  df-2nd 7320  df-map 8015  df-preset 17136  df-poset 17154  df-plt 17166  df-lub 17182  df-glb 17183  df-join 17184  df-meet 17185  df-p0 17247  df-p1 17248  df-lat 17254  df-clat 17316  df-oposet 34985  df-ol 34987  df-oml 34988  df-covers 35075  df-ats 35076  df-atl 35107  df-cvlat 35131  df-hlat 35160  df-llines 35307  df-psubsp 35312  df-pmap 35313  df-padd 35605  df-lhyp 35797  df-laut 35798  df-ldil 35913  df-ltrn 35914  df-trl 35969
This theorem is referenced by:  dia2dimlem3  36876  dia2dimlem6  36879
  Copyright terms: Public domain W3C validator