Metamath Proof Explorer


Theorem cdlemk39u1

Description: Lemma for cdlemk39u . (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 cdlemk39u1 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W R U G ˙ R G

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 simp22 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W F N
14 simp23 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W G T
15 11 12 cdlemk40f F N G T U G = G / g X
16 13 14 15 syl2anc K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W U G = G / g X
17 16 fveq2d K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W R U G = R G / g X
18 simp11 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W K HL W H
19 simp12 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W F T
20 simp13 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W N T
21 simp21 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W R F = R N
22 1 6 7 8 trlnid K HL W H F T N T F N R F = R N F I B
23 18 19 20 13 21 22 syl122anc K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W F I B
24 19 23 jca K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W F T F I B
25 simp3 K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W P A ¬ P ˙ W
26 1 2 3 4 5 6 7 8 9 10 11 cdlemk39s-id K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N R G / g X ˙ R G
27 18 24 14 20 25 21 26 syl132anc K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W R G / g X ˙ R G
28 17 27 eqbrtrd K HL W H F T N T R F = R N F N G T P A ¬ P ˙ W R U G ˙ R G