This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ldual0vs

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

Ref Expression
Hypotheses ldual0vs.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
ldual0vs.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
ldual0vs.z ⊢ 0 = ( 0g ‘ 𝑅 )
ldual0vs.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldual0vs.t ⊢ · = ( ·𝑠 ‘ 𝐷 )
ldual0vs.o ⊢ 𝑂 = ( 0g ‘ 𝐷 )
ldual0vs.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldual0vs.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion ldual0vs ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )

Proof

Step Hyp Ref Expression
1 ldual0vs.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 ldual0vs.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3 ldual0vs.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 ldual0vs.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
5 ldual0vs.t ⊢ · = ( ·𝑠 ‘ 𝐷 )
6 ldual0vs.o ⊢ 𝑂 = ( 0g ‘ 𝐷 )
7 ldual0vs.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 ldual0vs.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 eqid ⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
10 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
11 2 3 4 9 10 7 ldual0 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = 0 )
12 11 oveq1d ⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = ( 0 · 𝐺 ) )
13 4 7 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
14 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
15 1 4 14 7 8 ldualelvbase ⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
16 14 9 5 10 6 lmod0vs ⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = 𝑂 )
17 13 15 16 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = 𝑂 )
18 12 17 eqtr3d ⊢ ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )