Metamath Proof Explorer

Theorem cdlemg48

Description: Eliminate h from cdlemg47 . (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 cdlemg48 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) -> ( 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 1 2 3 4 cdlemftr1 
 |-  ( ( K e. HL /\ W e. H ) -> E. h e. T ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) )
6 5 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) -> E. h e. T ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) )
7 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( K e. HL /\ W e. H ) )
8 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> F e. T )
9 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> G e. T )
10 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> h e. T )
11 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` F ) = ( R ` G ) )
12 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> F =/= ( _I |` B ) )
13 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> h =/= ( _I |` B ) )
14 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` h ) =/= ( R ` F ) )
15 1 2 3 4 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 ) )
16 7 8 9 10 11 12 13 14 15 syl323anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) /\ h e. T /\ ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( F o. G ) = ( G o. F ) )
17 16 rexlimdv3a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) -> ( E. h e. T ( h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) -> ( F o. G ) = ( G o. F ) ) )
18 6 17 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) -> ( F o. G ) = ( G o. F ) )