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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑉 𝑃 𝑈 ) )