lfladdass

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

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

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

Metamath Proof Explorer