Metamath Proof Explorer

Theorem tendoid0

Description: A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013)

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

Proof

Step Hyp Ref Expression
1 tendoid0.b 
 |-  B = ( Base ` K )
2 tendoid0.h 
 |-  H = ( LHyp ` K )
3 tendoid0.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoid0.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 tendoid0.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
6 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> F e. T )
7 5 1 tendo02 
 |-  ( F e. T -> ( O ` F ) = ( _I |` B ) )
8 6 7 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( O ` F ) = ( _I |` B ) )
9 8 eqeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( ( U ` F ) = ( O ` F ) <-> ( U ` F ) = ( _I |` B ) ) )
10 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> ( K e. HL /\ W e. H ) )
11 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> U e. E )
12 1 2 3 4 5 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. E )
13 10 12 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> O e. E )
14 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> ( U ` F ) = ( O ` F ) )
15 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> F e. T )
16 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> F =/= ( _I |` B ) )
17 1 2 3 4 tendocan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ O e. E /\ ( U ` F ) = ( O ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> U = O )
18 10 11 13 14 15 16 17 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) /\ ( U ` F ) = ( O ` F ) ) -> U = O )
19 18 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( ( U ` F ) = ( O ` F ) -> U = O ) )
20 9 19 sylbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( ( U ` F ) = ( _I |` B ) -> U = O ) )
21 fveq1 
 |-  ( U = O -> ( U ` F ) = ( O ` F ) )
22 21 eqeq1d 
 |-  ( U = O -> ( ( U ` F ) = ( _I |` B ) <-> ( O ` F ) = ( _I |` B ) ) )
23 8 22 syl5ibrcom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( U = O -> ( U ` F ) = ( _I |` B ) ) )
24 20 23 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( ( U ` F ) = ( _I |` B ) <-> U = O ) )