lfladdcom

Description: Commutativity 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$
Assertion	lfladdcom	$⊢ φ \to G {\underset{˙}{+}}_{f} H = H {\underset{˙}{+}}_{f} G$

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		fvexd	$⊢ φ \to {Base}_{W} \in V$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ {Base}_{W} = {Base}_{W}$
10	1 8 9 3	lflf	$⊢ (W \in LMod \land G \in F) \to G : {Base}_{W} ⟶ {Base}_{R}$
11	4 5 10	syl2anc	$⊢ φ \to G : {Base}_{W} ⟶ {Base}_{R}$
12	1 8 9 3	lflf	$⊢ (W \in LMod \land H \in F) \to H : {Base}_{W} ⟶ {Base}_{R}$
13	4 6 12	syl2anc	$⊢ φ \to H : {Base}_{W} ⟶ {Base}_{R}$
14	1	lmodring	$⊢ W \in LMod \to R \in Ring$
15		ringabl	$⊢ R \in Ring \to R \in Abel$
16	4 14 15	3syl	$⊢ φ \to R \in Abel$
17	16	adantr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to R \in Abel$
18		simprl	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \in {Base}_{R}$
19		simprr	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to y \in {Base}_{R}$
20	8 2	ablcom	$⊢ (R \in Abel \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
21	17 18 19 20	syl3anc	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \underset{˙}{+} y = y \underset{˙}{+} x$
22	7 11 13 21	caofcom	$⊢ φ \to G {\underset{˙}{+}}_{f} H = H {\underset{˙}{+}}_{f} G$

Metamath Proof Explorer