Theorem lvecvs0or

Description: If a scalar product is zero, one of its factors must be zero. ( hvmul0or analog.) (Contributed by NM, 2-Jul-2014)

	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	lvecvs0or	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow \left(A=O\vee X=\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		df-ne	$$⊢A\ne O\leftrightarrow \neg A=O$$
11		oveq2	$$⊢A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)={inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}$$
12	11	ad2antlr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)={inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}$$
13	7	adantr	$$⊢\left(\phi \wedge A\ne O\right)\to W\in \mathrm{LVec}$$
14	3	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
15	13 14	syl	$$⊢\left(\phi \wedge A\ne O\right)\to F\in \mathrm{DivRing}$$
16	8	adantr	$$⊢\left(\phi \wedge A\ne O\right)\to A\in K$$
17		simpr	$$⊢\left(\phi \wedge A\ne O\right)\to A\ne O$$
18		eqid	$$⊢{\cdot }_F={\cdot }_F$$
19		eqid	$$⊢1_F=1_F$$
20		eqid	$$⊢{inv}_r\left(F\right)={inv}_r\left(F\right)$$
21	4 5 18 19 20	drnginvrl	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right){\cdot }_{F}A=1_F$$
22	15 16 17 21	syl3anc	$$⊢\left(\phi \wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right){\cdot }_{F}A=1_F$$
23	22	oveq1d	$$⊢\left(\phi \wedge A\ne O\right)\to \left({inv}_r\left(F\right)\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}X=1_F\underset{\dot{}}{·}X$$
24		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
25	7 24	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
26	25	adantr	$$⊢\left(\phi \wedge A\ne O\right)\to W\in \mathrm{LMod}$$
27	4 5 20	drnginvrcl	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\in K$$
28	15 16 17 27	syl3anc	$$⊢\left(\phi \wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\in K$$
29	9	adantr	$$⊢\left(\phi \wedge A\ne O\right)\to X\in V$$
30	1 3 2 4 18	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left({inv}_r\left(F\right)\left(A\right)\in K\wedge A\in K\wedge X\in V\right)\right)\to \left({inv}_r\left(F\right)\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}X={inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)$$
31	26 28 16 29 30	syl13anc	$$⊢\left(\phi \wedge A\ne O\right)\to \left({inv}_r\left(F\right)\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}X={inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)$$
32	1 3 2 19	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to 1_F\underset{\dot{}}{·}X=X$$
33	25 9 32	syl2anc	$$⊢\phi \to 1_F\underset{\dot{}}{·}X=X$$
34	33	adantr	$$⊢\left(\phi \wedge A\ne O\right)\to 1_F\underset{\dot{}}{·}X=X$$
35	23 31 34	3eqtr3d	$$⊢\left(\phi \wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)=X$$
36	35	adantlr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)=X$$
37	25	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\to W\in \mathrm{LMod}$$
38	37	adantr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\wedge A\ne O\right)\to W\in \mathrm{LMod}$$
39	28	adantlr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\in K$$
40	3 2 4 6	lmodvs0	$$⊢\left(W\in \mathrm{LMod}\wedge {inv}_r\left(F\right)\left(A\right)\in K\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
41	38 39 40	syl2anc	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\wedge A\ne O\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
42	12 36 41	3eqtr3d	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\wedge A\ne O\right)\to X=\underset{\dot{}}{0}$$
43	42	ex	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\to \left(A\ne O\to X=\underset{\dot{}}{0}\right)$$
44	10 43	biimtrrid	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\to \left(\neg A=O\to X=\underset{\dot{}}{0}\right)$$
45	44	orrd	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)\to \left(A=O\vee X=\underset{\dot{}}{0}\right)$$
46	45	ex	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\to \left(A=O\vee X=\underset{\dot{}}{0}\right)\right)$$
47	1 3 2 5 6	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
48	25 9 47	syl2anc	$$⊢\phi \to O\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
49		oveq1	$$⊢A=O\to A\underset{\dot{}}{·}X=O\underset{\dot{}}{·}X$$
50	49	eqeq1d	$$⊢A=O\to \left(A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow O\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
51	48 50	syl5ibrcom	$$⊢\phi \to \left(A=O\to A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
52	3 2 4 6	lmodvs0	$$⊢\left(W\in \mathrm{LMod}\wedge A\in K\right)\to A\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
53	25 8 52	syl2anc	$$⊢\phi \to A\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
54		oveq2	$$⊢X=\underset{\dot{}}{0}\to A\underset{\dot{}}{·}X=A\underset{\dot{}}{·}\underset{\dot{}}{0}$$
55	54	eqeq1d	$$⊢X=\underset{\dot{}}{0}\to \left(A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow A\underset{\dot{}}{·}\underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
56	53 55	syl5ibrcom	$$⊢\phi \to \left(X=\underset{\dot{}}{0}\to A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
57	51 56	jaod	$$⊢\phi \to \left(\left(A=O\vee X=\underset{\dot{}}{0}\right)\to A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\right)$$
58	46 57	impbid	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow \left(A=O\vee X=\underset{\dot{}}{0}\right)\right)$$