Metamath Proof Explorer


Theorem lcdvs0N

Description: A scalar times the zero functional is the zero functional. (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcdvs0.h H = LHyp K
lcdvs0.u U = DVecH K W
lcdvs0.s S = Scalar U
lcdvs0.r R = Base S
lcdvs0.c C = LCDual K W
lcdvs0.t · ˙ = C
lcdvs0.o 0 ˙ = 0 C
lcdvs0.k φ K HL W H
lcdvs0.x φ X R
Assertion lcdvs0N φ X · ˙ 0 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 lcdvs0.h H = LHyp K
2 lcdvs0.u U = DVecH K W
3 lcdvs0.s S = Scalar U
4 lcdvs0.r R = Base S
5 lcdvs0.c C = LCDual K W
6 lcdvs0.t · ˙ = C
7 lcdvs0.o 0 ˙ = 0 C
8 lcdvs0.k φ K HL W H
9 lcdvs0.x φ X R
10 1 5 8 lcdlmod φ C LMod
11 eqid Scalar C = Scalar C
12 eqid Base Scalar C = Base Scalar C
13 1 2 3 4 5 11 12 8 lcdsbase φ Base Scalar C = R
14 9 13 eleqtrrd φ X Base Scalar C
15 11 6 12 7 lmodvs0 C LMod X Base Scalar C X · ˙ 0 ˙ = 0 ˙
16 10 14 15 syl2anc φ X · ˙ 0 ˙ = 0 ˙