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

Metamath Proof Explorer

Theorem lvecvsn0

Description: A scalar product is nonzero iff both of its factors are nonzero. (Contributed by NM, 3-Jan-2015)

Ref Expression
Hypotheses lvecmul0or.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lvecmul0or.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lvecmul0or.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lvecmul0or.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lvecmul0or.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
lvecmul0or.z ⊢ 0 = ( 0g ‘ 𝑊 )
lvecmul0or.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lvecmul0or.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
lvecmul0or.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion lvecvsn0 ( 𝜑 → ( ( 𝐴 · 𝑋 ) ≠ 0 ↔ ( 𝐴 ≠ 𝑂 ∧ 𝑋 ≠ 0 ) ) )

Proof

Step Hyp Ref Expression
1 lvecmul0or.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lvecmul0or.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lvecmul0or.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lvecmul0or.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lvecmul0or.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
6 lvecmul0or.z ⊢ 0 = ( 0g ‘ 𝑊 )
7 lvecmul0or.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lvecmul0or.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9 lvecmul0or.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 1 2 3 4 5 6 7 8 9 lvecvs0or ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )
11 10 necon3abid ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ≠ 0 ↔ ¬ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )
12 neanior ⊢ ( ( 𝐴 ≠ 𝑂 ∧ 𝑋 ≠ 0 ) ↔ ¬ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) )
13 11 12 bitr4di ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ≠ 0 ↔ ( 𝐴 ≠ 𝑂 ∧ 𝑋 ≠ 0 ) ) )