Metamath Proof Explorer

Theorem lflsc0N

Description: The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lflsc0.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lflsc0.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lflsc0.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
4 lflsc0.t ⊢ · = ( .r ‘ 𝐷 )
5 lflsc0.o ⊢ 0 = ( 0g ‘ 𝐷 )
6 lflsc0.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 lflsc0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
8 1 fvexi ⊢ 𝑉 ∈ V
9 8 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
10 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Ring )
11 6 10 syl ⊢ ( 𝜑 → 𝐷 ∈ Ring )
12 3 5 ring0cl ⊢ ( 𝐷 ∈ Ring → 0 ∈ 𝐾 )
13 11 12 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
14 9 13 7 ofc12 ⊢ ( 𝜑 → ( ( 𝑉 × { 0 } ) ∘f · ( 𝑉 × { 𝑋 } ) ) = ( 𝑉 × { ( 0 · 𝑋 ) } ) )
15 3 4 5 ringlz ⊢ ( ( 𝐷 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 0 · 𝑋 ) = 0 )
16 11 7 15 syl2anc ⊢ ( 𝜑 → ( 0 · 𝑋 ) = 0 )
17 16 sneqd ⊢ ( 𝜑 → { ( 0 · 𝑋 ) } = { 0 } )
18 17 xpeq2d ⊢ ( 𝜑 → ( 𝑉 × { ( 0 · 𝑋 ) } ) = ( 𝑉 × { 0 } ) )
19 14 18 eqtrd ⊢ ( 𝜑 → ( ( 𝑉 × { 0 } ) ∘f · ( 𝑉 × { 𝑋 } ) ) = ( 𝑉 × { 0 } ) )