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 → U P V = V P U

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 → U P V ∈ E
7 1 2 3 4 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ U ∈ E → V P U ∈ E
8 7 3com23 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → V P U ∈ 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 → U P V ⁡ g = U ⁡ g ∘ V ⁡ g
20 10 14 11 19 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U P V ⁡ g = U ⁡ g ∘ V ⁡ g
21 4 2 tendopl2 ⊢ V ∈ E ∧ U ∈ E ∧ g ∈ T → V P U ⁡ g = V ⁡ g ∘ U ⁡ g
22 14 10 11 21 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → V P U ⁡ g = V ⁡ g ∘ U ⁡ g
23 18 20 22 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ g ∈ T → U P V ⁡ g = V P U ⁡ g
24 23 ralrimiva ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → ∀ g ∈ T U P V ⁡ g = V P U ⁡ g
25 1 2 3 tendoeq1 ⊢ K ∈ HL ∧ W ∈ H ∧ U P V ∈ E ∧ V P U ∈ E ∧ ∀ g ∈ T U P V ⁡ g = V P U ⁡ g → U P V = V P U
26 5 6 8 24 25 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E → U P V = V P U