Metamath Proof Explorer

Theorem tendodi1

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 tendodi1 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. ( U P V ) ) = ( ( S o. U ) P ( S 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 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> V e. E )
9 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) e. E )
10 5 7 8 9 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( U P V ) e. E )
11 1 3 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( U P V ) e. E ) -> ( S o. ( U P V ) ) e. E )
12 5 6 10 11 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. ( U P V ) ) e. E )
13 1 3 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ U e. E ) -> ( S o. U ) e. E )
14 5 6 7 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. U ) e. E )
15 1 3 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ V e. E ) -> ( S o. V ) e. E )
16 5 6 8 15 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. V ) e. E )
17 1 2 3 4 tendoplcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S o. U ) e. E /\ ( S o. V ) e. E ) -> ( ( S o. U ) P ( S 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. U ) P ( S o. V ) ) e. E )
19 simplll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> K e. HL )
20 simpllr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> W e. H )
21 simplr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> S e. E )
22 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 ) )
23 simplr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> U 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 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ g e. T ) -> ( U ` g ) e. T )
26 22 23 24 25 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( U ` g ) e. T )
27 simplr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> V e. E )
28 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ g e. T ) -> ( V ` g ) e. T )
29 22 27 24 28 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( V ` g ) e. T )
30 1 2 3 tendovalco 
 |-  ( ( ( K e. HL /\ W e. H /\ S e. E ) /\ ( ( U ` g ) e. T /\ ( V ` g ) e. T ) ) -> ( S ` ( ( U ` g ) o. ( V ` g ) ) ) = ( ( S ` ( U ` g ) ) o. ( S ` ( V ` g ) ) ) )
31 19 20 21 26 29 30 syl32anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S ` ( ( U ` g ) o. ( V ` g ) ) ) = ( ( S ` ( U ` g ) ) o. ( S ` ( V ` g ) ) ) )
32 4 2 tendopl2 
 |-  ( ( U e. E /\ V e. E /\ g e. T ) -> ( ( U P V ) ` g ) = ( ( U ` g ) o. ( V ` g ) ) )
33 23 27 24 32 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 ) ) )
34 33 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S ` ( ( U P V ) ` g ) ) = ( S ` ( ( U ` g ) o. ( V ` g ) ) ) )
35 1 2 3 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E ) /\ g e. T ) -> ( ( S o. U ) ` g ) = ( S ` ( U ` g ) ) )
36 19 20 21 23 24 35 syl221anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S o. U ) ` g ) = ( S ` ( U ` g ) ) )
37 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 ) ) )
38 19 20 21 27 24 37 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 ) ) )
39 36 38 coeq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S o. U ) ` g ) o. ( ( S o. V ) ` g ) ) = ( ( S ` ( U ` g ) ) o. ( S ` ( V ` g ) ) ) )
40 31 34 39 3eqtr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S o. U ) ` g ) o. ( ( S o. V ) ` g ) ) = ( S ` ( ( U P V ) ` g ) ) )
41 22 21 23 13 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S o. U ) e. E )
42 22 21 27 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( S o. V ) e. E )
43 4 2 tendopl2 
 |-  ( ( ( S o. U ) e. E /\ ( S o. V ) e. E /\ g e. T ) -> ( ( ( S o. U ) P ( S o. V ) ) ` g ) = ( ( ( S o. U ) ` g ) o. ( ( S o. V ) ` g ) ) )
44 41 42 24 43 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( ( S o. U ) P ( S o. V ) ) ` g ) = ( ( ( S o. U ) ` g ) o. ( ( S o. V ) ` g ) ) )
45 22 23 27 9 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( U P V ) e. E )
46 1 2 3 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ ( U P V ) e. E ) /\ g e. T ) -> ( ( S o. ( U P V ) ) ` g ) = ( S ` ( ( U P V ) ` g ) ) )
47 22 21 45 24 46 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S o. ( U P V ) ) ` g ) = ( S ` ( ( U P V ) ` g ) ) )
48 40 44 47 3eqtr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) /\ g e. T ) -> ( ( S o. ( U P V ) ) ` g ) = ( ( ( S o. U ) P ( S o. V ) ) ` g ) )
49 48 ralrimiva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> A. g e. T ( ( S o. ( U P V ) ) ` g ) = ( ( ( S o. U ) P ( S o. V ) ) ` g ) )
50 1 2 3 tendoeq1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S o. ( U P V ) ) e. E /\ ( ( S o. U ) P ( S o. V ) ) e. E ) /\ A. g e. T ( ( S o. ( U P V ) ) ` g ) = ( ( ( S o. U ) P ( S o. V ) ) ` g ) ) -> ( S o. ( U P V ) ) = ( ( S o. U ) P ( S o. V ) ) )
51 5 12 18 49 50 syl121anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. ( U P V ) ) = ( ( S o. U ) P ( S o. V ) ) )