Metamath Proof Explorer

Theorem tendodi2

Description: Endomorphism composition distributes over sum. (Contributed by NM, 13-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 tendodi2 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) o. V ) = ( ( S o. V ) P ( U o. 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 3 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S P U ) e. E /\ V e. E ) -> ( ( S P U ) o. 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 ) o. V ) e. E )
13 1 3 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ V e. E ) -> ( S o. V ) e. E )
14 5 6 10 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. V ) e. E )
15 1 3 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U o. V ) e. E )
16 5 7 10 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( U o. V ) e. E )
17 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S o. V ) e. E /\ ( U o. V ) e. E ) -> ( ( S o. V ) P ( U o. V ) ) e. E )
18 5 14 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S o. V ) P ( U o. V ) ) e. E )
19 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( K e. HL /\ W e. H ) )
20 simplr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> S e. E )
21 simplr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> U e. E )
22 19 20 21 8 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S P U ) e. E )
23 simplr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> V e. E )
24 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> g e. T )
25 1 2 3 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S P U ) e. E /\ V e. E ) /\ g e. T ) -> ( ( ( S P U ) o. V ) ` g ) = ( ( S P U ) ` ( V ` g ) ) )
26 19 22 23 24 25 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S P U ) o. V ) ` g ) = ( ( S P U ) ` ( V ` g ) ) )
27 simplll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> K e. HL )
28 simpllr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> W e. H )
29 1 2 3 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ V e. E ) /\ g e. T ) -> ( ( S o. V ) ` g ) = ( S ` ( V ` g ) ) )
30 27 28 20 23 24 29 syl221anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S o. V ) ` g ) = ( S ` ( V ` g ) ) )
31 1 2 3 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ g e. T ) -> ( ( U o. V ) ` g ) = ( U ` ( V ` g ) ) )
32 27 28 21 23 24 31 syl221anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( U o. V ) ` g ) = ( U ` ( V ` g ) ) )
33 30 32 coeq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S o. V ) ` g ) o. ( ( U o. V ) ` g ) ) = ( ( S ` ( V ` g ) ) o. ( U ` ( V ` g ) ) ) )
34 19 20 23 13 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S o. V ) e. E )
35 19 21 23 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( U o. V ) e. E )
36 4 2 tendopl2 
 |-  ( ( ( S o. V ) e. E /\ ( U o. V ) e. E /\ g e. T ) -> ( ( ( S o. V ) P ( U o. V ) ) ` g ) = ( ( ( S o. V ) ` g ) o. ( ( U o. V ) ` g ) ) )
37 34 35 24 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S o. V ) P ( U o. V ) ) ` g ) = ( ( ( S o. V ) ` g ) o. ( ( U o. V ) ` g ) ) )
38 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ g e. T ) -> ( V ` g ) e. T )
39 19 23 24 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( V ` g ) e. T )
40 4 2 tendopl2 
 |-  ( ( S e. E /\ U e. E /\ ( V ` g ) e. T ) -> ( ( S P U ) ` ( V ` g ) ) = ( ( S ` ( V ` g ) ) o. ( U ` ( V ` g ) ) ) )
41 20 21 39 40 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S P U ) ` ( V ` g ) ) = ( ( S ` ( V ` g ) ) o. ( U ` ( V ` g ) ) ) )
42 33 37 41 3eqtr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S P U ) ` ( V ` g ) ) = ( ( ( S o. V ) P ( U o. V ) ) ` g ) )
43 26 42 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S P U ) o. V ) ` g ) = ( ( ( S o. V ) P ( U o. V ) ) ` g ) )
44 43 ralrimiva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> A. g e. T ( ( ( S P U ) o. V ) ` g ) = ( ( ( S o. V ) P ( U o. V ) ) ` g ) )
45 1 2 3 tendoeq1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( S P U ) o. V ) e. E /\ ( ( S o. V ) P ( U o. V ) ) e. E ) /\ A. g e. T ( ( ( S P U ) o. V ) ` g ) = ( ( ( S o. V ) P ( U o. V ) ) ` g ) ) -> ( ( S P U ) o. V ) = ( ( S o. V ) P ( U o. V ) ) )
46 5 12 18 44 45 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) o. V ) = ( ( S o. V ) P ( U o. V ) ) )