Metamath Proof Explorer


Theorem cdlemk55a

Description: Lemma for cdlemk55 . (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 cdlemk55a K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X = G / g X I / g X

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 simp1l K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I K HL W H
13 simp211 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I F T
14 simp212 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I F I B
15 13 14 jca K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I F T F I B
16 simp32 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I j T
17 simp213 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I N T
18 simp23 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I P A ¬ P ˙ W
19 simp1r K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I R F = R N
20 18 19 jca K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I P A ¬ P ˙ W R F = R N
21 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s-id K HL W H F T F I B j T N T P A ¬ P ˙ W R F = R N j / g X T
22 12 15 16 17 20 21 syl131anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I j / g X T
23 1 6 7 ltrn1o K HL W H j / g X T j / g X : B 1-1 onto B
24 12 22 23 syl2anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I j / g X : B 1-1 onto B
25 f1ococnv2 j / g X : B 1-1 onto B j / g X j / g X -1 = I B
26 24 25 syl K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I j / g X j / g X -1 = I B
27 26 coeq2d K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X j / g X j / g X -1 = G I / g X I B
28 simp22 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G T
29 simp31l K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I I T
30 6 7 ltrnco K HL W H G T I T G I T
31 12 28 29 30 syl3anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I T
32 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s-id K HL W H F T F I B G I T N T P A ¬ P ˙ W R F = R N G I / g X T
33 12 15 31 17 20 32 syl131anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X T
34 1 6 7 ltrn1o K HL W H G I / g X T G I / g X : B 1-1 onto B
35 12 33 34 syl2anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X : B 1-1 onto B
36 f1of G I / g X : B 1-1 onto B G I / g X : B B
37 fcoi1 G I / g X : B B G I / g X I B = G I / g X
38 35 36 37 3syl K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X I B = G I / g X
39 27 38 eqtr2d K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X = G I / g X j / g X j / g X -1
40 coass G I / g X j / g X j / g X -1 = G I / g X j / g X j / g X -1
41 39 40 eqtr4di K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X = G I / g X j / g X j / g X -1
42 1 2 3 4 5 6 7 8 9 10 11 cdlemk54 K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X j / g X = G / g X I / g X j / g X
43 42 coeq1d K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X j / g X j / g X -1 = G / g X I / g X j / g X j / g X -1
44 coass G / g X I / g X j / g X j / g X -1 = G / g X I / g X j / g X j / g X -1
45 26 coeq2d K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X I / g X j / g X j / g X -1 = G / g X I / g X I B
46 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
47 12 15 28 17 20 46 syl131anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X T
48 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s-id K HL W H F T F I B I T N T P A ¬ P ˙ W R F = R N I / g X T
49 12 15 29 17 20 48 syl131anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I I / g X T
50 6 7 ltrnco K HL W H G / g X T I / g X T G / g X I / g X T
51 12 47 49 50 syl3anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X I / g X T
52 1 6 7 ltrn1o K HL W H G / g X I / g X T G / g X I / g X : B 1-1 onto B
53 12 51 52 syl2anc K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X I / g X : B 1-1 onto B
54 f1of G / g X I / g X : B 1-1 onto B G / g X I / g X : B B
55 fcoi1 G / g X I / g X : B B G / g X I / g X I B = G / g X I / g X
56 53 54 55 3syl K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X I / g X I B = G / g X I / g X
57 45 56 eqtrd K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X I / g X j / g X j / g X -1 = G / g X I / g X
58 44 57 syl5eq K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G / g X I / g X j / g X j / g X -1 = G / g X I / g X
59 43 58 eqtrd K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X j / g X j / g X -1 = G / g X I / g X
60 41 59 eqtrd K HL W H R F = R N F T F I B N T G T P A ¬ P ˙ W I T R G = R I j T j I B R j R G R j R G I G I / g X = G / g X I / g X