Metamath Proof Explorer


Theorem cdlemkid3N

Description: Lemma for cdlemkid . (Contributed by NM, 25-Jul-2013) (New usage is discouraged.)

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 cdlemkid3N K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B G / g X = ι z T | b T b I B R b R F R b R G z P = P

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 simp3r K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B G = I B
13 1 6 7 idltrn K HL W H I B T
14 13 3ad2ant1 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B I B T
15 12 14 eqeltrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B G T
16 11 csbeq2i G / g X = G / g ι z T | b T b I B R b R F R b R g z P = Y
17 csbriota G / g ι z T | b T b I B R b R F R b R g z P = Y = ι z T | [˙G / g]˙ b T b I B R b R F R b R g z P = Y
18 17 a1i G T G / g ι z T | b T b I B R b R F R b R g z P = Y = ι z T | [˙G / g]˙ b T b I B R b R F R b R g z P = Y
19 16 18 syl5eq G T G / g X = ι z T | [˙G / g]˙ b T b I B R b R F R b R g z P = Y
20 sbcralg G T [˙G / g]˙ b T b I B R b R F R b R g z P = Y b T [˙G / g]˙ b I B R b R F R b R g z P = Y
21 sbcimg G T [˙G / g]˙ b I B R b R F R b R g z P = Y [˙G / g]˙ b I B R b R F R b R g [˙G / g]˙ z P = Y
22 sbc3an [˙G / g]˙ b I B R b R F R b R g [˙G / g]˙ b I B [˙G / g]˙ R b R F [˙G / g]˙ R b R g
23 sbcg G T [˙G / g]˙ b I B b I B
24 sbcg G T [˙G / g]˙ R b R F R b R F
25 sbcne12 [˙G / g]˙ R b R g G / g R b G / g R g
26 csbconstg G T G / g R b = R b
27 csbfv G / g R g = R G
28 27 a1i G T G / g R g = R G
29 26 28 neeq12d G T G / g R b G / g R g R b R G
30 25 29 syl5bb G T [˙G / g]˙ R b R g R b R G
31 23 24 30 3anbi123d G T [˙G / g]˙ b I B [˙G / g]˙ R b R F [˙G / g]˙ R b R g b I B R b R F R b R G
32 22 31 syl5bb G T [˙G / g]˙ b I B R b R F R b R g b I B R b R F R b R G
33 sbceq2g G T [˙G / g]˙ z P = Y z P = G / g Y
34 32 33 imbi12d G T [˙G / g]˙ b I B R b R F R b R g [˙G / g]˙ z P = Y b I B R b R F R b R G z P = G / g Y
35 21 34 bitrd G T [˙G / g]˙ b I B R b R F R b R g z P = Y b I B R b R F R b R G z P = G / g Y
36 35 ralbidv G T b T [˙G / g]˙ b I B R b R F R b R g z P = Y b T b I B R b R F R b R G z P = G / g Y
37 20 36 bitrd G T [˙G / g]˙ b T b I B R b R F R b R g z P = Y b T b I B R b R F R b R G z P = G / g Y
38 37 riotabidv G T ι z T | [˙G / g]˙ b T b I B R b R F R b R g z P = Y = ι z T | b T b I B R b R F R b R G z P = G / g Y
39 19 38 eqtrd G T G / g X = ι z T | b T b I B R b R F R b R G z P = G / g Y
40 15 39 syl K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B G / g X = ι z T | b T b I B R b R F R b R G z P = G / g Y
41 simp11 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G K HL W H
42 simp12 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G F T N T R F = R N
43 simp13l K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G P A ¬ P ˙ W
44 simp13r K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G G = I B
45 simp2 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G b T
46 simp31 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G b I B
47 45 46 jca K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G b T b I B
48 1 2 3 4 5 6 7 8 9 10 cdlemkid2 K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B G / g Y = P
49 41 42 43 44 47 48 syl113anc K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G G / g Y = P
50 49 3expa K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G G / g Y = P
51 50 eqeq2d K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G z P = G / g Y z P = P
52 51 pm5.74da K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G z P = G / g Y b I B R b R F R b R G z P = P
53 52 ralbidva K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B b T b I B R b R F R b R G z P = G / g Y b T b I B R b R F R b R G z P = P
54 53 riotabidv K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B ι z T | b T b I B R b R F R b R G z P = G / g Y = ι z T | b T b I B R b R F R b R G z P = P
55 40 54 eqtrd K HL W H F T N T R F = R N P A ¬ P ˙ W G = I B G / g X = ι z T | b T b I B R b R F R b R G z P = P