Theorem lfladdass

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

	Ref	Expression
Hypotheses	lfladdcl.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	lfladdcl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	lfladdcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lfladdcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lfladdcl.g	$$⊢\phi \to G\in F$$
	lfladdcl.h	$$⊢\phi \to H\in F$$
	lfladdass.i	$$⊢\phi \to I\in F$$
Assertion	lfladdass	$$⊢\phi \to \left(G{\underset{\dot{}}{+}}_{f}H\right){\underset{\dot{}}{+}}_{f}I=G{\underset{\dot{}}{+}}_f\left(H{\underset{\dot{}}{+}}_{f}I\right)$$

Proof

Step	Hyp	Ref	Expression
1		lfladdcl.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		lfladdcl.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		lfladdcl.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
4		lfladdcl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lfladdcl.g	$$⊢\phi \to G\in F$$
6		lfladdcl.h	$$⊢\phi \to H\in F$$
7		lfladdass.i	$$⊢\phi \to I\in F$$
8		fvexd	$$⊢\phi \to {\mathrm{Base}}_W\in \mathrm{V}$$
9		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
10		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
11	1 9 10 3	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_R$$
12	4 5 11	syl2anc	$$⊢\phi \to G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_R$$
13	1 9 10 3	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge H\in F\right)\to H:{\mathrm{Base}}_W⟶{\mathrm{Base}}_R$$
14	4 6 13	syl2anc	$$⊢\phi \to H:{\mathrm{Base}}_W⟶{\mathrm{Base}}_R$$
15	1 9 10 3	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge I\in F\right)\to I:{\mathrm{Base}}_W⟶{\mathrm{Base}}_R$$
16	4 7 15	syl2anc	$$⊢\phi \to I:{\mathrm{Base}}_W⟶{\mathrm{Base}}_R$$
17	1	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
18		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
19	4 17 18	3syl	$$⊢\phi \to R\in \mathrm{Grp}$$
20	9 2	grpass	$$⊢\left(R\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\wedge z\in {\mathrm{Base}}_R\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
21	19 20	sylan	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\wedge z\in {\mathrm{Base}}_R\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
22	8 12 14 16 21	caofass	$$⊢\phi \to \left(G{\underset{\dot{}}{+}}_{f}H\right){\underset{\dot{}}{+}}_{f}I=G{\underset{\dot{}}{+}}_f\left(H{\underset{\dot{}}{+}}_{f}I\right)$$