Theorem lfladdcom

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

	Ref	Expression
Hypotheses	lfladdcl.r	|- R = ( Scalar ` W )
	lfladdcl.p	|- .+ = ( +g ` R )
	lfladdcl.f	|- F = ( LFnl ` W )
	lfladdcl.w	|- ( ph -> W e. LMod )
	lfladdcl.g	|- ( ph -> G e. F )
	lfladdcl.h	|- ( ph -> H e. F )
Assertion	lfladdcom	|- ( ph -> ( G oF .+ H ) = ( H oF .+ G ) )

Proof

Step	Hyp	Ref	Expression
1		lfladdcl.r	|- R = ( Scalar ` W )
2		lfladdcl.p	|- .+ = ( +g ` R )
3		lfladdcl.f	|- F = ( LFnl ` W )
4		lfladdcl.w	|- ( ph -> W e. LMod )
5		lfladdcl.g	|- ( ph -> G e. F )
6		lfladdcl.h	|- ( ph -> H e. F )
7		fvexd	|- ( ph -> ( Base ` W ) e. _V )
8		eqid	|- ( Base ` R ) = ( Base ` R )
9		eqid	|- ( Base ` W ) = ( Base ` W )
10	1 8 9 3	lflf	|- ( ( W e. LMod /\ G e. F ) -> G : ( Base ` W ) --> ( Base ` R ) )
11	4 5 10	syl2anc	|- ( ph -> G : ( Base ` W ) --> ( Base ` R ) )
12	1 8 9 3	lflf	|- ( ( W e. LMod /\ H e. F ) -> H : ( Base ` W ) --> ( Base ` R ) )
13	4 6 12	syl2anc	|- ( ph -> H : ( Base ` W ) --> ( Base ` R ) )
14	1	lmodring	|- ( W e. LMod -> R e. Ring )
15		ringabl	|- ( R e. Ring -> R e. Abel )
16	4 14 15	3syl	|- ( ph -> R e. Abel )
17	16	adantr	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> R e. Abel )
18		simprl	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> x e. ( Base ` R ) )
19		simprr	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> y e. ( Base ` R ) )
20	8 2	ablcom	|- ( ( R e. Abel /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .+ y ) = ( y .+ x ) )
21	17 18 19 20	syl3anc	|- ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x .+ y ) = ( y .+ x ) )
22	7 11 13 21	caofcom	|- ( ph -> ( G oF .+ H ) = ( H oF .+ G ) )