ldual0vs

Description: Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015)

	Ref	Expression
Hypotheses	ldual0vs.f	$⊢ F = LFnl (W)$
	ldual0vs.r	$⊢ R = Scalar (W)$
	ldual0vs.z	$⊢ \underset{˙}{0} = 0_{R}$
	ldual0vs.d	$⊢ D = LDual (W)$
	ldual0vs.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	ldual0vs.o	$⊢ O = 0_{D}$
	ldual0vs.w	$⊢ φ \to W \in LMod$
	ldual0vs.g	$⊢ φ \to G \in F$
Assertion	ldual0vs	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} G = O$

Step	Hyp	Ref	Expression
1		ldual0vs.f	$⊢ F = LFnl (W)$
2		ldual0vs.r	$⊢ R = Scalar (W)$
3		ldual0vs.z	$⊢ \underset{˙}{0} = 0_{R}$
4		ldual0vs.d	$⊢ D = LDual (W)$
5		ldual0vs.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
6		ldual0vs.o	$⊢ O = 0_{D}$
7		ldual0vs.w	$⊢ φ \to W \in LMod$
8		ldual0vs.g	$⊢ φ \to G \in F$
9		eqid	$⊢ Scalar (D) = Scalar (D)$
10		eqid	$⊢ 0_{Scalar (D)} = 0_{Scalar (D)}$
11	2 3 4 9 10 7	ldual0	$⊢ φ \to 0_{Scalar (D)} = \underset{˙}{0}$
12	11	oveq1d	$⊢ φ \to 0_{Scalar (D)} \underset{˙}{\cdot} G = \underset{˙}{0} \underset{˙}{\cdot} G$
13	4 7	lduallmod	$⊢ φ \to D \in LMod$
14		eqid	$⊢ {Base}_{D} = {Base}_{D}$
15	1 4 14 7 8	ldualelvbase	$⊢ φ \to G \in {Base}_{D}$
16	14 9 5 10 6	lmod0vs	$⊢ (D \in LMod \land G \in {Base}_{D}) \to 0_{Scalar (D)} \underset{˙}{\cdot} G = O$
17	13 15 16	syl2anc	$⊢ φ \to 0_{Scalar (D)} \underset{˙}{\cdot} G = O$
18	12 17	eqtr3d	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} G = O$

Metamath Proof Explorer