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 ) ) )