Metamath Proof Explorer


Theorem cdlemg47

Description: Part of proof of Lemma G of Crawley p. 116, ninth line of third paragraph on p. 117: "we conclude that gf = fg." (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses cdlemg46.b B = Base K
cdlemg46.h H = LHyp K
cdlemg46.t T = LTrn K W
cdlemg46.r R = trL K W
Assertion cdlemg47 K HL W H F T G T h T R F = R G F I B h I B R h R F F G = G F

Proof

Step Hyp Ref Expression
1 cdlemg46.b B = Base K
2 cdlemg46.h H = LHyp K
3 cdlemg46.t T = LTrn K W
4 cdlemg46.r R = trL K W
5 simp11 K HL W H F T G T h T R F = R G F I B h I B R h R F K HL W H
6 simp2l K HL W H F T G T h T R F = R G F I B h I B R h R F h T
7 simp12 K HL W H F T G T h T R F = R G F I B h I B R h R F F T
8 2 3 ltrnco K HL W H h T F T h F T
9 5 6 7 8 syl3anc K HL W H F T G T h T R F = R G F I B h I B R h R F h F T
10 simp13 K HL W H F T G T h T R F = R G F I B h I B R h R F G T
11 simp3 K HL W H F T G T h T R F = R G F I B h I B R h R F F I B h I B R h R F
12 1 2 3 4 cdlemg46 K HL W H F T h T F I B h I B R h R F R h F R F
13 5 7 6 11 12 syl121anc K HL W H F T G T h T R F = R G F I B h I B R h R F R h F R F
14 simp2r K HL W H F T G T h T R F = R G F I B h I B R h R F R F = R G
15 13 14 neeqtrd K HL W H F T G T h T R F = R G F I B h I B R h R F R h F R G
16 2 3 4 cdlemg44 K HL W H h F T G T R h F R G h F G = G h F
17 5 9 10 15 16 syl121anc K HL W H F T G T h T R F = R G F I B h I B R h R F h F G = G h F
18 coass G h F = G h F
19 17 18 eqtr4di K HL W H F T G T h T R F = R G F I B h I B R h R F h F G = G h F
20 simp33 K HL W H F T G T h T R F = R G F I B h I B R h R F R h R F
21 20 14 neeqtrd K HL W H F T G T h T R F = R G F I B h I B R h R F R h R G
22 2 3 4 cdlemg44 K HL W H h T G T R h R G h G = G h
23 5 6 10 21 22 syl121anc K HL W H F T G T h T R F = R G F I B h I B R h R F h G = G h
24 23 coeq1d K HL W H F T G T h T R F = R G F I B h I B R h R F h G F = G h F
25 19 24 eqtr4d K HL W H F T G T h T R F = R G F I B h I B R h R F h F G = h G F
26 coass h F G = h F G
27 coass h G F = h G F
28 25 26 27 3eqtr3g K HL W H F T G T h T R F = R G F I B h I B R h R F h F G = h G F
29 28 coeq2d K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h F G = h -1 h G F
30 coass h -1 h F G = h -1 h F G
31 1 2 3 ltrn1o K HL W H h T h : B 1-1 onto B
32 5 6 31 syl2anc K HL W H F T G T h T R F = R G F I B h I B R h R F h : B 1-1 onto B
33 f1ococnv1 h : B 1-1 onto B h -1 h = I B
34 32 33 syl K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h = I B
35 34 coeq1d K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h F G = I B F G
36 30 35 eqtr3id K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h F G = I B F G
37 2 3 ltrnco K HL W H F T G T F G T
38 5 7 10 37 syl3anc K HL W H F T G T h T R F = R G F I B h I B R h R F F G T
39 1 2 3 ltrn1o K HL W H F G T F G : B 1-1 onto B
40 5 38 39 syl2anc K HL W H F T G T h T R F = R G F I B h I B R h R F F G : B 1-1 onto B
41 f1of F G : B 1-1 onto B F G : B B
42 fcoi2 F G : B B I B F G = F G
43 40 41 42 3syl K HL W H F T G T h T R F = R G F I B h I B R h R F I B F G = F G
44 36 43 eqtrd K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h F G = F G
45 coass h -1 h G F = h -1 h G F
46 34 coeq1d K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h G F = I B G F
47 45 46 eqtr3id K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h G F = I B G F
48 2 3 ltrnco K HL W H G T F T G F T
49 5 10 7 48 syl3anc K HL W H F T G T h T R F = R G F I B h I B R h R F G F T
50 1 2 3 ltrn1o K HL W H G F T G F : B 1-1 onto B
51 5 49 50 syl2anc K HL W H F T G T h T R F = R G F I B h I B R h R F G F : B 1-1 onto B
52 f1of G F : B 1-1 onto B G F : B B
53 fcoi2 G F : B B I B G F = G F
54 51 52 53 3syl K HL W H F T G T h T R F = R G F I B h I B R h R F I B G F = G F
55 47 54 eqtrd K HL W H F T G T h T R F = R G F I B h I B R h R F h -1 h G F = G F
56 29 44 55 3eqtr3d K HL W H F T G T h T R F = R G F I B h I B R h R F F G = G F