Theorem lfladd0l

Description: Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	lfladd0l.v	|- V = ( Base ` W )
	lfladd0l.r	|- R = ( Scalar ` W )
	lfladd0l.p	|- .+ = ( +g ` R )
	lfladd0l.o	|- .0. = ( 0g ` R )
	lfladd0l.f	|- F = ( LFnl ` W )
	lfladd0l.w	|- ( ph -> W e. LMod )
	lfladd0l.g	|- ( ph -> G e. F )
Assertion	lfladd0l	|- ( ph -> ( ( V X. { .0. } ) oF .+ G ) = G )

Proof

Step	Hyp	Ref	Expression
1		lfladd0l.v	|- V = ( Base ` W )
2		lfladd0l.r	|- R = ( Scalar ` W )
3		lfladd0l.p	|- .+ = ( +g ` R )
4		lfladd0l.o	|- .0. = ( 0g ` R )
5		lfladd0l.f	|- F = ( LFnl ` W )
6		lfladd0l.w	|- ( ph -> W e. LMod )
7		lfladd0l.g	|- ( ph -> G e. F )
8	1	fvexi	|- V e. _V
9	8	a1i	|- ( ph -> V e. _V )
10		eqid	|- ( Base ` R ) = ( Base ` R )
11	2 10 1 5	lflf	|- ( ( W e. LMod /\ G e. F ) -> G : V --> ( Base ` R ) )
12	6 7 11	syl2anc	|- ( ph -> G : V --> ( Base ` R ) )
13	4	fvexi	|- .0. e. _V
14	13	a1i	|- ( ph -> .0. e. _V )
15	2	lmodring	|- ( W e. LMod -> R e. Ring )
16		ringgrp	|- ( R e. Ring -> R e. Grp )
17	6 15 16	3syl	|- ( ph -> R e. Grp )
18	10 3 4	grplid	|- ( ( R e. Grp /\ k e. ( Base ` R ) ) -> ( .0. .+ k ) = k )
19	17 18	sylan	|- ( ( ph /\ k e. ( Base ` R ) ) -> ( .0. .+ k ) = k )
20	9 12 14 19	caofid0l	|- ( ph -> ( ( V X. { .0. } ) oF .+ G ) = G )