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

Theorem dia2dimlem2 37679
Description: Lemma for dia2dim 37691. Define a translation 𝐺 whose trace is atom 𝑈. Part of proof of Lemma M in [Crawley] p. 121 line 4. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem2.l = (le‘𝐾)
dia2dimlem2.j = (join‘𝐾)
dia2dimlem2.m = (meet‘𝐾)
dia2dimlem2.a 𝐴 = (Atoms‘𝐾)
dia2dimlem2.h 𝐻 = (LHyp‘𝐾)
dia2dimlem2.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dia2dimlem2.r 𝑅 = ((trL‘𝐾)‘𝑊)
dia2dimlem2.q 𝑄 = ((𝑃 𝑈) ((𝐹𝑃) 𝑉))
dia2dimlem2.k (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
dia2dimlem2.u (𝜑 → (𝑈𝐴𝑈 𝑊))
dia2dimlem2.v (𝜑 → (𝑉𝐴𝑉 𝑊))
dia2dimlem2.p (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
dia2dimlem2.f (𝜑 → (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃))
dia2dimlem2.rf (𝜑 → (𝑅𝐹) (𝑈 𝑉))
dia2dimlem2.rv (𝜑 → (𝑅𝐹) ≠ 𝑉)
dia2dimlem2.g (𝜑𝐺𝑇)
dia2dimlem2.gv (𝜑 → (𝐺𝑃) = 𝑄)
Assertion
Ref Expression
dia2dimlem2 (𝜑 → (𝑅𝐺) = 𝑈)

Proof of Theorem dia2dimlem2
StepHypRef Expression
1 dia2dimlem2.k . . . . . . . . 9 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
21simpld 487 . . . . . . . 8 (𝜑𝐾 ∈ HL)
32hllatd 35978 . . . . . . 7 (𝜑𝐾 ∈ Lat)
4 dia2dimlem2.p . . . . . . . . 9 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
54simpld 487 . . . . . . . 8 (𝜑𝑃𝐴)
6 eqid 2773 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
7 dia2dimlem2.a . . . . . . . . 9 𝐴 = (Atoms‘𝐾)
86, 7atbase 35903 . . . . . . . 8 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
95, 8syl 17 . . . . . . 7 (𝜑𝑃 ∈ (Base‘𝐾))
10 dia2dimlem2.u . . . . . . . . 9 (𝜑 → (𝑈𝐴𝑈 𝑊))
1110simpld 487 . . . . . . . 8 (𝜑𝑈𝐴)
126, 7atbase 35903 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
1311, 12syl 17 . . . . . . 7 (𝜑𝑈 ∈ (Base‘𝐾))
14 dia2dimlem2.l . . . . . . . 8 = (le‘𝐾)
15 dia2dimlem2.j . . . . . . . 8 = (join‘𝐾)
166, 14, 15latlej2 17542 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑈 (𝑃 𝑈))
173, 9, 13, 16syl3anc 1352 . . . . . 6 (𝜑𝑈 (𝑃 𝑈))
186, 15, 7hlatjcl 35981 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
192, 5, 11, 18syl3anc 1352 . . . . . . 7 (𝜑 → (𝑃 𝑈) ∈ (Base‘𝐾))
20 dia2dimlem2.m . . . . . . . 8 = (meet‘𝐾)
216, 14, 20latleeqm2 17561 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾)) → (𝑈 (𝑃 𝑈) ↔ ((𝑃 𝑈) 𝑈) = 𝑈))
223, 13, 19, 21syl3anc 1352 . . . . . 6 (𝜑 → (𝑈 (𝑃 𝑈) ↔ ((𝑃 𝑈) 𝑈) = 𝑈))
2317, 22mpbid 224 . . . . 5 (𝜑 → ((𝑃 𝑈) 𝑈) = 𝑈)
24 dia2dimlem2.rf . . . . . . . 8 (𝜑 → (𝑅𝐹) (𝑈 𝑉))
25 dia2dimlem2.f . . . . . . . . . 10 (𝜑 → (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃))
26 dia2dimlem2.h . . . . . . . . . . 11 𝐻 = (LHyp‘𝐾)
27 dia2dimlem2.t . . . . . . . . . . 11 𝑇 = ((LTrn‘𝐾)‘𝑊)
28 dia2dimlem2.r . . . . . . . . . . 11 𝑅 = ((trL‘𝐾)‘𝑊)
2914, 7, 26, 27, 28trlat 36783 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
301, 4, 25, 29syl3anc 1352 . . . . . . . . 9 (𝜑 → (𝑅𝐹) ∈ 𝐴)
31 dia2dimlem2.v . . . . . . . . . 10 (𝜑 → (𝑉𝐴𝑉 𝑊))
3231simpld 487 . . . . . . . . 9 (𝜑𝑉𝐴)
33 dia2dimlem2.rv . . . . . . . . 9 (𝜑 → (𝑅𝐹) ≠ 𝑉)
3414, 15, 7hlatexch2 36010 . . . . . . . . 9 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑈𝐴𝑉𝐴) ∧ (𝑅𝐹) ≠ 𝑉) → ((𝑅𝐹) (𝑈 𝑉) → 𝑈 ((𝑅𝐹) 𝑉)))
352, 30, 11, 32, 33, 34syl131anc 1364 . . . . . . . 8 (𝜑 → ((𝑅𝐹) (𝑈 𝑉) → 𝑈 ((𝑅𝐹) 𝑉)))
3624, 35mpd 15 . . . . . . 7 (𝜑𝑈 ((𝑅𝐹) 𝑉))
3725simpld 487 . . . . . . . . . 10 (𝜑𝐹𝑇)
3814, 15, 20, 7, 26, 27, 28trlval2 36777 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
391, 37, 4, 38syl3anc 1352 . . . . . . . . 9 (𝜑 → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
4039oveq1d 6990 . . . . . . . 8 (𝜑 → ((𝑅𝐹) 𝑉) = (((𝑃 (𝐹𝑃)) 𝑊) 𝑉))
4114, 7, 26, 27ltrnel 36753 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
421, 37, 4, 41syl3anc 1352 . . . . . . . . . . . 12 (𝜑 → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
4342simpld 487 . . . . . . . . . . 11 (𝜑 → (𝐹𝑃) ∈ 𝐴)
446, 15, 7hlatjcl 35981 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
452, 5, 43, 44syl3anc 1352 . . . . . . . . . 10 (𝜑 → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
461simprd 488 . . . . . . . . . . 11 (𝜑𝑊𝐻)
476, 26lhpbase 36612 . . . . . . . . . . 11 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
4846, 47syl 17 . . . . . . . . . 10 (𝜑𝑊 ∈ (Base‘𝐾))
4931simprd 488 . . . . . . . . . 10 (𝜑𝑉 𝑊)
506, 14, 15, 20, 7atmod4i1 36480 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑉𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 𝑊) → (((𝑃 (𝐹𝑃)) 𝑊) 𝑉) = (((𝑃 (𝐹𝑃)) 𝑉) 𝑊))
512, 32, 45, 48, 49, 50syl131anc 1364 . . . . . . . . 9 (𝜑 → (((𝑃 (𝐹𝑃)) 𝑊) 𝑉) = (((𝑃 (𝐹𝑃)) 𝑉) 𝑊))
5215, 7hlatjass 35984 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴)) → ((𝑃 (𝐹𝑃)) 𝑉) = (𝑃 ((𝐹𝑃) 𝑉)))
532, 5, 43, 32, 52syl13anc 1353 . . . . . . . . . 10 (𝜑 → ((𝑃 (𝐹𝑃)) 𝑉) = (𝑃 ((𝐹𝑃) 𝑉)))
5453oveq1d 6990 . . . . . . . . 9 (𝜑 → (((𝑃 (𝐹𝑃)) 𝑉) 𝑊) = ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊))
5551, 54eqtrd 2809 . . . . . . . 8 (𝜑 → (((𝑃 (𝐹𝑃)) 𝑊) 𝑉) = ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊))
5640, 55eqtrd 2809 . . . . . . 7 (𝜑 → ((𝑅𝐹) 𝑉) = ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊))
5736, 56breqtrd 4952 . . . . . 6 (𝜑𝑈 ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊))
586, 15, 7hlatjcl 35981 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
592, 43, 32, 58syl3anc 1352 . . . . . . . . 9 (𝜑 → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
606, 15latjcl 17532 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) → (𝑃 ((𝐹𝑃) 𝑉)) ∈ (Base‘𝐾))
613, 9, 59, 60syl3anc 1352 . . . . . . . 8 (𝜑 → (𝑃 ((𝐹𝑃) 𝑉)) ∈ (Base‘𝐾))
626, 20latmcl 17533 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ((𝐹𝑃) 𝑉)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊) ∈ (Base‘𝐾))
633, 61, 48, 62syl3anc 1352 . . . . . . 7 (𝜑 → ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊) ∈ (Base‘𝐾))
646, 14, 20latmlem2 17563 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊) ∈ (Base‘𝐾) ∧ (𝑃 𝑈) ∈ (Base‘𝐾))) → (𝑈 ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊) → ((𝑃 𝑈) 𝑈) ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊))))
653, 13, 63, 19, 64syl13anc 1353 . . . . . 6 (𝜑 → (𝑈 ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊) → ((𝑃 𝑈) 𝑈) ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊))))
6657, 65mpd 15 . . . . 5 (𝜑 → ((𝑃 𝑈) 𝑈) ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
6723, 66eqbrtrrd 4950 . . . 4 (𝜑𝑈 ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
68 dia2dimlem2.g . . . . . . 7 (𝜑𝐺𝑇)
6914, 15, 20, 7, 26, 27, 28trlval2 36777 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐺) = ((𝑃 (𝐺𝑃)) 𝑊))
701, 68, 4, 69syl3anc 1352 . . . . . 6 (𝜑 → (𝑅𝐺) = ((𝑃 (𝐺𝑃)) 𝑊))
71 dia2dimlem2.gv . . . . . . . . . 10 (𝜑 → (𝐺𝑃) = 𝑄)
72 dia2dimlem2.q . . . . . . . . . 10 𝑄 = ((𝑃 𝑈) ((𝐹𝑃) 𝑉))
7371, 72syl6eq 2825 . . . . . . . . 9 (𝜑 → (𝐺𝑃) = ((𝑃 𝑈) ((𝐹𝑃) 𝑉)))
7473oveq2d 6991 . . . . . . . 8 (𝜑 → (𝑃 (𝐺𝑃)) = (𝑃 ((𝑃 𝑈) ((𝐹𝑃) 𝑉))))
7574oveq1d 6990 . . . . . . 7 (𝜑 → ((𝑃 (𝐺𝑃)) 𝑊) = ((𝑃 ((𝑃 𝑈) ((𝐹𝑃) 𝑉))) 𝑊))
7614, 15, 7hlatlej1 35989 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → 𝑃 (𝑃 𝑈))
772, 5, 11, 76syl3anc 1352 . . . . . . . . . 10 (𝜑𝑃 (𝑃 𝑈))
786, 14, 15, 20, 7atmod3i1 36478 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴 ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) ∧ 𝑃 (𝑃 𝑈)) → (𝑃 ((𝑃 𝑈) ((𝐹𝑃) 𝑉))) = ((𝑃 𝑈) (𝑃 ((𝐹𝑃) 𝑉))))
792, 5, 19, 59, 77, 78syl131anc 1364 . . . . . . . . 9 (𝜑 → (𝑃 ((𝑃 𝑈) ((𝐹𝑃) 𝑉))) = ((𝑃 𝑈) (𝑃 ((𝐹𝑃) 𝑉))))
8079oveq1d 6990 . . . . . . . 8 (𝜑 → ((𝑃 ((𝑃 𝑈) ((𝐹𝑃) 𝑉))) 𝑊) = (((𝑃 𝑈) (𝑃 ((𝐹𝑃) 𝑉))) 𝑊))
81 hlol 35975 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OL)
822, 81syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ OL)
836, 20latmassOLD 35843 . . . . . . . . 9 ((𝐾 ∈ OL ∧ ((𝑃 𝑈) ∈ (Base‘𝐾) ∧ (𝑃 ((𝐹𝑃) 𝑉)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑃 𝑈) (𝑃 ((𝐹𝑃) 𝑉))) 𝑊) = ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
8482, 19, 61, 48, 83syl13anc 1353 . . . . . . . 8 (𝜑 → (((𝑃 𝑈) (𝑃 ((𝐹𝑃) 𝑉))) 𝑊) = ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
8580, 84eqtrd 2809 . . . . . . 7 (𝜑 → ((𝑃 ((𝑃 𝑈) ((𝐹𝑃) 𝑉))) 𝑊) = ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
8675, 85eqtrd 2809 . . . . . 6 (𝜑 → ((𝑃 (𝐺𝑃)) 𝑊) = ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
8770, 86eqtrd 2809 . . . . 5 (𝜑 → (𝑅𝐺) = ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)))
8887eqcomd 2779 . . . 4 (𝜑 → ((𝑃 𝑈) ((𝑃 ((𝐹𝑃) 𝑉)) 𝑊)) = (𝑅𝐺))
8967, 88breqtrd 4952 . . 3 (𝜑𝑈 (𝑅𝐺))
90 hlatl 35974 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
912, 90syl 17 . . . 4 (𝜑𝐾 ∈ AtLat)
92 hlop 35976 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OP)
932, 92syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ OP)
94 eqid 2773 . . . . . . . . . 10 (0.‘𝐾) = (0.‘𝐾)
95 eqid 2773 . . . . . . . . . 10 (lt‘𝐾) = (lt‘𝐾)
9694, 95, 70ltat 35905 . . . . . . . . 9 ((𝐾 ∈ OP ∧ 𝑈𝐴) → (0.‘𝐾)(lt‘𝐾)𝑈)
9793, 11, 96syl2anc 576 . . . . . . . 8 (𝜑 → (0.‘𝐾)(lt‘𝐾)𝑈)
98 hlpos 35980 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ Poset)
992, 98syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Poset)
1006, 94op0cl 35798 . . . . . . . . . 10 (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
10193, 100syl 17 . . . . . . . . 9 (𝜑 → (0.‘𝐾) ∈ (Base‘𝐾))
1026, 26, 27, 28trlcl 36778 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → (𝑅𝐺) ∈ (Base‘𝐾))
1031, 68, 102syl2anc 576 . . . . . . . . 9 (𝜑 → (𝑅𝐺) ∈ (Base‘𝐾))
1046, 14, 95pltletr 17452 . . . . . . . . 9 ((𝐾 ∈ Poset ∧ ((0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑅𝐺) ∈ (Base‘𝐾))) → (((0.‘𝐾)(lt‘𝐾)𝑈𝑈 (𝑅𝐺)) → (0.‘𝐾)(lt‘𝐾)(𝑅𝐺)))
10599, 101, 13, 103, 104syl13anc 1353 . . . . . . . 8 (𝜑 → (((0.‘𝐾)(lt‘𝐾)𝑈𝑈 (𝑅𝐺)) → (0.‘𝐾)(lt‘𝐾)(𝑅𝐺)))
10697, 89, 105mp2and 687 . . . . . . 7 (𝜑 → (0.‘𝐾)(lt‘𝐾)(𝑅𝐺))
1076, 95, 94opltn0 35804 . . . . . . . 8 ((𝐾 ∈ OP ∧ (𝑅𝐺) ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)(𝑅𝐺) ↔ (𝑅𝐺) ≠ (0.‘𝐾)))
10893, 103, 107syl2anc 576 . . . . . . 7 (𝜑 → ((0.‘𝐾)(lt‘𝐾)(𝑅𝐺) ↔ (𝑅𝐺) ≠ (0.‘𝐾)))
109106, 108mpbid 224 . . . . . 6 (𝜑 → (𝑅𝐺) ≠ (0.‘𝐾))
110109neneqd 2967 . . . . 5 (𝜑 → ¬ (𝑅𝐺) = (0.‘𝐾))
11194, 7, 26, 27, 28trlator0 36785 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → ((𝑅𝐺) ∈ 𝐴 ∨ (𝑅𝐺) = (0.‘𝐾)))
1121, 68, 111syl2anc 576 . . . . . . 7 (𝜑 → ((𝑅𝐺) ∈ 𝐴 ∨ (𝑅𝐺) = (0.‘𝐾)))
113112orcomd 858 . . . . . 6 (𝜑 → ((𝑅𝐺) = (0.‘𝐾) ∨ (𝑅𝐺) ∈ 𝐴))
114113ord 851 . . . . 5 (𝜑 → (¬ (𝑅𝐺) = (0.‘𝐾) → (𝑅𝐺) ∈ 𝐴))
115110, 114mpd 15 . . . 4 (𝜑 → (𝑅𝐺) ∈ 𝐴)
11614, 7atcmp 35925 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑈𝐴 ∧ (𝑅𝐺) ∈ 𝐴) → (𝑈 (𝑅𝐺) ↔ 𝑈 = (𝑅𝐺)))
11791, 11, 115, 116syl3anc 1352 . . 3 (𝜑 → (𝑈 (𝑅𝐺) ↔ 𝑈 = (𝑅𝐺)))
11889, 117mpbid 224 . 2 (𝜑𝑈 = (𝑅𝐺))
119118eqcomd 2779 1 (𝜑 → (𝑅𝐺) = 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 834   = wceq 1508  wcel 2051  wne 2962   class class class wbr 4926  cfv 6186  (class class class)co 6975  Basecbs 16338  lecple 16427  Posetcpo 17421  ltcplt 17422  joincjn 17425  meetcmee 17426  0.cp0 17518  Latclat 17526  OPcops 35786  OLcol 35788  Atomscatm 35877  AtLatcal 35878  HLchlt 35964  LHypclh 36598  LTrncltrn 36715  trLctrl 36772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-1st 7500  df-2nd 7501  df-map 8207  df-proset 17409  df-poset 17427  df-plt 17439  df-lub 17455  df-glb 17456  df-join 17457  df-meet 17458  df-p0 17520  df-p1 17521  df-lat 17527  df-clat 17589  df-oposet 35790  df-ol 35792  df-oml 35793  df-covers 35880  df-ats 35881  df-atl 35912  df-cvlat 35936  df-hlat 35965  df-psubsp 36117  df-pmap 36118  df-padd 36410  df-lhyp 36602  df-laut 36603  df-ldil 36718  df-ltrn 36719  df-trl 36773
This theorem is referenced by:  dia2dimlem5  37682
  Copyright terms: Public domain W3C validator