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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcdvs0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcdvs0.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
lcdvs0.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
lcdvs0.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcdvs0.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
lcdvs0.o ⊢ 0 = ( 0g ‘ 𝐶 )
lcdvs0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcdvs0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion lcdvs0N ( 𝜑 → ( 𝑋 · 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 lcdvs0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcdvs0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcdvs0.s ⊢ 𝑆 = ( Scalar ‘ 𝑈 )
4 lcdvs0.r ⊢ 𝑅 = ( Base ‘ 𝑆 )
5 lcdvs0.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 lcdvs0.t ⊢ · = ( ·𝑠 ‘ 𝐶 )
7 lcdvs0.o ⊢ 0 = ( 0g ‘ 𝐶 )
8 lcdvs0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 lcdvs0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
10 1 5 8 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
11 eqid ⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐶 ) ) = ( Base ‘ ( Scalar ‘ 𝐶 ) )
13 1 2 3 4 5 11 12 8 lcdsbase ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐶 ) ) = 𝑅 )
14 9 13 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) )
15 11 6 12 7 lmodvs0 ⊢ ( ( 𝐶 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐶 ) ) ) → ( 𝑋 · 0 ) = 0 )
16 10 14 15 syl2anc ⊢ ( 𝜑 → ( 𝑋 · 0 ) = 0 )