Metamath Proof Explorer


Theorem cdlemkid2

Description: Lemma for cdlemkid . (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b B = Base K
cdlemk5.l ˙ = K
cdlemk5.j ˙ = join K
cdlemk5.m ˙ = meet K
cdlemk5.a A = Atoms K
cdlemk5.h H = LHyp K
cdlemk5.t T = LTrn K W
cdlemk5.r R = trL K W
cdlemk5.z Z = P ˙ R b ˙ N P ˙ R b F -1
cdlemk5.y Y = P ˙ R g ˙ Z ˙ R g b -1
Assertion cdlemkid2 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B G / g Y = P

Proof

Step Hyp Ref Expression
1 cdlemk5.b B = Base K
2 cdlemk5.l ˙ = K
3 cdlemk5.j ˙ = join K
4 cdlemk5.m ˙ = meet K
5 cdlemk5.a A = Atoms K
6 cdlemk5.h H = LHyp K
7 cdlemk5.t T = LTrn K W
8 cdlemk5.r R = trL K W
9 cdlemk5.z Z = P ˙ R b ˙ N P ˙ R b F -1
10 cdlemk5.y Y = P ˙ R g ˙ Z ˙ R g b -1
11 simp32 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B G = I B
12 11 csbeq1d K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B G / g Y = I B / g Y
13 1 6 7 idltrn K HL W H I B T
14 13 3ad2ant1 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B I B T
15 10 cdlemk41 I B T I B / g Y = P ˙ R I B ˙ Z ˙ R I B b -1
16 14 15 syl K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B I B / g Y = P ˙ R I B ˙ Z ˙ R I B b -1
17 eqid 0. K = 0. K
18 1 17 6 8 trlid0 K HL W H R I B = 0. K
19 18 3ad2ant1 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R I B = 0. K
20 19 oveq2d K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P ˙ R I B = P ˙ 0. K
21 simp1l K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B K HL
22 hlol K HL K OL
23 21 22 syl K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B K OL
24 simp31l K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P A
25 1 5 atbase P A P B
26 24 25 syl K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P B
27 1 3 17 olj01 K OL P B P ˙ 0. K = P
28 23 26 27 syl2anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P ˙ 0. K = P
29 20 28 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P ˙ R I B = P
30 simp1 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B K HL W H
31 simp33l K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B b T
32 6 7 ltrncnv K HL W H b T b -1 T
33 30 31 32 syl2anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B b -1 T
34 1 6 7 ltrn1o K HL W H b -1 T b -1 : B 1-1 onto B
35 30 33 34 syl2anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B b -1 : B 1-1 onto B
36 f1of b -1 : B 1-1 onto B b -1 : B B
37 fcoi2 b -1 : B B I B b -1 = b -1
38 35 36 37 3syl K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B I B b -1 = b -1
39 38 fveq2d K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R I B b -1 = R b -1
40 6 7 8 trlcnv K HL W H b T R b -1 = R b
41 30 31 40 syl2anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b -1 = R b
42 39 41 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R I B b -1 = R b
43 42 oveq2d K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B Z ˙ R I B b -1 = Z ˙ R b
44 simp31 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P A ¬ P ˙ W
45 simp33 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B b T b I B
46 44 45 jca K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P A ¬ P ˙ W b T b I B
47 1 2 3 4 5 6 7 8 9 cdlemkid1 K HL W H F T N T R F = R N P A ¬ P ˙ W b T b I B Z ˙ R b = P ˙ R b
48 46 47 syld3an3 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B Z ˙ R b = P ˙ R b
49 43 48 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B Z ˙ R I B b -1 = P ˙ R b
50 29 49 oveq12d K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P ˙ R I B ˙ Z ˙ R I B b -1 = P ˙ P ˙ R b
51 21 hllatd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B K Lat
52 1 6 7 8 trlcl K HL W H b T R b B
53 30 31 52 syl2anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b B
54 1 3 4 latabs2 K Lat P B R b B P ˙ P ˙ R b = P
55 51 26 53 54 syl3anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P ˙ P ˙ R b = P
56 50 55 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B P ˙ R I B ˙ Z ˙ R I B b -1 = P
57 16 56 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B I B / g Y = P
58 12 57 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B G / g Y = P