Metamath Proof Explorer


Theorem cdlemk55u1

Description: Lemma for cdlemk55u . (Contributed by NM, 31-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
cdlemk5.x X = ι z T | b T b I B R b R F R b R g z P = Y
cdlemk5.u U = g T if F = N g X
Assertion cdlemk55u1 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W U G I = U G U I

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 cdlemk5.x X = ι z T | b T b I B R b R F R b R g z P = Y
12 cdlemk5.u U = g T if F = N g X
13 simp11 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W K HL W H
14 simp21l K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W R F = R N
15 simp12 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W F T
16 simp13 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W N T
17 simp21r K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W F N
18 1 6 7 8 trlnid K HL W H F T N T F N R F = R N F I B
19 13 15 16 17 14 18 syl122anc K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W F I B
20 15 19 16 3jca K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W F T F I B N T
21 simp22 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W G T
22 simp23 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W I T
23 simp3 K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W P A ¬ P ˙ W
24 1 2 3 4 5 6 7 8 9 10 11 cdlemk55 K HL W H R F = R N F T F I B N T G T I T P A ¬ P ˙ W G I / g X = G / g X I / g X
25 13 14 20 21 22 23 24 syl231anc K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W G I / g X = G / g X I / g X
26 6 7 ltrnco K HL W H G T I T G I T
27 13 21 22 26 syl3anc K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W G I T
28 11 12 cdlemk40f F N G I T U G I = G I / g X
29 17 27 28 syl2anc K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W U G I = G I / g X
30 11 12 cdlemk40f F N G T U G = G / g X
31 17 21 30 syl2anc K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W U G = G / g X
32 11 12 cdlemk40f F N I T U I = I / g X
33 17 22 32 syl2anc K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W U I = I / g X
34 31 33 coeq12d K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W U G U I = G / g X I / g X
35 25 29 34 3eqtr4d K HL W H F T N T R F = R N F N G T I T P A ¬ P ˙ W U G I = U G U I