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 36952
Description: Lemma for dia2dim 36965. 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 488 . . . 4 (𝜑𝐾 ∈ HL)
4 dia2dimlem1.p . . . . 5 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
54simpld 488 . . . 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 36057 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
132, 4, 6, 12syl3anc 1490 . . . 4 (𝜑 → (𝑅𝐹) ∈ 𝐴)
14 dia2dimlem1.u . . . . 5 (𝜑 → (𝑈𝐴𝑈 𝑊))
1514simpld 488 . . . 4 (𝜑𝑈𝐴)
166simpld 488 . . . . . 6 (𝜑𝐹𝑇)
177, 8, 9, 10ltrnel 36027 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
182, 16, 4, 17syl3anc 1490 . . . . 5 (𝜑 → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
1918simpld 488 . . . 4 (𝜑 → (𝐹𝑃) ∈ 𝐴)
20 dia2dimlem1.v . . . . 5 (𝜑 → (𝑉𝐴𝑉 𝑊))
2120simpld 488 . . . 4 (𝜑𝑉𝐴)
224simprd 489 . . . . . 6 (𝜑 → ¬ 𝑃 𝑊)
237, 9, 10, 11trlle 36072 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) 𝑊)
242, 16, 23syl2anc 579 . . . . . . . 8 (𝜑 → (𝑅𝐹) 𝑊)
2514simprd 489 . . . . . . . 8 (𝜑𝑈 𝑊)
263hllatd 35252 . . . . . . . . 9 (𝜑𝐾 ∈ Lat)
27 eqid 2765 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
2827, 8atbase 35177 . . . . . . . . . 10 ((𝑅𝐹) ∈ 𝐴 → (𝑅𝐹) ∈ (Base‘𝐾))
2913, 28syl 17 . . . . . . . . 9 (𝜑 → (𝑅𝐹) ∈ (Base‘𝐾))
3027, 8atbase 35177 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
3115, 30syl 17 . . . . . . . . 9 (𝜑𝑈 ∈ (Base‘𝐾))
322simprd 489 . . . . . . . . . 10 (𝜑𝑊𝐻)
3327, 9lhpbase 35886 . . . . . . . . . 10 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3432, 33syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ (Base‘𝐾))
35 dia2dimlem1.j . . . . . . . . . 10 = (join‘𝐾)
3627, 7, 35latjle12 17330 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑅𝐹) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3726, 29, 31, 34, 36syl13anc 1491 . . . . . . . 8 (𝜑 → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3824, 25, 37mpbi2and 703 . . . . . . 7 (𝜑 → ((𝑅𝐹) 𝑈) 𝑊)
3927, 8atbase 35177 . . . . . . . . 9 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
405, 39syl 17 . . . . . . . 8 (𝜑𝑃 ∈ (Base‘𝐾))
4127, 35, 8hlatjcl 35255 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑅𝐹) ∈ 𝐴𝑈𝐴) → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
423, 13, 15, 41syl3anc 1490 . . . . . . . 8 (𝜑 → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
4327, 7lattr 17324 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4426, 40, 42, 34, 43syl13anc 1491 . . . . . . 7 (𝜑 → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4538, 44mpan2d 685 . . . . . 6 (𝜑 → (𝑃 ((𝑅𝐹) 𝑈) → 𝑃 𝑊))
4622, 45mtod 189 . . . . 5 (𝜑 → ¬ 𝑃 ((𝑅𝐹) 𝑈))
4720simprd 489 . . . . . . 7 (𝜑𝑉 𝑊)
4818simprd 489 . . . . . . 7 (𝜑 → ¬ (𝐹𝑃) 𝑊)
49 nbrne2 4829 . . . . . . 7 ((𝑉 𝑊 ∧ ¬ (𝐹𝑃) 𝑊) → 𝑉 ≠ (𝐹𝑃))
5047, 48, 49syl2anc 579 . . . . . 6 (𝜑𝑉 ≠ (𝐹𝑃))
5150necomd 2992 . . . . 5 (𝜑 → (𝐹𝑃) ≠ 𝑉)
5246, 51jca 507 . . . 4 (𝜑 → (¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉))
5326adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝐾 ∈ Lat)
5440adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
5527, 35, 8hlatjcl 35255 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑉𝐴𝑈𝐴) → (𝑉 𝑈) ∈ (Base‘𝐾))
563, 21, 15, 55syl3anc 1490 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) ∈ (Base‘𝐾))
5756adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) ∈ (Base‘𝐾))
5834adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑊 ∈ (Base‘𝐾))
597, 35, 8hlatlej2 35264 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → 𝑉 ((𝐹𝑃) 𝑉))
603, 19, 21, 59syl3anc 1490 . . . . . . . . . . 11 (𝜑𝑉 ((𝐹𝑃) 𝑉))
6160adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 ((𝐹𝑃) 𝑉))
62 simpr 477 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑃 𝑈) = ((𝐹𝑃) 𝑉))
6361, 62breqtrrd 4837 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 (𝑃 𝑈))
64 dia2dimlem1.uv . . . . . . . . . . . 12 (𝜑𝑈𝑉)
6564necomd 2992 . . . . . . . . . . 11 (𝜑𝑉𝑈)
667, 35, 8hlatexch2 35284 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴𝑃𝐴𝑈𝐴) ∧ 𝑉𝑈) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
673, 21, 5, 15, 65, 66syl131anc 1502 . . . . . . . . . 10 (𝜑 → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6867adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6963, 68mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 (𝑉 𝑈))
7027, 8atbase 35177 . . . . . . . . . . . 12 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
7121, 70syl 17 . . . . . . . . . . 11 (𝜑𝑉 ∈ (Base‘𝐾))
7227, 7, 35latjle12 17330 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7326, 71, 31, 34, 72syl13anc 1491 . . . . . . . . . 10 (𝜑 → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7447, 25, 73mpbi2and 703 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) 𝑊)
7574adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) 𝑊)
7627, 7, 53, 54, 57, 58, 69, 75lattrd 17326 . . . . . . 7 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 𝑊)
7776ex 401 . . . . . 6 (𝜑 → ((𝑃 𝑈) = ((𝐹𝑃) 𝑉) → 𝑃 𝑊))
7877necon3bd 2951 . . . . 5 (𝜑 → (¬ 𝑃 𝑊 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉)))
7922, 78mpd 15 . . . 4 (𝜑 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉))
807, 35, 8hlatlej2 35264 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝐹𝑃) (𝑃 (𝐹𝑃)))
813, 5, 19, 80syl3anc 1490 . . . . . 6 (𝜑 → (𝐹𝑃) (𝑃 (𝐹𝑃)))
82 dia2dimlem1.m . . . . . . . . . 10 = (meet‘𝐾)
837, 35, 82, 8, 9, 10, 11trlval2 36051 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
842, 16, 4, 83syl3anc 1490 . . . . . . . 8 (𝜑 → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
8584oveq2d 6858 . . . . . . 7 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)))
8627, 35, 8hlatjcl 35255 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
873, 5, 19, 86syl3anc 1490 . . . . . . . . 9 (𝜑 → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
887, 35, 8hlatlej1 35263 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → 𝑃 (𝑃 (𝐹𝑃)))
893, 5, 19, 88syl3anc 1490 . . . . . . . . 9 (𝜑𝑃 (𝑃 (𝐹𝑃)))
9027, 7, 35, 82, 8atmod3i1 35752 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 (𝐹𝑃))) → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
913, 5, 87, 34, 89, 90syl131anc 1502 . . . . . . . 8 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
92 eqid 2765 . . . . . . . . . . . 12 (1.‘𝐾) = (1.‘𝐾)
937, 35, 92, 8, 9lhpjat2 35909 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
942, 4, 93syl2anc 579 . . . . . . . . . 10 (𝜑 → (𝑃 𝑊) = (1.‘𝐾))
9594oveq2d 6858 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = ((𝑃 (𝐹𝑃)) (1.‘𝐾)))
96 hlol 35249 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
973, 96syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ OL)
9827, 82, 92olm11 35115 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
9997, 87, 98syl2anc 579 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
10095, 99eqtrd 2799 . . . . . . . 8 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = (𝑃 (𝐹𝑃)))
10191, 100eqtrd 2799 . . . . . . 7 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = (𝑃 (𝐹𝑃)))
10285, 101eqtrd 2799 . . . . . 6 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 (𝐹𝑃)))
10381, 102breqtrrd 4837 . . . . 5 (𝜑 → (𝐹𝑃) (𝑃 (𝑅𝐹)))
104 dia2dimlem1.rf . . . . . . 7 (𝜑 → (𝑅𝐹) (𝑈 𝑉))
10535, 8hlatjcom 35256 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) = (𝑉 𝑈))
1063, 15, 21, 105syl3anc 1490 . . . . . . 7 (𝜑 → (𝑈 𝑉) = (𝑉 𝑈))
107104, 106breqtrd 4835 . . . . . 6 (𝜑 → (𝑅𝐹) (𝑉 𝑈))
108 dia2dimlem1.ru . . . . . . 7 (𝜑 → (𝑅𝐹) ≠ 𝑈)
1097, 35, 8hlatexch2 35284 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑉𝐴𝑈𝐴) ∧ (𝑅𝐹) ≠ 𝑈) → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
1103, 13, 21, 15, 108, 109syl131anc 1502 . . . . . 6 (𝜑 → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
111107, 110mpd 15 . . . . 5 (𝜑𝑉 ((𝑅𝐹) 𝑈))
112103, 111jca 507 . . . 4 (𝜑 → ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))
1137, 35, 82, 8ps-2c 35416 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝐹) ∈ 𝐴) ∧ (𝑈𝐴 ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) ∧ ((¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉) ∧ (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉) ∧ ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1143, 5, 13, 15, 19, 21, 52, 79, 112, 113syl333anc 1521 . . 3 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1151, 114syl5eqel 2848 . 2 (𝜑𝑄𝐴)
11627, 35, 8hlatjcl 35255 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
1173, 5, 15, 116syl3anc 1490 . . . . . . . . . . . 12 (𝜑 → (𝑃 𝑈) ∈ (Base‘𝐾))
11827, 35, 8hlatjcl 35255 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
1193, 19, 21, 118syl3anc 1490 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
12027, 7, 82latmle1 17344 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
12126, 117, 119, 120syl3anc 1490 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
1221, 121syl5eqbr 4844 . . . . . . . . . 10 (𝜑𝑄 (𝑃 𝑈))
12327, 8atbase 35177 . . . . . . . . . . . . 13 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
124115, 123syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (Base‘𝐾))
12527, 7, 82latlem12 17346 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
12626, 124, 117, 34, 125syl13anc 1491 . . . . . . . . . . 11 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
127126biimpd 220 . . . . . . . . . 10 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊)))
128122, 127mpand 686 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 ((𝑃 𝑈) 𝑊)))
129128imp 395 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊))
130 eqid 2765 . . . . . . . . . . . . 13 (0.‘𝐾) = (0.‘𝐾)
1317, 82, 130, 8, 9lhpmat 35918 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (0.‘𝐾))
1322, 4, 131syl2anc 579 . . . . . . . . . . 11 (𝜑 → (𝑃 𝑊) = (0.‘𝐾))
133132oveq1d 6857 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((0.‘𝐾) 𝑈))
13427, 7, 35, 82, 8atmod4i1 35754 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 𝑊) → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
1353, 15, 40, 34, 25, 134syl131anc 1502 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
13627, 35, 130olj02 35114 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑈 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑈) = 𝑈)
13797, 31, 136syl2anc 579 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑈) = 𝑈)
138133, 135, 1373eqtr3d 2807 . . . . . . . . 9 (𝜑 → ((𝑃 𝑈) 𝑊) = 𝑈)
139138adantr 472 . . . . . . . 8 ((𝜑𝑄 𝑊) → ((𝑃 𝑈) 𝑊) = 𝑈)
140129, 139breqtrd 4835 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑈)
141 hlatl 35248 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
1423, 141syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ AtLat)
143142adantr 472 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝐾 ∈ AtLat)
144115adantr 472 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄𝐴)
14515adantr 472 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑈𝐴)
1467, 8atcmp 35199 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑈𝐴) → (𝑄 𝑈𝑄 = 𝑈))
147143, 144, 145, 146syl3anc 1490 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑈𝑄 = 𝑈))
148140, 147mpbid 223 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑈)
14927, 7, 82latmle2 17345 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
15026, 117, 119, 149syl3anc 1490 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
1511, 150syl5eqbr 4844 . . . . . . . . . 10 (𝜑𝑄 ((𝐹𝑃) 𝑉))
15227, 7, 82latlem12 17346 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
15326, 124, 119, 34, 152syl13anc 1491 . . . . . . . . . . 11 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
154153biimpd 220 . . . . . . . . . 10 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
155151, 154mpand 686 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
156155imp 395 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊))
1577, 82, 130, 8, 9lhpmat 35918 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊)) → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
1582, 18, 157syl2anc 579 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
159158oveq1d 6857 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = ((0.‘𝐾) 𝑉))
16027, 8atbase 35177 . . . . . . . . . . . 12 ((𝐹𝑃) ∈ 𝐴 → (𝐹𝑃) ∈ (Base‘𝐾))
16119, 160syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) ∈ (Base‘𝐾))
16227, 7, 35, 82, 8atmod4i1 35754 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴 ∧ (𝐹𝑃) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 𝑊) → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
1633, 21, 161, 34, 47, 162syl131anc 1502 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
16427, 35, 130olj02 35114 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑉 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑉) = 𝑉)
16597, 71, 164syl2anc 579 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑉) = 𝑉)
166159, 163, 1653eqtr3d 2807 . . . . . . . . 9 (𝜑 → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
167166adantr 472 . . . . . . . 8 ((𝜑𝑄 𝑊) → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
168156, 167breqtrd 4835 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑉)
16921adantr 472 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑉𝐴)
1707, 8atcmp 35199 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑉𝐴) → (𝑄 𝑉𝑄 = 𝑉))
171143, 144, 169, 170syl3anc 1490 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑉𝑄 = 𝑉))
172168, 171mpbid 223 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑉)
173148, 172eqtr3d 2801 . . . . 5 ((𝜑𝑄 𝑊) → 𝑈 = 𝑉)
174173ex 401 . . . 4 (𝜑 → (𝑄 𝑊𝑈 = 𝑉))
175174necon3ad 2950 . . 3 (𝜑 → (𝑈𝑉 → ¬ 𝑄 𝑊))
17664, 175mpd 15 . 2 (𝜑 → ¬ 𝑄 𝑊)
177115, 176jca 507 1 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937   class class class wbr 4809  cfv 6068  (class class class)co 6842  Basecbs 16132  lecple 16223  joincjn 17212  meetcmee 17213  0.cp0 17305  1.cp1 17306  Latclat 17313  OLcol 35062  Atomscatm 35151  AtLatcal 35152  HLchlt 35238  LHypclh 35872  LTrncltrn 35989  trLctrl 36046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-map 8062  df-proset 17196  df-poset 17214  df-plt 17226  df-lub 17242  df-glb 17243  df-join 17244  df-meet 17245  df-p0 17307  df-p1 17308  df-lat 17314  df-clat 17376  df-oposet 35064  df-ol 35066  df-oml 35067  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-llines 35386  df-psubsp 35391  df-pmap 35392  df-padd 35684  df-lhyp 35876  df-laut 35877  df-ldil 35992  df-ltrn 35993  df-trl 36047
This theorem is referenced by:  dia2dimlem3  36954  dia2dimlem6  36957
  Copyright terms: Public domain W3C validator