Metamath Proof Explorer

Theorem tendoplass

Description: The endomorphism sum operation is associative. (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 tendoplass 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) P V ) = ( S P ( U P V ) ) )

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 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( K e. HL /\ W e. H ) )
6 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> S e. E )
7 simpr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> U e. E )
8 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ U e. E ) -> ( S P U ) e. E )
9 5 6 7 8 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S P U ) e. E )
10 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> V e. E )
11 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S P U ) e. E /\ V e. E ) -> ( ( S P U ) P V ) e. E )
12 5 9 10 11 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) P V ) e. E )
13 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) e. E )
14 5 7 10 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( U P V ) e. E )
15 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( U P V ) e. E ) -> ( S P ( U P V ) ) e. E )
16 5 6 14 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S P ( U P V ) ) e. E )
17 coass 
 |-  ( ( ( S ` g ) o. ( U ` g ) ) o. ( V ` g ) ) = ( ( S ` g ) o. ( ( U ` g ) o. ( V ` g ) ) )
18 simplr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> S e. E )
19 simplr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> U e. E )
20 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> g e. T )
21 4 2 tendopl2 
 |-  ( ( S e. E /\ U e. E /\ g e. T ) -> ( ( S P U ) ` g ) = ( ( S ` g ) o. ( U ` g ) ) )
22 18 19 20 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S P U ) ` g ) = ( ( S ` g ) o. ( U ` g ) ) )
23 22 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S P U ) ` g ) o. ( V ` g ) ) = ( ( ( S ` g ) o. ( U ` g ) ) o. ( V ` g ) ) )
24 simplr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> V e. E )
25 4 2 tendopl2 
 |-  ( ( U e. E /\ V e. E /\ g e. T ) -> ( ( U P V ) ` g ) = ( ( U ` g ) o. ( V ` g ) ) )
26 19 24 20 25 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( U P V ) ` g ) = ( ( U ` g ) o. ( V ` g ) ) )
27 26 coeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S ` g ) o. ( ( U P V ) ` g ) ) = ( ( S ` g ) o. ( ( U ` g ) o. ( V ` g ) ) ) )
28 17 23 27 3eqtr4a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S P U ) ` g ) o. ( V ` g ) ) = ( ( S ` g ) o. ( ( U P V ) ` g ) ) )
29 9 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S P U ) e. E )
30 4 2 tendopl2 
 |-  ( ( ( S P U ) e. E /\ V e. E /\ g e. T ) -> ( ( ( S P U ) P V ) ` g ) = ( ( ( S P U ) ` g ) o. ( V ` g ) ) )
31 29 24 20 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S P U ) P V ) ` g ) = ( ( ( S P U ) ` g ) o. ( V ` g ) ) )
32 14 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( U P V ) e. E )
33 4 2 tendopl2 
 |-  ( ( S e. E /\ ( U P V ) e. E /\ g e. T ) -> ( ( S P ( U P V ) ) ` g ) = ( ( S ` g ) o. ( ( U P V ) ` g ) ) )
34 18 32 20 33 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S P ( U P V ) ) ` g ) = ( ( S ` g ) o. ( ( U P V ) ` g ) ) )
35 28 31 34 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S P U ) P V ) ` g ) = ( ( S P ( U P V ) ) ` g ) )
36 35 ralrimiva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> A. g e. T ( ( ( S P U ) P V ) ` g ) = ( ( S P ( U P V ) ) ` g ) )
37 1 2 3 tendoeq1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( S P U ) P V ) e. E /\ ( S P ( U P V ) ) e. E ) /\ A. g e. T ( ( ( S P U ) P V ) ` g ) = ( ( S P ( U P V ) ) ` g ) ) -> ( ( S P U ) P V ) = ( S P ( U P V ) ) )
38 5 12 16 36 37 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) P V ) = ( S P ( U P V ) ) )