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	$$⊢V={\mathrm{Base}}_W$$
	lvecmul0or.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lvecmul0or.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lvecmul0or.k	$$⊢K={\mathrm{Base}}_F$$
	lvecmul0or.o	$$⊢O=0_F$$
	lvecmul0or.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lvecmul0or.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lvecmul0or.a	$$⊢\phi \to A\in K$$
	lvecmul0or.x	$$⊢\phi \to X\in V$$
Assertion	lvecvsn0	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}\leftrightarrow \left(A\ne O\wedge X\ne \underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lvecmul0or.v	$$⊢V={\mathrm{Base}}_W$$
2		lvecmul0or.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lvecmul0or.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lvecmul0or.k	$$⊢K={\mathrm{Base}}_F$$
5		lvecmul0or.o	$$⊢O=0_F$$
6		lvecmul0or.z	$$⊢\underset{\dot{}}{0}=0_W$$
7		lvecmul0or.w	$$⊢\phi \to W\in \mathrm{LVec}$$
8		lvecmul0or.a	$$⊢\phi \to A\in K$$
9		lvecmul0or.x	$$⊢\phi \to X\in V$$
10	1 2 3 4 5 6 7 8 9	lvecvs0or	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow \left(A=O\vee X=\underset{\dot{}}{0}\right)\right)$$
11	10	necon3abid	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}\leftrightarrow \neg \left(A=O\vee X=\underset{\dot{}}{0}\right)\right)$$
12		neanior	$$⊢\left(A\ne O\wedge X\ne \underset{\dot{}}{0}\right)\leftrightarrow \neg \left(A=O\vee X=\underset{\dot{}}{0}\right)$$
13	11 12	bitr4di	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}\leftrightarrow \left(A\ne O\wedge X\ne \underset{\dot{}}{0}\right)\right)$$