Metamath Proof Explorer

Theorem tendoidcl

Description: The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013)

Ref Expression
Hypotheses tendof.h 
|- H = ( LHyp ` K )
tendof.t 
|- T = ( ( LTrn ` K ) ` W )
tendof.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion tendoidcl 
|- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )

Proof

Step Hyp Ref Expression
1 tendof.h 
 |-  H = ( LHyp ` K )
2 tendof.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 tendof.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 eqid 
 |-  ( le ` K ) = ( le ` K )
5 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
6 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
7 f1oi 
 |-  ( _I |` T ) : T -1-1-onto-> T
8 f1of 
 |-  ( ( _I |` T ) : T -1-1-onto-> T -> ( _I |` T ) : T --> T )
9 7 8 mp1i 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) : T --> T )
10 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ g e. T ) -> ( f o. g ) e. T )
11 fvresi 
 |-  ( ( f o. g ) e. T -> ( ( _I |` T ) ` ( f o. g ) ) = ( f o. g ) )
12 10 11 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ g e. T ) -> ( ( _I |` T ) ` ( f o. g ) ) = ( f o. g ) )
13 fvresi 
 |-  ( f e. T -> ( ( _I |` T ) ` f ) = f )
14 13 3ad2ant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ g e. T ) -> ( ( _I |` T ) ` f ) = f )
15 fvresi 
 |-  ( g e. T -> ( ( _I |` T ) ` g ) = g )
16 15 3ad2ant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ g e. T ) -> ( ( _I |` T ) ` g ) = g )
17 14 16 coeq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ g e. T ) -> ( ( ( _I |` T ) ` f ) o. ( ( _I |` T ) ` g ) ) = ( f o. g ) )
18 12 17 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ g e. T ) -> ( ( _I |` T ) ` ( f o. g ) ) = ( ( ( _I |` T ) ` f ) o. ( ( _I |` T ) ` g ) ) )
19 13 adantl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( _I |` T ) ` f ) = f )
20 19 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( _I |` T ) ` f ) ) = ( ( ( trL ` K ) ` W ) ` f ) )
21 hllat 
 |-  ( K e. HL -> K e. Lat )
22 21 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> K e. Lat )
23 eqid 
 |-  ( Base ` K ) = ( Base ` K )
24 23 1 2 5 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) )
25 23 4 latref 
 |-  ( ( K e. Lat /\ ( ( ( trL ` K ) ` W ) ` f ) e. ( Base ` K ) ) -> ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` f ) )
26 22 24 25 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` f ) )
27 20 26 eqbrtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( _I |` T ) ` f ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` f ) )
28 4 1 2 5 3 6 9 18 27 istendod 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )