Metamath Proof Explorer

Theorem tendotr

Description: The trace of the value of a nonzero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013)

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

Proof

Step Hyp Ref Expression
1 tendotr.b 
 |-  B = ( Base ` K )
2 tendotr.h 
 |-  H = ( LHyp ` K )
3 tendotr.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendotr.r 
 |-  R = ( ( trL ` K ) ` W )
5 tendotr.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 tendotr.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
7 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
8 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> U e. E )
9 1 2 5 tendoid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U ` ( _I |` B ) ) = ( _I |` B ) )
10 7 8 9 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> ( U ` ( _I |` B ) ) = ( _I |` B ) )
11 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> F = ( _I |` B ) )
12 11 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> ( U ` F ) = ( U ` ( _I |` B ) ) )
13 10 12 11 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> ( U ` F ) = F )
14 13 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F = ( _I |` B ) ) -> ( R ` ( U ` F ) ) = ( R ` F ) )
15 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
16 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> U e. E )
17 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> F e. T )
18 eqid 
 |-  ( le ` K ) = ( le ` K )
19 18 2 3 4 5 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ F e. T ) -> ( R ` ( U ` F ) ) ( le ` K ) ( R ` F ) )
20 15 16 17 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( R ` ( U ` F ) ) ( le ` K ) ( R ` F ) )
21 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> K e. HL )
22 hlatl 
 |-  ( K e. HL -> K e. AtLat )
23 21 22 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> K e. AtLat )
24 2 3 5 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ F e. T ) -> ( U ` F ) e. T )
25 15 16 17 24 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( U ` F ) e. T )
26 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> U =/= O )
27 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> F =/= ( _I |` B ) )
28 1 2 3 5 6 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( ( U ` F ) = ( _I |` B ) <-> U = O ) )
29 15 16 17 27 28 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( ( U ` F ) = ( _I |` B ) <-> U = O ) )
30 29 necon3bid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( ( U ` F ) =/= ( _I |` B ) <-> U =/= O ) )
31 26 30 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( U ` F ) =/= ( _I |` B ) )
32 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
33 1 32 2 3 4 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U ` F ) e. T /\ ( U ` F ) =/= ( _I |` B ) ) -> ( R ` ( U ` F ) ) e. ( Atoms ` K ) )
34 15 25 31 33 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( R ` ( U ` F ) ) e. ( Atoms ` K ) )
35 1 32 2 3 4 trlnidat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> ( R ` F ) e. ( Atoms ` K ) )
36 15 17 27 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( R ` F ) e. ( Atoms ` K ) )
37 18 32 atcmp 
 |-  ( ( K e. AtLat /\ ( R ` ( U ` F ) ) e. ( Atoms ` K ) /\ ( R ` F ) e. ( Atoms ` K ) ) -> ( ( R ` ( U ` F ) ) ( le ` K ) ( R ` F ) <-> ( R ` ( U ` F ) ) = ( R ` F ) ) )
38 23 34 36 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( ( R ` ( U ` F ) ) ( le ` K ) ( R ` F ) <-> ( R ` ( U ` F ) ) = ( R ` F ) ) )
39 20 38 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) /\ F =/= ( _I |` B ) ) -> ( R ` ( U ` F ) ) = ( R ` F ) )
40 14 39 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) -> ( R ` ( U ` F ) ) = ( R ` F ) )