Theorem lfladd0l

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

	Ref	Expression
Hypotheses	lfladd0l.v	$$⊢V={\mathrm{Base}}_W$$
	lfladd0l.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	lfladd0l.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	lfladd0l.o	$$⊢\underset{\dot{}}{0}=0_R$$
	lfladd0l.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lfladd0l.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lfladd0l.g	$$⊢\phi \to G\in F$$
Assertion	lfladd0l	$$⊢\phi \to \left(V\times \left\{\underset{\dot{}}{0}\right\}\right){\underset{\dot{}}{+}}_{f}G=G$$

Proof

Step	Hyp	Ref	Expression
1		lfladd0l.v	$$⊢V={\mathrm{Base}}_W$$
2		lfladd0l.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		lfladd0l.p	$$⊢\underset{\dot{}}{+}={+}_R$$
4		lfladd0l.o	$$⊢\underset{\dot{}}{0}=0_R$$
5		lfladd0l.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
6		lfladd0l.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lfladd0l.g	$$⊢\phi \to G\in F$$
8	1	fvexi	$$⊢V\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to V\in \mathrm{V}$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	2 10 1 5	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:V⟶{\mathrm{Base}}_R$$
12	6 7 11	syl2anc	$$⊢\phi \to G:V⟶{\mathrm{Base}}_R$$
13	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
15	2	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
16		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
17	6 15 16	3syl	$$⊢\phi \to R\in \mathrm{Grp}$$
18	10 3 4	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge k\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}k=k$$
19	17 18	sylan	$$⊢\left(\phi \wedge k\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}k=k$$
20	9 12 14 19	caofid0l	$$⊢\phi \to \left(V\times \left\{\underset{\dot{}}{0}\right\}\right){\underset{\dot{}}{+}}_{f}G=G$$