Metamath Proof Explorer


Theorem cdlemk39u

Description: Part of proof of Lemma K of Crawley p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by ( UG ) . (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 cdlemk39u K HL W H F T N T R F = R 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 simpr K HL W H F T N T R F = R N G T P A ¬ P ˙ W F = N F = N
14 simpl2r K HL W H F T N T R F = R N G T P A ¬ P ˙ W F = N G T
15 11 12 cdlemk40t F = N G T U G = G
16 13 14 15 syl2anc K HL W H F T N T R F = R N G T P A ¬ P ˙ W F = N U G = G
17 16 fveq2d K HL W H F T N T R F = R N G T P A ¬ P ˙ W F = N R U G = R G
18 simp11l K HL W H F T N T R F = R N G T P A ¬ P ˙ W K HL
19 18 hllatd K HL W H F T N T R F = R N G T P A ¬ P ˙ W K Lat
20 simp11 K HL W H F T N T R F = R N G T P A ¬ P ˙ W K HL W H
21 simp2r K HL W H F T N T R F = R N G T P A ¬ P ˙ W G T
22 1 6 7 8 trlcl K HL W H G T R G B
23 20 21 22 syl2anc K HL W H F T N T R F = R N G T P A ¬ P ˙ W R G B
24 1 2 latref K Lat R G B R G ˙ R G
25 19 23 24 syl2anc K HL W H F T N T R F = R N G T P A ¬ P ˙ W R G ˙ R G
26 25 adantr K HL W H F T N T R F = R N G T P A ¬ P ˙ W F = N R G ˙ R G
27 17 26 eqbrtrd K HL W H F T N T R F = R N G T P A ¬ P ˙ W F = N R U G ˙ R G
28 simpl1 K HL W H F T N T R F = R N G T P A ¬ P ˙ W F N K HL W H F T N T
29 simpl2l K HL W H F T N T R F = R N G T P A ¬ P ˙ W F N R F = R N
30 simpr K HL W H F T N T R F = R N G T P A ¬ P ˙ W F N F N
31 simpl2r K HL W H F T N T R F = R N G T P A ¬ P ˙ W F N G T
32 simpl3 K HL W H F T N T R F = R N G T P A ¬ P ˙ W F N P A ¬ P ˙ W
33 1 2 3 4 5 6 7 8 9 10 11 12 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
34 28 29 30 31 32 33 syl131anc K HL W H F T N T R F = R N G T P A ¬ P ˙ W F N R U G ˙ R G
35 27 34 pm2.61dane K HL W H F T N T R F = R N G T P A ¬ P ˙ W R U G ˙ R G