Metamath Proof Explorer

Theorem tendoplcom

Description: The endomorphism sum operation is commutative. (Contributed by NM, 11-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 tendoplcom 
|- ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) = ( V P U ) )

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 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( K e. HL /\ W e. H ) )
6 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) e. E )
7 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ U e. E ) -> ( V P U ) e. E )
8 7 3com23 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( V P U ) e. E )
9 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( K e. HL /\ W e. H ) )
10 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> U e. E )
11 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> g e. T )
12 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ g e. T ) -> ( U ` g ) e. T )
13 9 10 11 12 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( U ` g ) e. T )
14 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> V e. E )
15 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ g e. T ) -> ( V ` g ) e. T )
16 9 14 11 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( V ` g ) e. T )
17 1 2 ltrncom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U ` g ) e. T /\ ( V ` g ) e. T ) -> ( ( U ` g ) o. ( V ` g ) ) = ( ( V ` g ) o. ( U ` g ) ) )
18 9 13 16 17 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( ( U ` g ) o. ( V ` g ) ) = ( ( V ` g ) o. ( U ` g ) ) )
19 4 2 tendopl2 
 |-  ( ( U e. E /\ V e. E /\ g e. T ) -> ( ( U P V ) ` g ) = ( ( U ` g ) o. ( V ` g ) ) )
20 10 14 11 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( ( U P V ) ` g ) = ( ( U ` g ) o. ( V ` g ) ) )
21 4 2 tendopl2 
 |-  ( ( V e. E /\ U e. E /\ g e. T ) -> ( ( V P U ) ` g ) = ( ( V ` g ) o. ( U ` g ) ) )
22 14 10 11 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( ( V P U ) ` g ) = ( ( V ` g ) o. ( U ` g ) ) )
23 18 20 22 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) /\ g e. T ) -> ( ( U P V ) ` g ) = ( ( V P U ) ` g ) )
24 23 ralrimiva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> A. g e. T ( ( U P V ) ` g ) = ( ( V P U ) ` g ) )
25 1 2 3 tendoeq1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( U P V ) e. E /\ ( V P U ) e. E ) /\ A. g e. T ( ( U P V ) ` g ) = ( ( V P U ) ` g ) ) -> ( U P V ) = ( V P U ) )
26 5 6 8 24 25 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) = ( V P U ) )