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 , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
Assertion tendoplass ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ 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 , 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 2 3 4 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ S P U ∈ E ∧ V ∈ E → S P U P V ∈ E
12 5 9 10 11 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U P V ∈ E
13 1 2 3 4 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U P V ∈ E
14 5 7 10 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → U P V ∈ E
15 1 2 3 4 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U P V ∈ E → S P U P V ∈ E
16 5 6 14 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U P V ∈ E
17 coass ⊢ S ⁡ g ∘ U ⁡ g ∘ V ⁡ g = S ⁡ g ∘ U ⁡ g ∘ V ⁡ g
18 simplr1 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ∈ E
19 simplr2 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U ∈ E
20 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → g ∈ T
21 4 2 tendopl2 ⊢ S ∈ E ∧ U ∈ E ∧ g ∈ T → S P U ⁡ g = S ⁡ g ∘ U ⁡ g
22 18 19 20 21 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ⁡ g = S ⁡ g ∘ U ⁡ g
23 22 coeq1d ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ⁡ g ∘ V ⁡ g = S ⁡ g ∘ U ⁡ g ∘ V ⁡ g
24 simplr3 ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → V ∈ E
25 4 2 tendopl2 ⊢ U ∈ E ∧ V ∈ E ∧ g ∈ T → U P V ⁡ g = U ⁡ g ∘ V ⁡ g
26 19 24 20 25 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U P V ⁡ g = U ⁡ g ∘ V ⁡ g
27 26 coeq2d ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S ⁡ g ∘ U P V ⁡ g = S ⁡ g ∘ U ⁡ g ∘ V ⁡ g
28 17 23 27 3eqtr4a ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ⁡ g ∘ V ⁡ g = S ⁡ g ∘ U P V ⁡ g
29 9 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U ∈ E
30 4 2 tendopl2 ⊢ S P U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U P V ⁡ g = S P U ⁡ g ∘ V ⁡ g
31 29 24 20 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U P V ⁡ g = S P U ⁡ g ∘ V ⁡ g
32 14 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U P V ∈ E
33 4 2 tendopl2 ⊢ S ∈ E ∧ U P V ∈ E ∧ g ∈ T → S P U P V ⁡ g = S ⁡ g ∘ U P V ⁡ g
34 18 32 20 33 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U P V ⁡ g = S ⁡ g ∘ U P V ⁡ g
35 28 31 34 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → S P U P V ⁡ g = S P U P V ⁡ g
36 35 ralrimiva ⊢ K ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → ∀ g ∈ T S P U P V ⁡ g = S P U P V ⁡ g
37 1 2 3 tendoeq1 ⊢ K ∈ HL ∧ W ∈ H ∧ S P U P V ∈ E ∧ S P U P V ∈ E ∧ ∀ g ∈ 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 ∈ HL ∧ W ∈ H ∧ S ∈ E ∧ U ∈ E ∧ V ∈ E → S P U P V = S P U P V