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 + 𝐺 ) )