Metamath Proof Explorer

Theorem tendoplcl

Description: Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses tendopl.h 
|- H = ( LHyp ` K )
tendopl.t 
|- T = ( ( LTrn ` K ) ` W )
tendopl.e 
|- E = ( ( TEndo ` K ) ` W )
tendopl.p 
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
Assertion tendoplcl 
|- ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) e. E )

Proof

Step Hyp Ref Expression
1 tendopl.h 
 |-  H = ( LHyp ` K )
2 tendopl.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 tendopl.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 tendopl.p 
 |-  P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
7 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( K e. HL /\ W e. H ) )
8 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( K e. HL /\ W e. H ) )
9 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> U e. E )
10 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> g e. T )
11 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ g e. T ) -> ( U ` g ) e. T )
12 8 9 10 11 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( U ` g ) e. T )
13 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> V e. E )
14 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ g e. T ) -> ( V ` g ) e. T )
15 8 13 10 14 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( V ` g ) e. T )
16 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U ` g ) e. T /\ ( V ` g ) e. T ) -> ( ( U ` g ) o. ( V ` g ) ) e. T )
17 8 12 15 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( ( U ` g ) o. ( V ` g ) ) e. T )
18 17 fmpttd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( g e. T |-> ( ( U ` g ) o. ( V ` g ) ) ) : T --> T )
19 4 2 tendopl 
 |-  ( ( U e. E /\ V e. E ) -> ( U P V ) = ( g e. T |-> ( ( U ` g ) o. ( V ` g ) ) ) )
20 19 3adant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) = ( g e. T |-> ( ( U ` g ) o. ( V ` g ) ) ) )
21 20 feq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( ( U P V ) : T --> T <-> ( g e. T |-> ( ( U ` g ) o. ( V ` g ) ) ) : T --> T ) )
22 18 21 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) : T --> T )
23 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T /\ i e. T ) -> ( K e. HL /\ W e. H ) )
24 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T /\ i e. T ) -> U e. E )
25 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T /\ i e. T ) -> V e. E )
26 3simpc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T /\ i e. T ) -> ( h e. T /\ i e. T ) )
27 1 2 3 4 tendoplco2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( h e. T /\ i e. T ) ) -> ( ( U P V ) ` ( h o. i ) ) = ( ( ( U P V ) ` h ) o. ( ( U P V ) ` i ) ) )
28 23 24 25 26 27 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T /\ i e. T ) -> ( ( U P V ) ` ( h o. i ) ) = ( ( ( U P V ) ` h ) o. ( ( U P V ) ` i ) ) )
29 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T ) -> ( K e. HL /\ W e. H ) )
30 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T ) -> U e. E )
31 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T ) -> V e. E )
32 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T ) -> h e. T )
33 1 2 3 4 5 6 tendopltp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ h e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( U P V ) ` h ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` h ) )
34 29 30 31 32 33 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ h e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( U P V ) ` h ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` h ) )
35 5 1 2 6 3 7 22 28 34 istendod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) e. E )