Metamath Proof Explorer


Theorem cdlemk39s-id

Description: Substitution version of cdlemk39 with non-identity requirement on G removed. TODO: Can any commonality with cdlemk35s be exploited? (Contributed by NM, 26-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
Assertion 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

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 simpl1 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B K HL W H
13 simp21l K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N F T
14 simp23 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N N T
15 simp3r K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N R F = R N
16 13 14 15 3jca K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N F T N T R F = R N
17 16 adantr K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B F T N T R F = R N
18 simpl3l K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B P A ¬ P ˙ W
19 simpr K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B G = I B
20 1 2 3 4 5 6 7 8 9 10 11 cdlemkid K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B G / g X = I B
21 12 17 18 19 20 syl112anc K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B G / g X = I B
22 21 fveq2d K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B R G / g X = R I B
23 simpl1l K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B K HL
24 simpl1r K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B W H
25 eqid 0. K = 0. K
26 1 25 6 8 trlid0 K HL W H R I B = 0. K
27 23 24 26 syl2anc K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B R I B = 0. K
28 22 27 eqtrd K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B R G / g X = 0. K
29 hlop K HL K OP
30 23 29 syl K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B K OP
31 simpl22 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B G T
32 1 6 7 8 trlcl K HL W H G T R G B
33 12 31 32 syl2anc K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B R G B
34 1 2 25 op0le K OP R G B 0. K ˙ R G
35 30 33 34 syl2anc K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B 0. K ˙ R G
36 28 35 eqbrtrd K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G = I B R G / g X ˙ R G
37 simpl1 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B K HL W H
38 simpl21 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B F T F I B
39 simpl22 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B G T
40 simpr K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B G I B
41 39 40 jca K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B G T G I B
42 simpl23 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B N T
43 simpl3 K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B P A ¬ P ˙ W R F = R N
44 1 2 3 4 5 6 7 8 9 10 11 cdlemk39s K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N R G / g X ˙ R G
45 37 38 41 42 43 44 syl131anc K HL W H F T F I B G T N T P A ¬ P ˙ W R F = R N G I B R G / g X ˙ R G
46 36 45 pm2.61dane 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