Metamath Proof Explorer


Theorem cdlemk35u

Description: Substitution version of cdlemk35 . (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 cdlemk35u K HL W H R F = R N F T N T G T P A ¬ P ˙ W U G T

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 R F = R N F T N T G T P A ¬ P ˙ W F = N F = N
14 simpl23 K HL W H R F = R N F T N T 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 R F = R N F T N T G T P A ¬ P ˙ W F = N U G = G
17 16 14 eqeltrd K HL W H R F = R N F T N T G T P A ¬ P ˙ W F = N U G T
18 simpr K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N F N
19 simpl23 K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N G T
20 11 12 cdlemk40f F N G T U G = G / g X
21 18 19 20 syl2anc K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N U G = G / g X
22 simpl1l K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N K HL W H
23 simpl21 K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N F T
24 simpl22 K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N N T
25 simpl1r K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N R F = R N
26 1 6 7 8 trlnid K HL W H F T N T F N R F = R N F I B
27 22 23 24 18 25 26 syl122anc K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N F I B
28 23 27 jca K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N F T F I B
29 simpl3 K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N P A ¬ P ˙ W
30 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s-id K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G / g X T
31 22 28 19 24 29 25 30 syl132anc K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N G / g X T
32 21 31 eqeltrd K HL W H R F = R N F T N T G T P A ¬ P ˙ W F N U G T
33 17 32 pm2.61dane K HL W H R F = R N F T N T G T P A ¬ P ˙ W U G T