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

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

Proof of Theorem dia2dimlem3
StepHypRef Expression
1 dia2dimlem3.k . . . . . . 7 (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))
21simpld 476 . . . . . 6 (𝜑𝐾 ∈ HL)
3 dia2dimlem3.f . . . . . . . . 9 (𝜑 → (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃))
43simpld 476 . . . . . . . 8 (𝜑𝐹𝑇)
5 dia2dimlem3.p . . . . . . . 8 (𝜑 → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
6 dia2dimlem3.l . . . . . . . . 9 = (le‘𝐾)
7 dia2dimlem3.a . . . . . . . . 9 𝐴 = (Atoms‘𝐾)
8 dia2dimlem3.h . . . . . . . . 9 𝐻 = (LHyp‘𝐾)
9 dia2dimlem3.t . . . . . . . . 9 𝑇 = ((LTrn‘𝐾)‘𝑊)
106, 7, 8, 9ltrnel 35940 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
111, 4, 5, 10syl3anc 1475 . . . . . . 7 (𝜑 → ((𝐹𝑃) ∈ 𝐴 ∧ ¬ (𝐹𝑃) 𝑊))
1211simpld 476 . . . . . 6 (𝜑 → (𝐹𝑃) ∈ 𝐴)
13 dia2dimlem3.v . . . . . . 7 (𝜑 → (𝑉𝐴𝑉 𝑊))
1413simpld 476 . . . . . 6 (𝜑𝑉𝐴)
15 dia2dimlem3.j . . . . . . 7 = (join‘𝐾)
166, 15, 7hlatlej2 35177 . . . . . 6 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → 𝑉 ((𝐹𝑃) 𝑉))
172, 12, 14, 16syl3anc 1475 . . . . 5 (𝜑𝑉 ((𝐹𝑃) 𝑉))
18 hllat 35165 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ Lat)
192, 18syl 17 . . . . . 6 (𝜑𝐾 ∈ Lat)
20 eqid 2770 . . . . . . . 8 (Base‘𝐾) = (Base‘𝐾)
2120, 7atbase 35091 . . . . . . 7 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
2214, 21syl 17 . . . . . 6 (𝜑𝑉 ∈ (Base‘𝐾))
2320, 15, 7hlatjcl 35168 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
242, 12, 14, 23syl3anc 1475 . . . . . 6 (𝜑 → ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾))
25 dia2dimlem3.r . . . . . . . . 9 𝑅 = ((trL‘𝐾)‘𝑊)
266, 7, 8, 9, 25trlat 35971 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝐹𝑇 ∧ (𝐹𝑃) ≠ 𝑃)) → (𝑅𝐹) ∈ 𝐴)
271, 5, 3, 26syl3anc 1475 . . . . . . 7 (𝜑 → (𝑅𝐹) ∈ 𝐴)
28 dia2dimlem3.u . . . . . . . 8 (𝜑 → (𝑈𝐴𝑈 𝑊))
2928simpld 476 . . . . . . 7 (𝜑𝑈𝐴)
3020, 15, 7hlatjcl 35168 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑅𝐹) ∈ 𝐴𝑈𝐴) → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
312, 27, 29, 30syl3anc 1475 . . . . . 6 (𝜑 → ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))
32 dia2dimlem3.m . . . . . . 7 = (meet‘𝐾)
3320, 6, 32latmlem2 17289 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾) ∧ ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾))) → (𝑉 ((𝐹𝑃) 𝑉) → (((𝑅𝐹) 𝑈) 𝑉) (((𝑅𝐹) 𝑈) ((𝐹𝑃) 𝑉))))
3419, 22, 24, 31, 33syl13anc 1477 . . . . 5 (𝜑 → (𝑉 ((𝐹𝑃) 𝑉) → (((𝑅𝐹) 𝑈) 𝑉) (((𝑅𝐹) 𝑈) ((𝐹𝑃) 𝑉))))
3517, 34mpd 15 . . . 4 (𝜑 → (((𝑅𝐹) 𝑈) 𝑉) (((𝑅𝐹) 𝑈) ((𝐹𝑃) 𝑉)))
36 dia2dimlem3.rf . . . . . . 7 (𝜑 → (𝑅𝐹) (𝑈 𝑉))
3715, 7hlatjcom 35169 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑈𝐴𝑉𝐴) → (𝑈 𝑉) = (𝑉 𝑈))
382, 29, 14, 37syl3anc 1475 . . . . . . 7 (𝜑 → (𝑈 𝑉) = (𝑉 𝑈))
3936, 38breqtrd 4810 . . . . . 6 (𝜑 → (𝑅𝐹) (𝑉 𝑈))
40 dia2dimlem3.ru . . . . . . 7 (𝜑 → (𝑅𝐹) ≠ 𝑈)
416, 15, 7hlatexch2 35197 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝑅𝐹) ∈ 𝐴𝑉𝐴𝑈𝐴) ∧ (𝑅𝐹) ≠ 𝑈) → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
422, 27, 14, 29, 40, 41syl131anc 1488 . . . . . 6 (𝜑 → ((𝑅𝐹) (𝑉 𝑈) → 𝑉 ((𝑅𝐹) 𝑈)))
4339, 42mpd 15 . . . . 5 (𝜑𝑉 ((𝑅𝐹) 𝑈))
4420, 6, 32latleeqm2 17287 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑉 ∈ (Base‘𝐾) ∧ ((𝑅𝐹) 𝑈) ∈ (Base‘𝐾)) → (𝑉 ((𝑅𝐹) 𝑈) ↔ (((𝑅𝐹) 𝑈) 𝑉) = 𝑉))
4519, 22, 31, 44syl3anc 1475 . . . . 5 (𝜑 → (𝑉 ((𝑅𝐹) 𝑈) ↔ (((𝑅𝐹) 𝑈) 𝑉) = 𝑉))
4643, 45mpbid 222 . . . 4 (𝜑 → (((𝑅𝐹) 𝑈) 𝑉) = 𝑉)
47 dia2dimlem3.d . . . . . 6 (𝜑𝐷𝑇)
48 dia2dimlem3.q . . . . . . 7 𝑄 = ((𝑃 𝑈) ((𝐹𝑃) 𝑉))
49 dia2dimlem3.uv . . . . . . 7 (𝜑𝑈𝑉)
506, 15, 32, 7, 8, 9, 25, 48, 1, 28, 13, 5, 3, 36, 49, 40dia2dimlem1 36867 . . . . . 6 (𝜑 → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
516, 15, 32, 7, 8, 9, 25trlval2 35965 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐷𝑇 ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝑅𝐷) = ((𝑄 (𝐷𝑄)) 𝑊))
521, 47, 50, 51syl3anc 1475 . . . . 5 (𝜑 → (𝑅𝐷) = ((𝑄 (𝐷𝑄)) 𝑊))
5348a1i 11 . . . . . . . . 9 (𝜑𝑄 = ((𝑃 𝑈) ((𝐹𝑃) 𝑉)))
54 dia2dimlem3.dv . . . . . . . . 9 (𝜑 → (𝐷𝑄) = (𝐹𝑃))
5553, 54oveq12d 6810 . . . . . . . 8 (𝜑 → (𝑄 (𝐷𝑄)) = (((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝐹𝑃)))
565simpld 476 . . . . . . . . . 10 (𝜑𝑃𝐴)
5720, 15, 7hlatjcl 35168 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) → (𝑃 𝑈) ∈ (Base‘𝐾))
582, 56, 29, 57syl3anc 1475 . . . . . . . . 9 (𝜑 → (𝑃 𝑈) ∈ (Base‘𝐾))
596, 15, 7hlatlej1 35176 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝐹𝑃) ∈ 𝐴𝑉𝐴) → (𝐹𝑃) ((𝐹𝑃) 𝑉))
602, 12, 14, 59syl3anc 1475 . . . . . . . . 9 (𝜑 → (𝐹𝑃) ((𝐹𝑃) 𝑉))
6120, 6, 15, 32, 7atmod4i1 35667 . . . . . . . . 9 ((𝐾 ∈ HL ∧ ((𝐹𝑃) ∈ 𝐴 ∧ (𝑃 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾)) ∧ (𝐹𝑃) ((𝐹𝑃) 𝑉)) → (((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝐹𝑃)) = (((𝑃 𝑈) (𝐹𝑃)) ((𝐹𝑃) 𝑉)))
622, 12, 58, 24, 60, 61syl131anc 1488 . . . . . . . 8 (𝜑 → (((𝑃 𝑈) ((𝐹𝑃) 𝑉)) (𝐹𝑃)) = (((𝑃 𝑈) (𝐹𝑃)) ((𝐹𝑃) 𝑉)))
6315, 7hlatj32 35173 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑈𝐴 ∧ (𝐹𝑃) ∈ 𝐴)) → ((𝑃 𝑈) (𝐹𝑃)) = ((𝑃 (𝐹𝑃)) 𝑈))
642, 56, 29, 12, 63syl13anc 1477 . . . . . . . . 9 (𝜑 → ((𝑃 𝑈) (𝐹𝑃)) = ((𝑃 (𝐹𝑃)) 𝑈))
6564oveq1d 6807 . . . . . . . 8 (𝜑 → (((𝑃 𝑈) (𝐹𝑃)) ((𝐹𝑃) 𝑉)) = (((𝑃 (𝐹𝑃)) 𝑈) ((𝐹𝑃) 𝑉)))
6655, 62, 653eqtrd 2808 . . . . . . 7 (𝜑 → (𝑄 (𝐷𝑄)) = (((𝑃 (𝐹𝑃)) 𝑈) ((𝐹𝑃) 𝑉)))
6766oveq1d 6807 . . . . . 6 (𝜑 → ((𝑄 (𝐷𝑄)) 𝑊) = ((((𝑃 (𝐹𝑃)) 𝑈) ((𝐹𝑃) 𝑉)) 𝑊))
68 hlol 35163 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OL)
692, 68syl 17 . . . . . . 7 (𝜑𝐾 ∈ OL)
7020, 15, 7hlatjcl 35168 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐹𝑃) ∈ 𝐴) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
712, 56, 12, 70syl3anc 1475 . . . . . . . 8 (𝜑 → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
7220, 7atbase 35091 . . . . . . . . 9 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
7329, 72syl 17 . . . . . . . 8 (𝜑𝑈 ∈ (Base‘𝐾))
7420, 15latjcl 17258 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) 𝑈) ∈ (Base‘𝐾))
7519, 71, 73, 74syl3anc 1475 . . . . . . 7 (𝜑 → ((𝑃 (𝐹𝑃)) 𝑈) ∈ (Base‘𝐾))
761simprd 477 . . . . . . . 8 (𝜑𝑊𝐻)
7720, 8lhpbase 35799 . . . . . . . 8 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
7876, 77syl 17 . . . . . . 7 (𝜑𝑊 ∈ (Base‘𝐾))
7920, 32latm32 35033 . . . . . . 7 ((𝐾 ∈ OL ∧ (((𝑃 (𝐹𝑃)) 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹𝑃) 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 (𝐹𝑃)) 𝑈) ((𝐹𝑃) 𝑉)) 𝑊) = ((((𝑃 (𝐹𝑃)) 𝑈) 𝑊) ((𝐹𝑃) 𝑉)))
8069, 75, 24, 78, 79syl13anc 1477 . . . . . 6 (𝜑 → ((((𝑃 (𝐹𝑃)) 𝑈) ((𝐹𝑃) 𝑉)) 𝑊) = ((((𝑃 (𝐹𝑃)) 𝑈) 𝑊) ((𝐹𝑃) 𝑉)))
816, 15, 32, 7, 8, 9, 25trlval2 35965 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
821, 4, 5, 81syl3anc 1475 . . . . . . . . 9 (𝜑 → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
8382oveq1d 6807 . . . . . . . 8 (𝜑 → ((𝑅𝐹) 𝑈) = (((𝑃 (𝐹𝑃)) 𝑊) 𝑈))
8428simprd 477 . . . . . . . . 9 (𝜑𝑈 𝑊)
8520, 6, 15, 32, 7atmod4i1 35667 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (𝑈𝐴 ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 𝑊) → (((𝑃 (𝐹𝑃)) 𝑊) 𝑈) = (((𝑃 (𝐹𝑃)) 𝑈) 𝑊))
862, 29, 71, 78, 84, 85syl131anc 1488 . . . . . . . 8 (𝜑 → (((𝑃 (𝐹𝑃)) 𝑊) 𝑈) = (((𝑃 (𝐹𝑃)) 𝑈) 𝑊))
8783, 86eqtr2d 2805 . . . . . . 7 (𝜑 → (((𝑃 (𝐹𝑃)) 𝑈) 𝑊) = ((𝑅𝐹) 𝑈))
8887oveq1d 6807 . . . . . 6 (𝜑 → ((((𝑃 (𝐹𝑃)) 𝑈) 𝑊) ((𝐹𝑃) 𝑉)) = (((𝑅𝐹) 𝑈) ((𝐹𝑃) 𝑉)))
8967, 80, 883eqtrd 2808 . . . . 5 (𝜑 → ((𝑄 (𝐷𝑄)) 𝑊) = (((𝑅𝐹) 𝑈) ((𝐹𝑃) 𝑉)))
9052, 89eqtr2d 2805 . . . 4 (𝜑 → (((𝑅𝐹) 𝑈) ((𝐹𝑃) 𝑉)) = (𝑅𝐷))
9135, 46, 903brtr3d 4815 . . 3 (𝜑𝑉 (𝑅𝐷))
92 hlatl 35162 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
932, 92syl 17 . . . 4 (𝜑𝐾 ∈ AtLat)
94 hlop 35164 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OP)
952, 94syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ OP)
96 eqid 2770 . . . . . . . . . 10 (0.‘𝐾) = (0.‘𝐾)
97 eqid 2770 . . . . . . . . . 10 (lt‘𝐾) = (lt‘𝐾)
9896, 97, 70ltat 35093 . . . . . . . . 9 ((𝐾 ∈ OP ∧ 𝑉𝐴) → (0.‘𝐾)(lt‘𝐾)𝑉)
9995, 14, 98syl2anc 565 . . . . . . . 8 (𝜑 → (0.‘𝐾)(lt‘𝐾)𝑉)
100 hlpos 35167 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ Poset)
1012, 100syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Poset)
10220, 96op0cl 34986 . . . . . . . . . 10 (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
10395, 102syl 17 . . . . . . . . 9 (𝜑 → (0.‘𝐾) ∈ (Base‘𝐾))
10420, 8, 9, 25trlcl 35966 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐷𝑇) → (𝑅𝐷) ∈ (Base‘𝐾))
1051, 47, 104syl2anc 565 . . . . . . . . 9 (𝜑 → (𝑅𝐷) ∈ (Base‘𝐾))
10620, 6, 97pltletr 17178 . . . . . . . . 9 ((𝐾 ∈ Poset ∧ ((0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ (𝑅𝐷) ∈ (Base‘𝐾))) → (((0.‘𝐾)(lt‘𝐾)𝑉𝑉 (𝑅𝐷)) → (0.‘𝐾)(lt‘𝐾)(𝑅𝐷)))
107101, 103, 22, 105, 106syl13anc 1477 . . . . . . . 8 (𝜑 → (((0.‘𝐾)(lt‘𝐾)𝑉𝑉 (𝑅𝐷)) → (0.‘𝐾)(lt‘𝐾)(𝑅𝐷)))
10899, 91, 107mp2and 671 . . . . . . 7 (𝜑 → (0.‘𝐾)(lt‘𝐾)(𝑅𝐷))
10920, 97, 96opltn0 34992 . . . . . . . 8 ((𝐾 ∈ OP ∧ (𝑅𝐷) ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)(𝑅𝐷) ↔ (𝑅𝐷) ≠ (0.‘𝐾)))
11095, 105, 109syl2anc 565 . . . . . . 7 (𝜑 → ((0.‘𝐾)(lt‘𝐾)(𝑅𝐷) ↔ (𝑅𝐷) ≠ (0.‘𝐾)))
111108, 110mpbid 222 . . . . . 6 (𝜑 → (𝑅𝐷) ≠ (0.‘𝐾))
112111neneqd 2947 . . . . 5 (𝜑 → ¬ (𝑅𝐷) = (0.‘𝐾))
11396, 7, 8, 9, 25trlator0 35973 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐷𝑇) → ((𝑅𝐷) ∈ 𝐴 ∨ (𝑅𝐷) = (0.‘𝐾)))
1141, 47, 113syl2anc 565 . . . . . . 7 (𝜑 → ((𝑅𝐷) ∈ 𝐴 ∨ (𝑅𝐷) = (0.‘𝐾)))
115114orcomd 851 . . . . . 6 (𝜑 → ((𝑅𝐷) = (0.‘𝐾) ∨ (𝑅𝐷) ∈ 𝐴))
116115ord 844 . . . . 5 (𝜑 → (¬ (𝑅𝐷) = (0.‘𝐾) → (𝑅𝐷) ∈ 𝐴))
117112, 116mpd 15 . . . 4 (𝜑 → (𝑅𝐷) ∈ 𝐴)
1186, 7atcmp 35113 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑉𝐴 ∧ (𝑅𝐷) ∈ 𝐴) → (𝑉 (𝑅𝐷) ↔ 𝑉 = (𝑅𝐷)))
11993, 14, 117, 118syl3anc 1475 . . 3 (𝜑 → (𝑉 (𝑅𝐷) ↔ 𝑉 = (𝑅𝐷)))
12091, 119mpbid 222 . 2 (𝜑𝑉 = (𝑅𝐷))
121120eqcomd 2776 1 (𝜑 → (𝑅𝐷) = 𝑉)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826   = wceq 1630  wcel 2144  wne 2942   class class class wbr 4784  cfv 6031  (class class class)co 6792  Basecbs 16063  lecple 16155  Posetcpo 17147  ltcplt 17148  joincjn 17151  meetcmee 17152  0.cp0 17244  Latclat 17252  OPcops 34974  OLcol 34976  Atomscatm 35065  AtLatcal 35066  HLchlt 35152  LHypclh 35785  LTrncltrn 35902  trLctrl 35960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-iun 4654  df-iin 4655  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-1st 7314  df-2nd 7315  df-map 8010  df-preset 17135  df-poset 17153  df-plt 17165  df-lub 17181  df-glb 17182  df-join 17183  df-meet 17184  df-p0 17246  df-p1 17247  df-lat 17253  df-clat 17315  df-oposet 34978  df-ol 34980  df-oml 34981  df-covers 35068  df-ats 35069  df-atl 35100  df-cvlat 35124  df-hlat 35153  df-llines 35299  df-psubsp 35304  df-pmap 35305  df-padd 35597  df-lhyp 35789  df-laut 35790  df-ldil 35905  df-ltrn 35906  df-trl 35961
This theorem is referenced by:  dia2dimlem5  36871
  Copyright terms: Public domain W3C validator