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 = {Base}_{W}$
	lvecmul0or.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lvecmul0or.f	$⊢ F = Scalar (W)$
	lvecmul0or.k	$⊢ K = {Base}_{F}$
	lvecmul0or.o	$⊢ O = 0_{F}$
	lvecmul0or.z	$⊢ \underset{˙}{0} = 0_{W}$
	lvecmul0or.w	$⊢ φ \to W \in LVec$
	lvecmul0or.a	$⊢ φ \to A \in K$
	lvecmul0or.x	$⊢ φ \to X \in V$
Assertion	lvecvsn0	$⊢ φ \to (A \underset{˙}{\cdot} X \neq \underset{˙}{0} \leftrightarrow (A \neq O \land X \neq \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		lvecmul0or.v	$⊢ V = {Base}_{W}$
2		lvecmul0or.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
3		lvecmul0or.f	$⊢ F = Scalar (W)$
4		lvecmul0or.k	$⊢ K = {Base}_{F}$
5		lvecmul0or.o	$⊢ O = 0_{F}$
6		lvecmul0or.z	$⊢ \underset{˙}{0} = 0_{W}$
7		lvecmul0or.w	$⊢ φ \to W \in LVec$
8		lvecmul0or.a	$⊢ φ \to A \in K$
9		lvecmul0or.x	$⊢ φ \to X \in V$
10	1 2 3 4 5 6 7 8 9	lvecvs0or	$⊢ φ \to (A \underset{˙}{\cdot} X = \underset{˙}{0} \leftrightarrow (A = O \lor X = \underset{˙}{0}))$
11	10	necon3abid	$⊢ φ \to (A \underset{˙}{\cdot} X \neq \underset{˙}{0} \leftrightarrow \neg (A = O \lor X = \underset{˙}{0}))$
12		neanior	$⊢ (A \neq O \land X \neq \underset{˙}{0}) \leftrightarrow \neg (A = O \lor X = \underset{˙}{0})$
13	11 12	bitr4di	$⊢ φ \to (A \underset{˙}{\cdot} X \neq \underset{˙}{0} \leftrightarrow (A \neq O \land X \neq \underset{˙}{0}))$

Metamath Proof Explorer