Metamath Proof Explorer

Theorem tendoeq2

Description: Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan , we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 tendoeq2.b 
 |-  B = ( Base ` K )
2 tendoeq2.h 
 |-  H = ( LHyp ` K )
3 tendoeq2.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoeq2.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 1 2 4 tendoid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U ` ( _I |` B ) ) = ( _I |` B ) )
6 5 adantrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U ` ( _I |` B ) ) = ( _I |` B ) )
7 1 2 4 tendoid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E ) -> ( V ` ( _I |` B ) ) = ( _I |` B ) )
8 7 adantrl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( V ` ( _I |` B ) ) = ( _I |` B ) )
9 6 8 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U ` ( _I |` B ) ) = ( V ` ( _I |` B ) ) )
10 fveq2 
 |-  ( f = ( _I |` B ) -> ( U ` f ) = ( U ` ( _I |` B ) ) )
11 fveq2 
 |-  ( f = ( _I |` B ) -> ( V ` f ) = ( V ` ( _I |` B ) ) )
12 10 11 eqeq12d 
 |-  ( f = ( _I |` B ) -> ( ( U ` f ) = ( V ` f ) <-> ( U ` ( _I |` B ) ) = ( V ` ( _I |` B ) ) ) )
13 9 12 syl5ibrcom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) )
14 13 ralrimivw 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> A. f e. T ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) )
15 r19.26 
 |-  ( A. f e. T ( ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) <-> ( A. f e. T ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ A. f e. T ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) )
16 jaob 
 |-  ( ( ( f = ( _I |` B ) \/ f =/= ( _I |` B ) ) -> ( U ` f ) = ( V ` f ) ) <-> ( ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) )
17 exmidne 
 |-  ( f = ( _I |` B ) \/ f =/= ( _I |` B ) )
18 pm5.5 
 |-  ( ( f = ( _I |` B ) \/ f =/= ( _I |` B ) ) -> ( ( ( f = ( _I |` B ) \/ f =/= ( _I |` B ) ) -> ( U ` f ) = ( V ` f ) ) <-> ( U ` f ) = ( V ` f ) ) )
19 17 18 ax-mp 
 |-  ( ( ( f = ( _I |` B ) \/ f =/= ( _I |` B ) ) -> ( U ` f ) = ( V ` f ) ) <-> ( U ` f ) = ( V ` f ) )
20 16 19 bitr3i 
 |-  ( ( ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) <-> ( U ` f ) = ( V ` f ) )
21 20 ralbii 
 |-  ( A. f e. T ( ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) <-> A. f e. T ( U ` f ) = ( V ` f ) )
22 15 21 bitr3i 
 |-  ( ( A. f e. T ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ A. f e. T ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) <-> A. f e. T ( U ` f ) = ( V ` f ) )
23 2 3 4 tendoeq1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U = V )
24 23 3expia 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( A. f e. T ( U ` f ) = ( V ` f ) -> U = V ) )
25 22 24 syl5bi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( ( A. f e. T ( f = ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) /\ A. f e. T ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) -> U = V ) )
26 14 25 mpand 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( A. f e. T ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) -> U = V ) )
27 26 3impia 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) -> U = V )