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