Metamath Proof Explorer

Theorem lfladdass

Description: Associativity 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 ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
lfladdass.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐹 )
Assertion lfladdass ( 𝜑 → ( ( 𝐺 ∘f + 𝐻 ) ∘f + 𝐼 ) = ( 𝐺 ∘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 lfladdass.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐹 )
8 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) ∈ V )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
11 1 9 10 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
12 4 5 11 syl2anc ⊢ ( 𝜑 → 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
13 1 9 10 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ) → 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
14 4 6 13 syl2anc ⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
15 1 9 10 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝐹 ) → 𝐼 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
16 4 7 15 syl2anc ⊢ ( 𝜑 → 𝐼 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑅 ) )
17 1 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
18 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
19 4 17 18 3syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
20 9 2 grpass ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
21 19 20 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
22 8 12 14 16 21 caofass ⊢ ( 𝜑 → ( ( 𝐺 ∘f + 𝐻 ) ∘f + 𝐼 ) = ( 𝐺 ∘f + ( 𝐻 ∘f + 𝐼 ) ) )