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 41047
Description: Lemma for dia2dim 41060. 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 494 . . . 4 (𝜑𝐾 ∈ HL)
4 dia2dimlem1.p . . . . 5 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
54simpld 494 . . . 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 40152 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
132, 4, 6, 12syl3anc 1370 . . . 4 (𝜑 → (𝑅𝐹) ∈ 𝐴)
14 dia2dimlem1.u . . . . 5 (𝜑 → (𝑈𝐴𝑈 𝑊))
1514simpld 494 . . . 4 (𝜑𝑈𝐴)
166simpld 494 . . . . . 6 (𝜑𝐹𝑇)
177, 8, 9, 10ltrnel 40122 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
182, 16, 4, 17syl3anc 1370 . . . . 5 (𝜑 → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
1918simpld 494 . . . 4 (𝜑 → (𝐹𝑃) ∈ 𝐴)
20 dia2dimlem1.v . . . . 5 (𝜑 → (𝑉𝐴𝑉 𝑊))
2120simpld 494 . . . 4 (𝜑𝑉𝐴)
224simprd 495 . . . . . 6 (𝜑 → ¬ 𝑃 𝑊)
237, 9, 10, 11trlle 40167 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) 𝑊)
242, 16, 23syl2anc 584 . . . . . . . 8 (𝜑 → (𝑅𝐹) 𝑊)
2514simprd 495 . . . . . . . 8 (𝜑𝑈 𝑊)
263hllatd 39346 . . . . . . . . 9 (𝜑𝐾 ∈ Lat)
27 eqid 2735 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
2827, 8atbase 39271 . . . . . . . . . 10 ((𝑅𝐹) ∈ 𝐴 → (𝑅𝐹) ∈ (Base‘𝐾))
2913, 28syl 17 . . . . . . . . 9 (𝜑 → (𝑅𝐹) ∈ (Base‘𝐾))
3027, 8atbase 39271 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
3115, 30syl 17 . . . . . . . . 9 (𝜑𝑈 ∈ (Base‘𝐾))
322simprd 495 . . . . . . . . . 10 (𝜑𝑊𝐻)
3327, 9lhpbase 39981 . . . . . . . . . 10 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3432, 33syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ (Base‘𝐾))
35 dia2dimlem1.j . . . . . . . . . 10 = (join‘𝐾)
3627, 7, 35latjle12 18508 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑅𝐹) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3726, 29, 31, 34, 36syl13anc 1371 . . . . . . . 8 (𝜑 → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3824, 25, 37mpbi2and 712 . . . . . . 7 (𝜑 → ((𝑅𝐹) 𝑈) 𝑊)
3927, 8atbase 39271 . . . . . . . . 9 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
405, 39syl 17 . . . . . . . 8 (𝜑𝑃 ∈ (Base‘𝐾))
4127, 35, 8hlatjcl 39349 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑅𝐹) ∈ 𝐴𝑈𝐴) → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
423, 13, 15, 41syl3anc 1370 . . . . . . . 8 (𝜑 → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
4327, 7lattr 18502 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4426, 40, 42, 34, 43syl13anc 1371 . . . . . . 7 (𝜑 → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4538, 44mpan2d 694 . . . . . 6 (𝜑 → (𝑃 ((𝑅𝐹) 𝑈) → 𝑃 𝑊))
4622, 45mtod 198 . . . . 5 (𝜑 → ¬ 𝑃 ((𝑅𝐹) 𝑈))
4720simprd 495 . . . . . . 7 (𝜑𝑉 𝑊)
4818simprd 495 . . . . . . 7 (𝜑 → ¬ (𝐹𝑃) 𝑊)
49 nbrne2 5168 . . . . . . 7 ((𝑉 𝑊 ∧ ¬ (𝐹𝑃) 𝑊) → 𝑉 ≠ (𝐹𝑃))
5047, 48, 49syl2anc 584 . . . . . 6 (𝜑𝑉 ≠ (𝐹𝑃))
5150necomd 2994 . . . . 5 (𝜑 → (𝐹𝑃) ≠ 𝑉)
5246, 51jca 511 . . . 4 (𝜑 → (¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉))
5326adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝐾 ∈ Lat)
5440adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
5527, 35, 8hlatjcl 39349 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑉𝐴𝑈𝐴) → (𝑉 𝑈) ∈ (Base‘𝐾))
563, 21, 15, 55syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) ∈ (Base‘𝐾))
5756adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) ∈ (Base‘𝐾))
5834adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑊 ∈ (Base‘𝐾))
597, 35, 8hlatlej2 39358 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → 𝑉 ((𝐹𝑃) 𝑉))
603, 19, 21, 59syl3anc 1370 . . . . . . . . . . 11 (𝜑𝑉 ((𝐹𝑃) 𝑉))
6160adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 ((𝐹𝑃) 𝑉))
62 simpr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑃 𝑈) = ((𝐹𝑃) 𝑉))
6361, 62breqtrrd 5176 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 (𝑃 𝑈))
64 dia2dimlem1.uv . . . . . . . . . . . 12 (𝜑𝑈𝑉)
6564necomd 2994 . . . . . . . . . . 11 (𝜑𝑉𝑈)
667, 35, 8hlatexch2 39379 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴𝑃𝐴𝑈𝐴) ∧ 𝑉𝑈) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
673, 21, 5, 15, 65, 66syl131anc 1382 . . . . . . . . . 10 (𝜑 → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6867adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6963, 68mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 (𝑉 𝑈))
7027, 8atbase 39271 . . . . . . . . . . . 12 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
7121, 70syl 17 . . . . . . . . . . 11 (𝜑𝑉 ∈ (Base‘𝐾))
7227, 7, 35latjle12 18508 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7326, 71, 31, 34, 72syl13anc 1371 . . . . . . . . . 10 (𝜑 → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7447, 25, 73mpbi2and 712 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) 𝑊)
7574adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) 𝑊)
7627, 7, 53, 54, 57, 58, 69, 75lattrd 18504 . . . . . . 7 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 𝑊)
7776ex 412 . . . . . 6 (𝜑 → ((𝑃 𝑈) = ((𝐹𝑃) 𝑉) → 𝑃 𝑊))
7877necon3bd 2952 . . . . 5 (𝜑 → (¬ 𝑃 𝑊 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉)))
7922, 78mpd 15 . . . 4 (𝜑 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉))
807, 35, 8hlatlej2 39358 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝐹𝑃) (𝑃 (𝐹𝑃)))
813, 5, 19, 80syl3anc 1370 . . . . . 6 (𝜑 → (𝐹𝑃) (𝑃 (𝐹𝑃)))
82 dia2dimlem1.m . . . . . . . . . 10 = (meet‘𝐾)
837, 35, 82, 8, 9, 10, 11trlval2 40146 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
842, 16, 4, 83syl3anc 1370 . . . . . . . 8 (𝜑 → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
8584oveq2d 7447 . . . . . . 7 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)))
8627, 35, 8hlatjcl 39349 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
873, 5, 19, 86syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
887, 35, 8hlatlej1 39357 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → 𝑃 (𝑃 (𝐹𝑃)))
893, 5, 19, 88syl3anc 1370 . . . . . . . . 9 (𝜑𝑃 (𝑃 (𝐹𝑃)))
9027, 7, 35, 82, 8atmod3i1 39847 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 (𝐹𝑃))) → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
913, 5, 87, 34, 89, 90syl131anc 1382 . . . . . . . 8 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
92 eqid 2735 . . . . . . . . . . . 12 (1.‘𝐾) = (1.‘𝐾)
937, 35, 92, 8, 9lhpjat2 40004 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
942, 4, 93syl2anc 584 . . . . . . . . . 10 (𝜑 → (𝑃 𝑊) = (1.‘𝐾))
9594oveq2d 7447 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = ((𝑃 (𝐹𝑃)) (1.‘𝐾)))
96 hlol 39343 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
973, 96syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ OL)
9827, 82, 92olm11 39209 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
9997, 87, 98syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
10095, 99eqtrd 2775 . . . . . . . 8 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = (𝑃 (𝐹𝑃)))
10191, 100eqtrd 2775 . . . . . . 7 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = (𝑃 (𝐹𝑃)))
10285, 101eqtrd 2775 . . . . . 6 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 (𝐹𝑃)))
10381, 102breqtrrd 5176 . . . . 5 (𝜑 → (𝐹𝑃) (𝑃 (𝑅𝐹)))
104 dia2dimlem1.rf . . . . . . 7 (𝜑 → (𝑅𝐹) (𝑈 𝑉))
10535, 8hlatjcom 39350 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) = (𝑉 𝑈))
1063, 15, 21, 105syl3anc 1370 . . . . . . 7 (𝜑 → (𝑈 𝑉) = (𝑉 𝑈))
107104, 106breqtrd 5174 . . . . . 6 (𝜑 → (𝑅𝐹) (𝑉 𝑈))
108 dia2dimlem1.ru . . . . . . 7 (𝜑 → (𝑅𝐹) ≠ 𝑈)
1097, 35, 8hlatexch2 39379 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑉𝐴𝑈𝐴) ∧ (𝑅𝐹) ≠ 𝑈) → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
1103, 13, 21, 15, 108, 109syl131anc 1382 . . . . . 6 (𝜑 → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
111107, 110mpd 15 . . . . 5 (𝜑𝑉 ((𝑅𝐹) 𝑈))
112103, 111jca 511 . . . 4 (𝜑 → ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))
1137, 35, 82, 8ps-2c 39511 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝐹) ∈ 𝐴) ∧ (𝑈𝐴 ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) ∧ ((¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉) ∧ (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉) ∧ ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1143, 5, 13, 15, 19, 21, 52, 79, 112, 113syl333anc 1401 . . 3 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1151, 114eqeltrid 2843 . 2 (𝜑𝑄𝐴)
11627, 35, 8hlatjcl 39349 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
1173, 5, 15, 116syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → (𝑃 𝑈) ∈ (Base‘𝐾))
11827, 35, 8hlatjcl 39349 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
1193, 19, 21, 118syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
12027, 7, 82latmle1 18522 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
12126, 117, 119, 120syl3anc 1370 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
1221, 121eqbrtrid 5183 . . . . . . . . . 10 (𝜑𝑄 (𝑃 𝑈))
12327, 8atbase 39271 . . . . . . . . . . . . 13 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
124115, 123syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (Base‘𝐾))
12527, 7, 82latlem12 18524 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
12626, 124, 117, 34, 125syl13anc 1371 . . . . . . . . . . 11 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
127126biimpd 229 . . . . . . . . . 10 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊)))
128122, 127mpand 695 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 ((𝑃 𝑈) 𝑊)))
129128imp 406 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊))
130 eqid 2735 . . . . . . . . . . . . 13 (0.‘𝐾) = (0.‘𝐾)
1317, 82, 130, 8, 9lhpmat 40013 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (0.‘𝐾))
1322, 4, 131syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝑃 𝑊) = (0.‘𝐾))
133132oveq1d 7446 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((0.‘𝐾) 𝑈))
13427, 7, 35, 82, 8atmod4i1 39849 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 𝑊) → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
1353, 15, 40, 34, 25, 134syl131anc 1382 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
13627, 35, 130olj02 39208 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑈 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑈) = 𝑈)
13797, 31, 136syl2anc 584 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑈) = 𝑈)
138133, 135, 1373eqtr3d 2783 . . . . . . . . 9 (𝜑 → ((𝑃 𝑈) 𝑊) = 𝑈)
139138adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → ((𝑃 𝑈) 𝑊) = 𝑈)
140129, 139breqtrd 5174 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑈)
141 hlatl 39342 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
1423, 141syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ AtLat)
143142adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝐾 ∈ AtLat)
144115adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄𝐴)
14515adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑈𝐴)
1467, 8atcmp 39293 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑈𝐴) → (𝑄 𝑈𝑄 = 𝑈))
147143, 144, 145, 146syl3anc 1370 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑈𝑄 = 𝑈))
148140, 147mpbid 232 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑈)
14927, 7, 82latmle2 18523 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
15026, 117, 119, 149syl3anc 1370 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
1511, 150eqbrtrid 5183 . . . . . . . . . 10 (𝜑𝑄 ((𝐹𝑃) 𝑉))
15227, 7, 82latlem12 18524 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
15326, 124, 119, 34, 152syl13anc 1371 . . . . . . . . . . 11 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
154153biimpd 229 . . . . . . . . . 10 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
155151, 154mpand 695 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
156155imp 406 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊))
1577, 82, 130, 8, 9lhpmat 40013 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊)) → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
1582, 18, 157syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
159158oveq1d 7446 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = ((0.‘𝐾) 𝑉))
16027, 8atbase 39271 . . . . . . . . . . . 12 ((𝐹𝑃) ∈ 𝐴 → (𝐹𝑃) ∈ (Base‘𝐾))
16119, 160syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) ∈ (Base‘𝐾))
16227, 7, 35, 82, 8atmod4i1 39849 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴 ∧ (𝐹𝑃) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 𝑊) → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
1633, 21, 161, 34, 47, 162syl131anc 1382 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
16427, 35, 130olj02 39208 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑉 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑉) = 𝑉)
16597, 71, 164syl2anc 584 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑉) = 𝑉)
166159, 163, 1653eqtr3d 2783 . . . . . . . . 9 (𝜑 → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
167166adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
168156, 167breqtrd 5174 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑉)
16921adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑉𝐴)
1707, 8atcmp 39293 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑉𝐴) → (𝑄 𝑉𝑄 = 𝑉))
171143, 144, 169, 170syl3anc 1370 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑉𝑄 = 𝑉))
172168, 171mpbid 232 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑉)
173148, 172eqtr3d 2777 . . . . 5 ((𝜑𝑄 𝑊) → 𝑈 = 𝑉)
174173ex 412 . . . 4 (𝜑 → (𝑄 𝑊𝑈 = 𝑉))
175174necon3ad 2951 . . 3 (𝜑 → (𝑈𝑉 → ¬ 𝑄 𝑊))
17664, 175mpd 15 . 2 (𝜑 → ¬ 𝑄 𝑊)
177115, 176jca 511 1 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wne 2938   class class class wbr 5148  cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305  joincjn 18369  meetcmee 18370  0.cp0 18481  1.cp1 18482  Latclat 18489  OLcol 39156  Atomscatm 39245  AtLatcal 39246  HLchlt 39332  LHypclh 39967  LTrncltrn 40084  trLctrl 40141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-map 8867  df-proset 18352  df-poset 18371  df-plt 18388  df-lub 18404  df-glb 18405  df-join 18406  df-meet 18407  df-p0 18483  df-p1 18484  df-lat 18490  df-clat 18557  df-oposet 39158  df-ol 39160  df-oml 39161  df-covers 39248  df-ats 39249  df-atl 39280  df-cvlat 39304  df-hlat 39333  df-llines 39481  df-psubsp 39486  df-pmap 39487  df-padd 39779  df-lhyp 39971  df-laut 39972  df-ldil 40087  df-ltrn 40088  df-trl 40142
This theorem is referenced by:  dia2dimlem3  41049  dia2dimlem6  41052
  Copyright terms: Public domain W3C validator