Metamath Proof Explorer


Theorem tendoplcom

Description: The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013)

Ref Expression
Hypotheses tendopl.h 𝐻 = ( LHyp ‘ 𝐾 )
tendopl.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendopl.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendopl.p 𝑃 = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) )
Assertion tendoplcom ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑉 𝑃 𝑈 ) )

Proof

Step Hyp Ref Expression
1 tendopl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 tendopl.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendopl.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendopl.p 𝑃 = ( 𝑠𝐸 , 𝑡𝐸 ↦ ( 𝑓𝑇 ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) )
5 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 1 2 3 4 tendoplcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) → ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 )
7 1 2 3 4 tendoplcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑉𝐸𝑈𝐸 ) → ( 𝑉 𝑃 𝑈 ) ∈ 𝐸 )
8 7 3com23 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) → ( 𝑉 𝑃 𝑈 ) ∈ 𝐸 )
9 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → 𝑈𝐸 )
11 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → 𝑔𝑇 )
12 1 2 3 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑔𝑇 ) → ( 𝑈𝑔 ) ∈ 𝑇 )
13 9 10 11 12 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( 𝑈𝑔 ) ∈ 𝑇 )
14 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → 𝑉𝐸 )
15 1 2 3 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑉𝐸𝑔𝑇 ) → ( 𝑉𝑔 ) ∈ 𝑇 )
16 9 14 11 15 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( 𝑉𝑔 ) ∈ 𝑇 )
17 1 2 ltrncom ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝑔 ) ∈ 𝑇 ∧ ( 𝑉𝑔 ) ∈ 𝑇 ) → ( ( 𝑈𝑔 ) ∘ ( 𝑉𝑔 ) ) = ( ( 𝑉𝑔 ) ∘ ( 𝑈𝑔 ) ) )
18 9 13 16 17 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( ( 𝑈𝑔 ) ∘ ( 𝑉𝑔 ) ) = ( ( 𝑉𝑔 ) ∘ ( 𝑈𝑔 ) ) )
19 4 2 tendopl2 ( ( 𝑈𝐸𝑉𝐸𝑔𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑈𝑔 ) ∘ ( 𝑉𝑔 ) ) )
20 10 14 11 19 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑈𝑔 ) ∘ ( 𝑉𝑔 ) ) )
21 4 2 tendopl2 ( ( 𝑉𝐸𝑈𝐸𝑔𝑇 ) → ( ( 𝑉 𝑃 𝑈 ) ‘ 𝑔 ) = ( ( 𝑉𝑔 ) ∘ ( 𝑈𝑔 ) ) )
22 14 10 11 21 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( ( 𝑉 𝑃 𝑈 ) ‘ 𝑔 ) = ( ( 𝑉𝑔 ) ∘ ( 𝑈𝑔 ) ) )
23 18 20 22 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) ∧ 𝑔𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑉 𝑃 𝑈 ) ‘ 𝑔 ) )
24 23 ralrimiva ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) → ∀ 𝑔𝑇 ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑉 𝑃 𝑈 ) ‘ 𝑔 ) )
25 1 2 3 tendoeq1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑈 𝑃 𝑉 ) ∈ 𝐸 ∧ ( 𝑉 𝑃 𝑈 ) ∈ 𝐸 ) ∧ ∀ 𝑔𝑇 ( ( 𝑈 𝑃 𝑉 ) ‘ 𝑔 ) = ( ( 𝑉 𝑃 𝑈 ) ‘ 𝑔 ) ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑉 𝑃 𝑈 ) )
26 5 6 8 24 25 syl121anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝑉𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑉 𝑃 𝑈 ) )