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 ) )