Metamath Proof Explorer

Theorem tendoplcom

Description: The endomorphism sum operation is commutative. (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 tendoplcom ⊢K∈HL∧W∈H∧U∈E∧V∈E→UPV=VPU

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 simp1 ⊢K∈HL∧W∈H∧U∈E∧V∈E→K∈HL∧W∈H
6 1 2 3 4 tendoplcl ⊢K∈HL∧W∈H∧U∈E∧V∈E→UPV∈E
7 1 2 3 4 tendoplcl ⊢K∈HL∧W∈H∧V∈E∧U∈E→VPU∈E
8 7 3com23 ⊢K∈HL∧W∈H∧U∈E∧V∈E→VPU∈E
9 simpl1 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→K∈HL∧W∈H
10 simpl2 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→U∈E
11 simpr ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→g∈T
12 1 2 3 tendocl ⊢K∈HL∧W∈H∧U∈E∧g∈T→U⁡g∈T
13 9 10 11 12 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→U⁡g∈T
14 simpl3 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→V∈E
15 1 2 3 tendocl ⊢K∈HL∧W∈H∧V∈E∧g∈T→V⁡g∈T
16 9 14 11 15 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→V⁡g∈T
17 1 2 ltrncom ⊢K∈HL∧W∈H∧U⁡g∈T∧V⁡g∈T→U⁡g∘V⁡g=V⁡g∘U⁡g
18 9 13 16 17 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→U⁡g∘V⁡g=V⁡g∘U⁡g
19 4 2 tendopl2 ⊢U∈E∧V∈E∧g∈T→UPV⁡g=U⁡g∘V⁡g
20 10 14 11 19 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→UPV⁡g=U⁡g∘V⁡g
21 4 2 tendopl2 ⊢V∈E∧U∈E∧g∈T→VPU⁡g=V⁡g∘U⁡g
22 14 10 11 21 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→VPU⁡g=V⁡g∘U⁡g
23 18 20 22 3eqtr4d ⊢K∈HL∧W∈H∧U∈E∧V∈E∧g∈T→UPV⁡g=VPU⁡g
24 23 ralrimiva ⊢K∈HL∧W∈H∧U∈E∧V∈E→∀g∈TUPV⁡g=VPU⁡g
25 1 2 3 tendoeq1 ⊢K∈HL∧W∈H∧UPV∈E∧VPU∈E∧∀g∈TUPV⁡g=VPU⁡g→UPV=VPU
26 5 6 8 24 25 syl121anc ⊢K∈HL∧W∈H∧U∈E∧V∈E→UPV=VPU