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

Theorem cdlemkid2 40334
Description: Lemma for cdlemkid 40346. (Contributed by NM, 24-Jul-2013.)
Hypotheses
Ref Expression
cdlemk5.b 𝐵 = (Base‘𝐾)
cdlemk5.l = (le‘𝐾)
cdlemk5.j = (join‘𝐾)
cdlemk5.m = (meet‘𝐾)
cdlemk5.a 𝐴 = (Atoms‘𝐾)
cdlemk5.h 𝐻 = (LHyp‘𝐾)
cdlemk5.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk5.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk5.z 𝑍 = ((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹))))
cdlemk5.y 𝑌 = ((𝑃 (𝑅𝑔)) (𝑍 (𝑅‘(𝑔𝑏))))
Assertion
Ref Expression
cdlemkid2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐺 / 𝑔𝑌 = 𝑃)
Distinct variable groups:   ,𝑔   ,𝑔   𝐵,𝑔   𝑃,𝑔   𝑅,𝑔   𝑇,𝑔   𝑔,𝑍   𝑔,𝑏
Allowed substitution hints:   𝐴(𝑔,𝑏)   𝐵(𝑏)   𝑃(𝑏)   𝑅(𝑏)   𝑇(𝑏)   𝐹(𝑔,𝑏)   𝐺(𝑔,𝑏)   𝐻(𝑔,𝑏)   (𝑏)   𝐾(𝑔,𝑏)   (𝑔,𝑏)   (𝑏)   𝑁(𝑔,𝑏)   𝑊(𝑔,𝑏)   𝑌(𝑔,𝑏)   𝑍(𝑏)

Proof of Theorem cdlemkid2
StepHypRef Expression
1 simp32 1208 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐺 = ( I ↾ 𝐵))
21csbeq1d 3893 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐺 / 𝑔𝑌 = ( I ↾ 𝐵) / 𝑔𝑌)
3 cdlemk5.b . . . . . 6 𝐵 = (Base‘𝐾)
4 cdlemk5.h . . . . . 6 𝐻 = (LHyp‘𝐾)
5 cdlemk5.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
63, 4, 5idltrn 39560 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( I ↾ 𝐵) ∈ 𝑇)
763ad2ant1 1131 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ( I ↾ 𝐵) ∈ 𝑇)
8 cdlemk5.y . . . . 5 𝑌 = ((𝑃 (𝑅𝑔)) (𝑍 (𝑅‘(𝑔𝑏))))
98cdlemk41 40330 . . . 4 (( I ↾ 𝐵) ∈ 𝑇( I ↾ 𝐵) / 𝑔𝑌 = ((𝑃 (𝑅‘( I ↾ 𝐵))) (𝑍 (𝑅‘(( I ↾ 𝐵) ∘ 𝑏)))))
107, 9syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ( I ↾ 𝐵) / 𝑔𝑌 = ((𝑃 (𝑅‘( I ↾ 𝐵))) (𝑍 (𝑅‘(( I ↾ 𝐵) ∘ 𝑏)))))
11 eqid 2727 . . . . . . . . 9 (0.‘𝐾) = (0.‘𝐾)
12 cdlemk5.r . . . . . . . . 9 𝑅 = ((trL‘𝐾)‘𝑊)
133, 11, 4, 12trlid0 39586 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾))
14133ad2ant1 1131 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾))
1514oveq2d 7430 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 (𝑅‘( I ↾ 𝐵))) = (𝑃 (0.‘𝐾)))
16 simp1l 1195 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL)
17 hlol 38770 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OL)
1816, 17syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ OL)
19 simp31l 1294 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃𝐴)
20 cdlemk5.a . . . . . . . . 9 𝐴 = (Atoms‘𝐾)
213, 20atbase 38698 . . . . . . . 8 (𝑃𝐴𝑃𝐵)
2219, 21syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃𝐵)
23 cdlemk5.j . . . . . . . 8 = (join‘𝐾)
243, 23, 11olj01 38634 . . . . . . 7 ((𝐾 ∈ OL ∧ 𝑃𝐵) → (𝑃 (0.‘𝐾)) = 𝑃)
2518, 22, 24syl2anc 583 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 (0.‘𝐾)) = 𝑃)
2615, 25eqtrd 2767 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 (𝑅‘( I ↾ 𝐵))) = 𝑃)
27 simp1 1134 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
28 simp33l 1298 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏𝑇)
294, 5ltrncnv 39556 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇) → 𝑏𝑇)
3027, 28, 29syl2anc 583 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏𝑇)
313, 4, 5ltrn1o 39534 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇) → 𝑏:𝐵1-1-onto𝐵)
3227, 30, 31syl2anc 583 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏:𝐵1-1-onto𝐵)
33 f1of 6833 . . . . . . . . . 10 (𝑏:𝐵1-1-onto𝐵𝑏:𝐵𝐵)
34 fcoi2 6766 . . . . . . . . . 10 (𝑏:𝐵𝐵 → (( I ↾ 𝐵) ∘ 𝑏) = 𝑏)
3532, 33, 343syl 18 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (( I ↾ 𝐵) ∘ 𝑏) = 𝑏)
3635fveq2d 6895 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(( I ↾ 𝐵) ∘ 𝑏)) = (𝑅𝑏))
374, 5, 12trlcnv 39575 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇) → (𝑅𝑏) = (𝑅𝑏))
3827, 28, 37syl2anc 583 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝑏) = (𝑅𝑏))
3936, 38eqtrd 2767 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(( I ↾ 𝐵) ∘ 𝑏)) = (𝑅𝑏))
4039oveq2d 7430 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 (𝑅‘(( I ↾ 𝐵) ∘ 𝑏))) = (𝑍 (𝑅𝑏)))
41 simp31 1207 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
42 simp33 1209 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))
4341, 42jca 511 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵))))
44 cdlemk5.l . . . . . . . 8 = (le‘𝐾)
45 cdlemk5.m . . . . . . . 8 = (meet‘𝐾)
46 cdlemk5.z . . . . . . . 8 𝑍 = ((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹))))
473, 44, 23, 45, 20, 4, 5, 12, 46cdlemkid1 40332 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 (𝑅𝑏)) = (𝑃 (𝑅𝑏)))
4843, 47syld3an3 1407 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 (𝑅𝑏)) = (𝑃 (𝑅𝑏)))
4940, 48eqtrd 2767 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 (𝑅‘(( I ↾ 𝐵) ∘ 𝑏))) = (𝑃 (𝑅𝑏)))
5026, 49oveq12d 7432 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅‘( I ↾ 𝐵))) (𝑍 (𝑅‘(( I ↾ 𝐵) ∘ 𝑏)))) = (𝑃 (𝑃 (𝑅𝑏))))
5116hllatd 38773 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat)
523, 4, 5, 12trlcl 39574 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇) → (𝑅𝑏) ∈ 𝐵)
5327, 28, 52syl2anc 583 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝑏) ∈ 𝐵)
543, 23, 45latabs2 18459 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ (𝑅𝑏) ∈ 𝐵) → (𝑃 (𝑃 (𝑅𝑏))) = 𝑃)
5551, 22, 53, 54syl3anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 (𝑃 (𝑅𝑏))) = 𝑃)
5650, 55eqtrd 2767 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅‘( I ↾ 𝐵))) (𝑍 (𝑅‘(( I ↾ 𝐵) ∘ 𝑏)))) = 𝑃)
5710, 56eqtrd 2767 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ( I ↾ 𝐵) / 𝑔𝑌 = 𝑃)
582, 57eqtrd 2767 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐺 / 𝑔𝑌 = 𝑃)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2935  csb 3889   class class class wbr 5142   I cid 5569  ccnv 5671  cres 5674  ccom 5676  wf 6538  1-1-ontowf1o 6541  cfv 6542  (class class class)co 7414  Basecbs 17171  lecple 17231  joincjn 18294  meetcmee 18295  0.cp0 18406  Latclat 18414  OLcol 38583  Atomscatm 38672  HLchlt 38759  LHypclh 39394  LTrncltrn 39511  trLctrl 39568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-riotaBAD 38362
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-undef 8272  df-map 8838  df-proset 18278  df-poset 18296  df-plt 18313  df-lub 18329  df-glb 18330  df-join 18331  df-meet 18332  df-p0 18408  df-p1 18409  df-lat 18415  df-clat 18482  df-oposet 38585  df-ol 38587  df-oml 38588  df-covers 38675  df-ats 38676  df-atl 38707  df-cvlat 38731  df-hlat 38760  df-llines 38908  df-lplanes 38909  df-lvols 38910  df-lines 38911  df-psubsp 38913  df-pmap 38914  df-padd 39206  df-lhyp 39398  df-laut 39399  df-ldil 39514  df-ltrn 39515  df-trl 39569
This theorem is referenced by:  cdlemkid3N  40343  cdlemkid4  40344
  Copyright terms: Public domain W3C validator