This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( F o. G ) = ( G o. 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 e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( K e. HL /\ W e. H ) )
6 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> h e. T )
7 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> F e. T )
8 2 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ h e. T /\ F e. T ) -> ( h o. F ) e. T )
9 5 6 7 8 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( h o. F ) e. T )
10 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> G e. T )
11 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. 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 e. HL /\ W e. H ) /\ ( F e. T /\ h e. T ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` ( h o. F ) ) =/= ( R ` F ) )
13 5 7 6 11 12 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` ( h o. F ) ) =/= ( R ` F ) )
14 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` F ) = ( R ` G ) )
15 13 14 neeqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` ( h o. F ) ) =/= ( R ` G ) )
16 2 3 4 cdlemg44 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( h o. F ) e. T /\ G e. T ) /\ ( R ` ( h o. F ) ) =/= ( R ` G ) ) -> ( ( h o. F ) o. G ) = ( G o. ( h o. F ) ) )
17 5 9 10 15 16 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( h o. F ) o. G ) = ( G o. ( h o. F ) ) )
18 coass 
 |-  ( ( G o. h ) o. F ) = ( G o. ( h o. F ) )
19 17 18 eqtr4di 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( h o. F ) o. G ) = ( ( G o. h ) o. F ) )
20 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` h ) =/= ( R ` F ) )
21 20 14 neeqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. 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 e. HL /\ W e. H ) /\ ( h e. T /\ G e. T ) /\ ( R ` h ) =/= ( R ` G ) ) -> ( h o. G ) = ( G o. h ) )
23 5 6 10 21 22 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( h o. G ) = ( G o. h ) )
24 23 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( h o. G ) o. F ) = ( ( G o. h ) o. F ) )
25 19 24 eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( h o. F ) o. G ) = ( ( h o. G ) o. F ) )
26 coass 
 |-  ( ( h o. F ) o. G ) = ( h o. ( F o. G ) )
27 coass 
 |-  ( ( h o. G ) o. F ) = ( h o. ( G o. F ) )
28 25 26 27 3eqtr3g 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( h o. ( F o. G ) ) = ( h o. ( G o. F ) ) )
29 28 coeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( `' h o. ( h o. ( F o. G ) ) ) = ( `' h o. ( h o. ( G o. F ) ) ) )
30 coass 
 |-  ( ( `' h o. h ) o. ( F o. G ) ) = ( `' h o. ( h o. ( F o. G ) ) )
31 1 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ h e. T ) -> h : B -1-1-onto-> B )
32 5 6 31 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. 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 o. h ) = ( _I |` B ) )
34 32 33 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( `' h o. h ) = ( _I |` B ) )
35 34 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( `' h o. h ) o. ( F o. G ) ) = ( ( _I |` B ) o. ( F o. G ) ) )
36 30 35 eqtr3id 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( `' h o. ( h o. ( F o. G ) ) ) = ( ( _I |` B ) o. ( F o. G ) ) )
37 2 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
38 5 7 10 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( F o. G ) e. T )
39 1 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F o. G ) e. T ) -> ( F o. G ) : B -1-1-onto-> B )
40 5 38 39 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( F o. G ) : B -1-1-onto-> B )
41 f1of 
 |-  ( ( F o. G ) : B -1-1-onto-> B -> ( F o. G ) : B --> B )
42 fcoi2 
 |-  ( ( F o. G ) : B --> B -> ( ( _I |` B ) o. ( F o. G ) ) = ( F o. G ) )
43 40 41 42 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( _I |` B ) o. ( F o. G ) ) = ( F o. G ) )
44 36 43 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( `' h o. ( h o. ( F o. G ) ) ) = ( F o. G ) )
45 coass 
 |-  ( ( `' h o. h ) o. ( G o. F ) ) = ( `' h o. ( h o. ( G o. F ) ) )
46 34 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( `' h o. h ) o. ( G o. F ) ) = ( ( _I |` B ) o. ( G o. F ) ) )
47 45 46 eqtr3id 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( `' h o. ( h o. ( G o. F ) ) ) = ( ( _I |` B ) o. ( G o. F ) ) )
48 2 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ F e. T ) -> ( G o. F ) e. T )
49 5 10 7 48 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( G o. F ) e. T )
50 1 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G o. F ) e. T ) -> ( G o. F ) : B -1-1-onto-> B )
51 5 49 50 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( G o. F ) : B -1-1-onto-> B )
52 f1of 
 |-  ( ( G o. F ) : B -1-1-onto-> B -> ( G o. F ) : B --> B )
53 fcoi2 
 |-  ( ( G o. F ) : B --> B -> ( ( _I |` B ) o. ( G o. F ) ) = ( G o. F ) )
54 51 52 53 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( ( _I |` B ) o. ( G o. F ) ) = ( G o. F ) )
55 47 54 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( `' h o. ( h o. ( G o. F ) ) ) = ( G o. F ) )
56 29 44 55 3eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( F o. G ) = ( G o. F ) )