Metamath Proof Explorer


Theorem cdlemk45

Description: Part of proof of Lemma K of Crawley p. 118. Line 37, p. 119. G , I stand for g, h. X represents tau. They do not explicitly mention the requirement ` ( G o. I ) =/= ( _I |`B ) . (Contributed by NM, 22-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 cdlemk45 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G I / g X P ˙ I / g X P ˙ 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 simp11 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B K HL W H
13 simp12 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B F T F I B
14 simp13l K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G T
15 simp31 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I T
16 6 7 ltrnco K HL W H G T I T G I T
17 12 14 15 16 syl3anc K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G I T
18 simp33 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G I I B
19 17 18 jca K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G I T G I I B
20 simp2 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B N T P A ¬ P ˙ W R F = R N
21 simp32 K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I I B
22 1 2 3 4 5 6 7 8 9 10 11 cdlemk11t K HL W H F T F I B G I T G I I B N T P A ¬ P ˙ W R F = R N I T I I B G I / g X P ˙ I / g X P ˙ R I G I -1
23 12 13 19 20 15 21 22 syl312anc K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G I / g X P ˙ I / g X P ˙ R I G I -1
24 cnvco G I -1 = I -1 G -1
25 24 coeq2i I G I -1 = I I -1 G -1
26 coass I I -1 G -1 = I I -1 G -1
27 25 26 eqtr4i I G I -1 = I I -1 G -1
28 1 6 7 ltrn1o K HL W H I T I : B 1-1 onto B
29 12 15 28 syl2anc K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I : B 1-1 onto B
30 f1ococnv2 I : B 1-1 onto B I I -1 = I B
31 29 30 syl K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I I -1 = I B
32 31 coeq1d K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I I -1 G -1 = I B G -1
33 1 6 7 ltrn1o K HL W H G T G : B 1-1 onto B
34 12 14 33 syl2anc K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G : B 1-1 onto B
35 f1ocnv G : B 1-1 onto B G -1 : B 1-1 onto B
36 f1of G -1 : B 1-1 onto B G -1 : B B
37 fcoi2 G -1 : B B I B G -1 = G -1
38 34 35 36 37 4syl K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I B G -1 = G -1
39 32 38 eqtrd K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I I -1 G -1 = G -1
40 27 39 syl5eq K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I G I -1 = G -1
41 40 fveq2d K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B R I G I -1 = R G -1
42 6 7 8 trlcnv K HL W H G T R G -1 = R G
43 12 14 42 syl2anc K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B R G -1 = R G
44 41 43 eqtrd K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B R I G I -1 = R G
45 44 oveq2d K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B I / g X P ˙ R I G I -1 = I / g X P ˙ R G
46 23 45 breqtrd K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N I T I I B G I I B G I / g X P ˙ I / g X P ˙ R G