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 36670
Description: Lemma for dia2dim 36683. 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 474 . . . 4 (𝜑𝐾 ∈ HL)
4 dia2dimlem1.p . . . . 5 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
54simpld 474 . . . 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 35774 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
132, 4, 6, 12syl3anc 1366 . . . 4 (𝜑 → (𝑅𝐹) ∈ 𝐴)
14 dia2dimlem1.u . . . . 5 (𝜑 → (𝑈𝐴𝑈 𝑊))
1514simpld 474 . . . 4 (𝜑𝑈𝐴)
166simpld 474 . . . . . 6 (𝜑𝐹𝑇)
177, 8, 9, 10ltrnel 35743 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
182, 16, 4, 17syl3anc 1366 . . . . 5 (𝜑 → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
1918simpld 474 . . . 4 (𝜑 → (𝐹𝑃) ∈ 𝐴)
20 dia2dimlem1.v . . . . 5 (𝜑 → (𝑉𝐴𝑉 𝑊))
2120simpld 474 . . . 4 (𝜑𝑉𝐴)
224simprd 478 . . . . . 6 (𝜑 → ¬ 𝑃 𝑊)
237, 9, 10, 11trlle 35789 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) 𝑊)
242, 16, 23syl2anc 694 . . . . . . . 8 (𝜑 → (𝑅𝐹) 𝑊)
2514simprd 478 . . . . . . . 8 (𝜑𝑈 𝑊)
26 hllat 34968 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ Lat)
273, 26syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Lat)
28 eqid 2651 . . . . . . . . . . 11 (Base‘𝐾) = (Base‘𝐾)
2928, 8atbase 34894 . . . . . . . . . 10 ((𝑅𝐹) ∈ 𝐴 → (𝑅𝐹) ∈ (Base‘𝐾))
3013, 29syl 17 . . . . . . . . 9 (𝜑 → (𝑅𝐹) ∈ (Base‘𝐾))
3128, 8atbase 34894 . . . . . . . . . 10 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
3215, 31syl 17 . . . . . . . . 9 (𝜑𝑈 ∈ (Base‘𝐾))
332simprd 478 . . . . . . . . . 10 (𝜑𝑊𝐻)
3428, 9lhpbase 35602 . . . . . . . . . 10 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3533, 34syl 17 . . . . . . . . 9 (𝜑𝑊 ∈ (Base‘𝐾))
36 dia2dimlem1.j . . . . . . . . . 10 = (join‘𝐾)
3728, 7, 36latjle12 17109 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((𝑅𝐹) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3827, 30, 32, 35, 37syl13anc 1368 . . . . . . . 8 (𝜑 → (((𝑅𝐹) 𝑊𝑈 𝑊) ↔ ((𝑅𝐹) 𝑈) 𝑊))
3924, 25, 38mpbi2and 976 . . . . . . 7 (𝜑 → ((𝑅𝐹) 𝑈) 𝑊)
4028, 8atbase 34894 . . . . . . . . 9 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
415, 40syl 17 . . . . . . . 8 (𝜑𝑃 ∈ (Base‘𝐾))
4228, 36, 8hlatjcl 34971 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑅𝐹) ∈ 𝐴𝑈𝐴) → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
433, 13, 15, 42syl3anc 1366 . . . . . . . 8 (𝜑 → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
4428, 7lattr 17103 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4527, 41, 43, 35, 44syl13anc 1368 . . . . . . 7 (𝜑 → ((𝑃 ((𝑅𝐹) 𝑈) ∧ ((𝑅𝐹) 𝑈) 𝑊) → 𝑃 𝑊))
4639, 45mpan2d 710 . . . . . 6 (𝜑 → (𝑃 ((𝑅𝐹) 𝑈) → 𝑃 𝑊))
4722, 46mtod 189 . . . . 5 (𝜑 → ¬ 𝑃 ((𝑅𝐹) 𝑈))
4820simprd 478 . . . . . . 7 (𝜑𝑉 𝑊)
4918simprd 478 . . . . . . 7 (𝜑 → ¬ (𝐹𝑃) 𝑊)
50 nbrne2 4705 . . . . . . 7 ((𝑉 𝑊 ∧ ¬ (𝐹𝑃) 𝑊) → 𝑉 ≠ (𝐹𝑃))
5148, 49, 50syl2anc 694 . . . . . 6 (𝜑𝑉 ≠ (𝐹𝑃))
5251necomd 2878 . . . . 5 (𝜑 → (𝐹𝑃) ≠ 𝑉)
5347, 52jca 553 . . . 4 (𝜑 → (¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉))
5427adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝐾 ∈ Lat)
5541adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
5628, 36, 8hlatjcl 34971 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑉𝐴𝑈𝐴) → (𝑉 𝑈) ∈ (Base‘𝐾))
573, 21, 15, 56syl3anc 1366 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) ∈ (Base‘𝐾))
5857adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) ∈ (Base‘𝐾))
5935adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑊 ∈ (Base‘𝐾))
607, 36, 8hlatlej2 34980 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → 𝑉 ((𝐹𝑃) 𝑉))
613, 19, 21, 60syl3anc 1366 . . . . . . . . . . 11 (𝜑𝑉 ((𝐹𝑃) 𝑉))
6261adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 ((𝐹𝑃) 𝑉))
63 simpr 476 . . . . . . . . . 10 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑃 𝑈) = ((𝐹𝑃) 𝑉))
6462, 63breqtrrd 4713 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑉 (𝑃 𝑈))
65 dia2dimlem1.uv . . . . . . . . . . . 12 (𝜑𝑈𝑉)
6665necomd 2878 . . . . . . . . . . 11 (𝜑𝑉𝑈)
677, 36, 8hlatexch2 35000 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴𝑃𝐴𝑈𝐴) ∧ 𝑉𝑈) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
683, 21, 5, 15, 66, 67syl131anc 1379 . . . . . . . . . 10 (𝜑 → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
6968adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 (𝑃 𝑈) → 𝑃 (𝑉 𝑈)))
7064, 69mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 (𝑉 𝑈))
7128, 8atbase 34894 . . . . . . . . . . . 12 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
7221, 71syl 17 . . . . . . . . . . 11 (𝜑𝑉 ∈ (Base‘𝐾))
7328, 7, 36latjle12 17109 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7427, 72, 32, 35, 73syl13anc 1368 . . . . . . . . . 10 (𝜑 → ((𝑉 𝑊𝑈 𝑊) ↔ (𝑉 𝑈) 𝑊))
7548, 25, 74mpbi2and 976 . . . . . . . . 9 (𝜑 → (𝑉 𝑈) 𝑊)
7675adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → (𝑉 𝑈) 𝑊)
7728, 7, 54, 55, 58, 59, 70, 76lattrd 17105 . . . . . . 7 ((𝜑 ∧ (𝑃 𝑈) = ((𝐹𝑃) 𝑉)) → 𝑃 𝑊)
7877ex 449 . . . . . 6 (𝜑 → ((𝑃 𝑈) = ((𝐹𝑃) 𝑉) → 𝑃 𝑊))
7978necon3bd 2837 . . . . 5 (𝜑 → (¬ 𝑃 𝑊 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉)))
8022, 79mpd 15 . . . 4 (𝜑 → (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉))
817, 36, 8hlatlej2 34980 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝐹𝑃) (𝑃 (𝐹𝑃)))
823, 5, 19, 81syl3anc 1366 . . . . . 6 (𝜑 → (𝐹𝑃) (𝑃 (𝐹𝑃)))
83 dia2dimlem1.m . . . . . . . . . 10 = (meet‘𝐾)
847, 36, 83, 8, 9, 10, 11trlval2 35768 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
852, 16, 4, 84syl3anc 1366 . . . . . . . 8 (𝜑 → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
8685oveq2d 6706 . . . . . . 7 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)))
8728, 36, 8hlatjcl 34971 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
883, 5, 19, 87syl3anc 1366 . . . . . . . . 9 (𝜑 → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
897, 36, 8hlatlej1 34979 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → 𝑃 (𝑃 (𝐹𝑃)))
903, 5, 19, 89syl3anc 1366 . . . . . . . . 9 (𝜑𝑃 (𝑃 (𝐹𝑃)))
9128, 7, 36, 83, 8atmod3i1 35468 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 (𝐹𝑃))) → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
923, 5, 88, 35, 90, 91syl131anc 1379 . . . . . . . 8 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = ((𝑃 (𝐹𝑃)) (𝑃 𝑊)))
93 eqid 2651 . . . . . . . . . . . 12 (1.‘𝐾) = (1.‘𝐾)
947, 36, 93, 8, 9lhpjat2 35625 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (1.‘𝐾))
952, 4, 94syl2anc 694 . . . . . . . . . 10 (𝜑 → (𝑃 𝑊) = (1.‘𝐾))
9695oveq2d 6706 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = ((𝑃 (𝐹𝑃)) (1.‘𝐾)))
97 hlol 34966 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
983, 97syl 17 . . . . . . . . . 10 (𝜑𝐾 ∈ OL)
9928, 83, 93olm11 34832 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
10098, 88, 99syl2anc 694 . . . . . . . . 9 (𝜑 → ((𝑃 (𝐹𝑃)) (1.‘𝐾)) = (𝑃 (𝐹𝑃)))
10196, 100eqtrd 2685 . . . . . . . 8 (𝜑 → ((𝑃 (𝐹𝑃)) (𝑃 𝑊)) = (𝑃 (𝐹𝑃)))
10292, 101eqtrd 2685 . . . . . . 7 (𝜑 → (𝑃 ((𝑃 (𝐹𝑃)) 𝑊)) = (𝑃 (𝐹𝑃)))
10386, 102eqtrd 2685 . . . . . 6 (𝜑 → (𝑃 (𝑅𝐹)) = (𝑃 (𝐹𝑃)))
10482, 103breqtrrd 4713 . . . . 5 (𝜑 → (𝐹𝑃) (𝑃 (𝑅𝐹)))
105 dia2dimlem1.rf . . . . . . 7 (𝜑 → (𝑅𝐹) (𝑈 𝑉))
10636, 8hlatjcom 34972 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) = (𝑉 𝑈))
1073, 15, 21, 106syl3anc 1366 . . . . . . 7 (𝜑 → (𝑈 𝑉) = (𝑉 𝑈))
108105, 107breqtrd 4711 . . . . . 6 (𝜑 → (𝑅𝐹) (𝑉 𝑈))
109 dia2dimlem1.ru . . . . . . 7 (𝜑 → (𝑅𝐹) ≠ 𝑈)
1107, 36, 8hlatexch2 35000 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑉𝐴𝑈𝐴) ∧ (𝑅𝐹) ≠ 𝑈) → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
1113, 13, 21, 15, 109, 110syl131anc 1379 . . . . . 6 (𝜑 → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
112108, 111mpd 15 . . . . 5 (𝜑𝑉 ((𝑅𝐹) 𝑈))
113104, 112jca 553 . . . 4 (𝜑 → ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))
1147, 36, 83, 8ps-2c 35132 . . . 4 (((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝐹) ∈ 𝐴) ∧ (𝑈𝐴 ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) ∧ ((¬ 𝑃 ((𝑅𝐹) 𝑈) ∧ (𝐹𝑃) ≠ 𝑉) ∧ (𝑃 𝑈) ≠ ((𝐹𝑃) 𝑉) ∧ ((𝐹𝑃) (𝑃 (𝑅𝐹)) ∧ 𝑉 ((𝑅𝐹) 𝑈)))) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1153, 5, 13, 15, 19, 21, 53, 80, 113, 114syl333anc 1398 . . 3 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ∈ 𝐴)
1161, 115syl5eqel 2734 . 2 (𝜑𝑄𝐴)
11728, 36, 8hlatjcl 34971 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
1183, 5, 15, 117syl3anc 1366 . . . . . . . . . . . 12 (𝜑 → (𝑃 𝑈) ∈ (Base‘𝐾))
11928, 36, 8hlatjcl 34971 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
1203, 19, 21, 119syl3anc 1366 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
12128, 7, 83latmle1 17123 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
12227, 118, 120, 121syl3anc 1366 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝑃 𝑈))
1231, 122syl5eqbr 4720 . . . . . . . . . 10 (𝜑𝑄 (𝑃 𝑈))
12428, 8atbase 34894 . . . . . . . . . . . . 13 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
125116, 124syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (Base‘𝐾))
12628, 7, 83latlem12 17125 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
12727, 125, 118, 35, 126syl13anc 1368 . . . . . . . . . . 11 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) ↔ 𝑄 ((𝑃 𝑈) 𝑊)))
128127biimpd 219 . . . . . . . . . 10 (𝜑 → ((𝑄 (𝑃 𝑈) ∧ 𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊)))
129123, 128mpand 711 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 ((𝑃 𝑈) 𝑊)))
130129imp 444 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 ((𝑃 𝑈) 𝑊))
131 eqid 2651 . . . . . . . . . . . . 13 (0.‘𝐾) = (0.‘𝐾)
1327, 83, 131, 8, 9lhpmat 35634 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 𝑊) = (0.‘𝐾))
1332, 4, 132syl2anc 694 . . . . . . . . . . 11 (𝜑 → (𝑃 𝑊) = (0.‘𝐾))
134133oveq1d 6705 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((0.‘𝐾) 𝑈))
13528, 7, 36, 83, 8atmod4i1 35470 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑈𝐴𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 𝑊) → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
1363, 15, 41, 35, 25, 135syl131anc 1379 . . . . . . . . . 10 (𝜑 → ((𝑃 𝑊) 𝑈) = ((𝑃 𝑈) 𝑊))
13728, 36, 131olj02 34831 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑈 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑈) = 𝑈)
13898, 32, 137syl2anc 694 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑈) = 𝑈)
139134, 136, 1383eqtr3d 2693 . . . . . . . . 9 (𝜑 → ((𝑃 𝑈) 𝑊) = 𝑈)
140139adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → ((𝑃 𝑈) 𝑊) = 𝑈)
141130, 140breqtrd 4711 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑈)
142 hlatl 34965 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
1433, 142syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ AtLat)
144143adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝐾 ∈ AtLat)
145116adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄𝐴)
14615adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑈𝐴)
1477, 8atcmp 34916 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑈𝐴) → (𝑄 𝑈𝑄 = 𝑈))
148144, 145, 146, 147syl3anc 1366 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑈𝑄 = 𝑈))
149141, 148mpbid 222 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑈)
15028, 7, 83latmle2 17124 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
15127, 118, 120, 150syl3anc 1366 . . . . . . . . . . 11 (𝜑 → ((𝑃 𝑈) ((𝐹𝑃) 𝑉)) ((𝐹𝑃) 𝑉))
1521, 151syl5eqbr 4720 . . . . . . . . . 10 (𝜑𝑄 ((𝐹𝑃) 𝑉))
15328, 7, 83latlem12 17125 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
15427, 125, 120, 35, 153syl13anc 1368 . . . . . . . . . . 11 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) ↔ 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
155154biimpd 219 . . . . . . . . . 10 (𝜑 → ((𝑄 ((𝐹𝑃) 𝑉) ∧ 𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
156152, 155mpand 711 . . . . . . . . 9 (𝜑 → (𝑄 𝑊𝑄 (((𝐹𝑃) 𝑉) 𝑊)))
157156imp 444 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑄 (((𝐹𝑃) 𝑉) 𝑊))
1587, 83, 131, 8, 9lhpmat 35634 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊)) → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
1592, 18, 158syl2anc 694 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑃) 𝑊) = (0.‘𝐾))
160159oveq1d 6705 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = ((0.‘𝐾) 𝑉))
16128, 8atbase 34894 . . . . . . . . . . . 12 ((𝐹𝑃) ∈ 𝐴 → (𝐹𝑃) ∈ (Base‘𝐾))
16219, 161syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) ∈ (Base‘𝐾))
16328, 7, 36, 83, 8atmod4i1 35470 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑉𝐴 ∧ (𝐹𝑃) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 𝑊) → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
1643, 21, 162, 35, 48, 163syl131anc 1379 . . . . . . . . . 10 (𝜑 → (((𝐹𝑃) 𝑊) 𝑉) = (((𝐹𝑃) 𝑉) 𝑊))
16528, 36, 131olj02 34831 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑉 ∈ (Base‘𝐾)) → ((0.‘𝐾) 𝑉) = 𝑉)
16698, 72, 165syl2anc 694 . . . . . . . . . 10 (𝜑 → ((0.‘𝐾) 𝑉) = 𝑉)
167160, 164, 1663eqtr3d 2693 . . . . . . . . 9 (𝜑 → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
168167adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → (((𝐹𝑃) 𝑉) 𝑊) = 𝑉)
169157, 168breqtrd 4711 . . . . . . 7 ((𝜑𝑄 𝑊) → 𝑄 𝑉)
17021adantr 480 . . . . . . . 8 ((𝜑𝑄 𝑊) → 𝑉𝐴)
1717, 8atcmp 34916 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑄𝐴𝑉𝐴) → (𝑄 𝑉𝑄 = 𝑉))
172144, 145, 170, 171syl3anc 1366 . . . . . . 7 ((𝜑𝑄 𝑊) → (𝑄 𝑉𝑄 = 𝑉))
173169, 172mpbid 222 . . . . . 6 ((𝜑𝑄 𝑊) → 𝑄 = 𝑉)
174149, 173eqtr3d 2687 . . . . 5 ((𝜑𝑄 𝑊) → 𝑈 = 𝑉)
175174ex 449 . . . 4 (𝜑 → (𝑄 𝑊𝑈 = 𝑉))
176175necon3ad 2836 . . 3 (𝜑 → (𝑈𝑉 → ¬ 𝑄 𝑊))
17765, 176mpd 15 . 2 (𝜑 → ¬ 𝑄 𝑊)
178116, 177jca 553 1 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wne 2823   class class class wbr 4685  cfv 5926  (class class class)co 6690  Basecbs 15904  lecple 15995  joincjn 16991  meetcmee 16992  0.cp0 17084  1.cp1 17085  Latclat 17092  OLcol 34779  Atomscatm 34868  AtLatcal 34869  HLchlt 34955  LHypclh 35588  LTrncltrn 35705  trLctrl 35763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-preset 16975  df-poset 16993  df-plt 17005  df-lub 17021  df-glb 17022  df-join 17023  df-meet 17024  df-p0 17086  df-p1 17087  df-lat 17093  df-clat 17155  df-oposet 34781  df-ol 34783  df-oml 34784  df-covers 34871  df-ats 34872  df-atl 34903  df-cvlat 34927  df-hlat 34956  df-llines 35102  df-psubsp 35107  df-pmap 35108  df-padd 35400  df-lhyp 35592  df-laut 35593  df-ldil 35708  df-ltrn 35709  df-trl 35764
This theorem is referenced by:  dia2dimlem3  36672  dia2dimlem6  36675
  Copyright terms: Public domain W3C validator