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

Metamath Proof Explorer

Theorem lfl0sc

Description: The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of ( V X. { .0. } ) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014)

Ref Expression
Hypotheses lfl0sc.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lfl0sc.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lfl0sc.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lfl0sc.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lfl0sc.t ⊢ · = ( .r ‘ 𝐷 )
lfl0sc.o ⊢ 0 = ( 0g ‘ 𝐷 )
lfl0sc.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lfl0sc.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lfl0sc ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) )

Proof

Step Hyp Ref Expression
1 lfl0sc.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lfl0sc.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lfl0sc.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lfl0sc.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
5 lfl0sc.t ⊢ · = ( .r ‘ 𝐷 )
6 lfl0sc.o ⊢ 0 = ( 0g ‘ 𝐷 )
7 lfl0sc.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
8 lfl0sc.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 1 fvexi ⊢ 𝑉 ∈ V
10 9 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
11 2 4 1 3 lflf ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
12 7 8 11 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
13 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
14 7 13 syl ⊢ ( 𝜑 → 𝐷 ∈ Ring )
15 4 6 ring0cl ⊢ ( 𝐷 ∈ Ring → 0 ∈ 𝐾 )
16 14 15 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
17 4 5 6 ringrz ⊢ ( ( 𝐷 ∈ Ring ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 0 ) = 0 )
18 14 17 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑘 · 0 ) = 0 )
19 10 12 16 16 18 caofid1 ⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 0 } ) ) = ( 𝑉 × { 0 } ) )