Metamath Proof Explorer


Theorem lcd0vs

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

Ref Expression
Hypotheses lcd0vs.h 𝐻 = ( LHyp ‘ 𝐾 )
lcd0vs.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcd0vs.r 𝑅 = ( Scalar ‘ 𝑈 )
lcd0vs.z 0 = ( 0g𝑅 )
lcd0vs.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
lcd0vs.v 𝑉 = ( Base ‘ 𝐶 )
lcd0vs.t · = ( ·𝑠𝐶 )
lcd0vs.o 𝑂 = ( 0g𝐶 )
lcd0vs.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcd0vs.g ( 𝜑𝐺𝑉 )
Assertion lcd0vs ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )

Proof

Step Hyp Ref Expression
1 lcd0vs.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcd0vs.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 lcd0vs.r 𝑅 = ( Scalar ‘ 𝑈 )
4 lcd0vs.z 0 = ( 0g𝑅 )
5 lcd0vs.c 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 lcd0vs.v 𝑉 = ( Base ‘ 𝐶 )
7 lcd0vs.t · = ( ·𝑠𝐶 )
8 lcd0vs.o 𝑂 = ( 0g𝐶 )
9 lcd0vs.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 lcd0vs.g ( 𝜑𝐺𝑉 )
11 eqid ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
12 eqid ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) )
13 1 2 3 4 5 11 12 9 lcd0 ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = 0 )
14 13 oveq1d ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = ( 0 · 𝐺 ) )
15 1 5 9 lcdlmod ( 𝜑𝐶 ∈ LMod )
16 6 11 7 12 8 lmod0vs ( ( 𝐶 ∈ LMod ∧ 𝐺𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = 𝑂 )
17 15 10 16 syl2anc ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = 𝑂 )
18 14 17 eqtr3d ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )