Theorem lfl0sc

Description: The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014)

	Ref	Expression
Hypotheses	lfl0sc.v	$$⊢V={\mathrm{Base}}_W$$
	lfl0sc.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lfl0sc.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lfl0sc.k	$$⊢K={\mathrm{Base}}_D$$
	lfl0sc.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lfl0sc.o	$$⊢\underset{\dot{}}{0}=0_D$$
	lfl0sc.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lfl0sc.g	$$⊢\phi \to G\in F$$
Assertion	lfl0sc	$$⊢\phi \to G{\underset{\dot{}}{·}}_f\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=V\times \left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lfl0sc.v	$$⊢V={\mathrm{Base}}_W$$
2		lfl0sc.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
3		lfl0sc.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
4		lfl0sc.k	$$⊢K={\mathrm{Base}}_D$$
5		lfl0sc.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
6		lfl0sc.o	$$⊢\underset{\dot{}}{0}=0_D$$
7		lfl0sc.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		lfl0sc.g	$$⊢\phi \to G\in F$$
9	1	fvexi	$$⊢V\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to V\in \mathrm{V}$$
11	2 4 1 3	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:V⟶K$$
12	7 8 11	syl2anc	$$⊢\phi \to G:V⟶K$$
13	2	lmodring	$$⊢W\in \mathrm{LMod}\to D\in \mathrm{Ring}$$
14	7 13	syl	$$⊢\phi \to D\in \mathrm{Ring}$$
15	4 6	ring0cl	$$⊢D\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
16	14 15	syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
17	4 5 6	ringrz	$$⊢\left(D\in \mathrm{Ring}\wedge k\in K\right)\to k\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
18	14 17	sylan	$$⊢\left(\phi \wedge k\in K\right)\to k\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
19	10 12 16 16 18	caofid1	$$⊢\phi \to G{\underset{\dot{}}{·}}_f\left(V\times \left\{\underset{\dot{}}{0}\right\}\right)=V\times \left\{\underset{\dot{}}{0}\right\}$$