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