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 , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
Assertion tendodi2 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U ∘ V = S ∘ V P U ∘ 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 , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
5 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → K ∈ HL ∧ W ∈ H
6 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S ∈ E
7 simpr2 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → U ∈ E
8 1 2 3 4 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E → S P U ∈ E
9 5 6 7 8 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U ∈ E
10 simpr3 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → V ∈ E
11 1 3 tendococl ⊢ K ∈ HL ∧ W ∈ H ∧ S P U ∈ E ∧ V ∈ E → S P U ∘ V ∈ E
12 5 9 10 11 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U ∘ V ∈ E
13 1 3 tendococl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ V ∈ E → S ∘ V ∈ E
14 5 6 10 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S ∘ V ∈ E
15 1 3 tendococl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U ∘ V ∈ E
16 5 7 10 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → U ∘ V ∈ E
17 1 2 3 4 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∘ V ∈ E ∧ U ∘ V ∈ E → S ∘ V P U ∘ V ∈ E
18 5 14 16 17 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S ∘ V P U ∘ V ∈ E
19 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → K ∈ HL ∧ W ∈ H
20 simplr1 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ∈ E
21 simplr2 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U ∈ E
22 19 20 21 8 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ∈ E
23 simplr3 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → V ∈ E
24 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → g ∈ T
25 1 2 3 tendocoval ⊢ K ∈ HL ∧ W ∈ H ∧ S P U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ∘ V ⁡ g = S P U ⁡ V ⁡ g
26 19 22 23 24 25 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ∘ V ⁡ g = S P U ⁡ V ⁡ g
27 simplll ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → K ∈ HL
28 simpllr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → W ∈ H
29 1 2 3 tendocoval ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ V ∈ E ∧ g ∈ T → S ∘ V ⁡ g = S ⁡ V ⁡ g
30 27 28 20 23 24 29 syl221anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ∘ V ⁡ g = S ⁡ V ⁡ g
31 1 2 3 tendocoval ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U ∘ V ⁡ g = U ⁡ V ⁡ g
32 27 28 21 23 24 31 syl221anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U ∘ V ⁡ g = U ⁡ V ⁡ g
33 30 32 coeq12d ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ∘ V ⁡ g ∘ U ∘ V ⁡ g = S ⁡ V ⁡ g ∘ U ⁡ V ⁡ g
34 19 20 23 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ∘ V ∈ E
35 19 21 23 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U ∘ V ∈ E
36 4 2 tendopl2 ⊢ S ∘ V ∈ E ∧ U ∘ V ∈ E ∧ g ∈ T → S ∘ V P U ∘ V ⁡ g = S ∘ V ⁡ g ∘ U ∘ V ⁡ g
37 34 35 24 36 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ∘ V P U ∘ V ⁡ g = S ∘ V ⁡ g ∘ U ∘ V ⁡ g
38 1 2 3 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ g ∈ T → V ⁡ g ∈ T
39 19 23 24 38 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → V ⁡ g ∈ T
40 4 2 tendopl2 ⊢ S ∈ E ∧ U ∈ E ∧ V ⁡ g ∈ T → S P U ⁡ V ⁡ g = S ⁡ V ⁡ g ∘ U ⁡ V ⁡ g
41 20 21 39 40 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ⁡ V ⁡ g = S ⁡ V ⁡ g ∘ U ⁡ V ⁡ g
42 33 37 41 3eqtr4rd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ⁡ V ⁡ g = S ∘ V P U ∘ V ⁡ g
43 26 42 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ∘ V ⁡ g = S ∘ V P U ∘ V ⁡ g
44 43 ralrimiva ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → ∀ g ∈ T S P U ∘ V ⁡ g = S ∘ V P U ∘ V ⁡ g
45 1 2 3 tendoeq1 ⊢ K ∈ HL ∧ W ∈ H ∧ S P U ∘ V ∈ E ∧ S ∘ V P U ∘ V ∈ E ∧ ∀ g ∈ T S P U ∘ V ⁡ g = S ∘ V P U ∘ V ⁡ g → S P U ∘ V = S ∘ V P U ∘ V
46 5 12 18 44 45 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U ∘ V = S ∘ V P U ∘ V