Metamath Proof Explorer

Theorem lfladdcom

Description: Commutativity of functional addition. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses lfladdcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
lfladdcl.p ⊢ + = ( +g ‘ 𝑅 )
lfladdcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lfladdcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lfladdcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lfladdcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
Assertion lfladdcom ( 𝜑 → ( 𝐺 ∘f + 𝐻 ) = ( 𝐻 ∘f + 𝐺 ) )

Proof

Step Hyp Ref Expression
1 lfladdcl.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
2 lfladdcl.p ⊢ + = ( +g ‘ 𝑅 )
3 lfladdcl.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lfladdcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lfladdcl.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
6 lfladdcl.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
7 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) ∈ V )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 1 8 9 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
11 4 5 10 syl2anc ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
12 1 8 9 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ) → 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
13 4 6 12 syl2anc ⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
14 1 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
15 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
16 4 14 15 3syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Abel )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
19 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
20 8 2 ablcom ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
21 17 18 19 20 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
22 7 11 13 21 caofcom ⊢ ( 𝜑 → ( 𝐺 ∘f + 𝐻 ) = ( 𝐻 ∘f + 𝐺 ) )