Metamath Proof Explorer

Theorem tendocan

Description: Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of Crawley p. 118. (Contributed by NM, 21-Jun-2013)

Ref Expression
Hypotheses tendocan.b 
|- B = ( Base ` K )
tendocan.h 
|- H = ( LHyp ` K )
tendocan.t 
|- T = ( ( LTrn ` K ) ` W )
tendocan.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion tendocan 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> U = V )

Proof

Step Hyp Ref Expression
1 tendocan.b 
 |-  B = ( Base ` K )
2 tendocan.h 
 |-  H = ( LHyp ` K )
3 tendocan.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendocan.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> K e. HL )
6 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> W e. H )
7 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> U e. E )
8 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> V e. E )
9 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
10 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) )
11 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> F e. T )
12 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> F =/= ( _I |` B ) )
13 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> h e. T )
14 11 12 13 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) )
15 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> h =/= ( _I |` B ) )
16 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
17 1 2 3 16 4 cdlemj3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ h =/= ( _I |` B ) ) -> ( U ` h ) = ( V ` h ) )
18 9 10 14 15 17 syl31anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ h e. T /\ h =/= ( _I |` B ) ) -> ( U ` h ) = ( V ` h ) )
19 18 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( h e. T -> ( h =/= ( _I |` B ) -> ( U ` h ) = ( V ` h ) ) ) )
20 19 ralrimiv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> A. h e. T ( h =/= ( _I |` B ) -> ( U ` h ) = ( V ` h ) ) )
21 1 2 3 4 tendoeq2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. h e. T ( h =/= ( _I |` B ) -> ( U ` h ) = ( V ` h ) ) ) -> U = V )
22 5 6 7 8 20 21 syl221anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> U = V )