Theorem cdlemg47a

Description: TODO: fix comment. TODO: Use this above in place of ( FP ) = P antecedents? (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 )
Assertion	cdlemg47a	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( 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		simp1	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
5		simp2r	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> G e. T )
6	1 2 3	ltrn1o	|- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> G : B -1-1-onto-> B )
7	4 5 6	syl2anc	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> G : B -1-1-onto-> B )
8		f1of	|- ( G : B -1-1-onto-> B -> G : B --> B )
9	7 8	syl	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> G : B --> B )
10		fcoi1	|- ( G : B --> B -> ( G o. ( _I |` B ) ) = G )
11	9 10	syl	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( G o. ( _I |` B ) ) = G )
12		simp3	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> F = ( _I |` B ) )
13	12	coeq2d	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( G o. F ) = ( G o. ( _I |` B ) ) )
14	12	coeq1d	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( F o. G ) = ( ( _I |` B ) o. G ) )
15		fcoi2	|- ( G : B --> B -> ( ( _I |` B ) o. G ) = G )
16	9 15	syl	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( ( _I |` B ) o. G ) = G )
17	14 16	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( F o. G ) = G )
18	11 13 17	3eqtr4rd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( F o. G ) = ( G o. F ) )