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 )