Theorem lssvs0or

Description: If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015)

	Ref	Expression
Hypotheses	lssvs0or.v	$$⊢V={\mathrm{Base}}_W$$
	lssvs0or.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lssvs0or.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lssvs0or.k	$$⊢K={\mathrm{Base}}_F$$
	lssvs0or.o	$$⊢\underset{\dot{}}{0}=0_F$$
	lssvs0or.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lssvs0or.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lssvs0or.u	$$⊢\phi \to U\in S$$
	lssvs0or.x	$$⊢\phi \to X\in V$$
	lssvs0or.a	$$⊢\phi \to A\in K$$
Assertion	lssvs0or	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\in U\leftrightarrow \left(A=\underset{\dot{}}{0}\vee X\in U\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lssvs0or.v	$$⊢V={\mathrm{Base}}_W$$
2		lssvs0or.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lssvs0or.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lssvs0or.k	$$⊢K={\mathrm{Base}}_F$$
5		lssvs0or.o	$$⊢\underset{\dot{}}{0}=0_F$$
6		lssvs0or.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
7		lssvs0or.w	$$⊢\phi \to W\in \mathrm{LVec}$$
8		lssvs0or.u	$$⊢\phi \to U\in S$$
9		lssvs0or.x	$$⊢\phi \to X\in V$$
10		lssvs0or.a	$$⊢\phi \to A\in K$$
11	3	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
12	7 11	syl	$$⊢\phi \to F\in \mathrm{DivRing}$$
13	12	ad2antrr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to F\in \mathrm{DivRing}$$
14	10	ad2antrr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to A\in K$$
15		simpr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to A\ne \underset{\dot{}}{0}$$
16		eqid	$$⊢{\cdot }_F={\cdot }_F$$
17		eqid	$$⊢1_F=1_F$$
18		eqid	$$⊢{inv}_r\left(F\right)={inv}_r\left(F\right)$$
19	4 5 16 17 18	drnginvrl	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(F\right)\left(A\right){\cdot }_{F}A=1_F$$
20	13 14 15 19	syl3anc	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(F\right)\left(A\right){\cdot }_{F}A=1_F$$
21	20	oveq1d	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to \left({inv}_r\left(F\right)\left(A\right){\cdot }_{F}A\right)\underset{\dot{}}{·}X=1_F\underset{\dot{}}{·}X$$
22		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
23	7 22	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
24	23	ad2antrr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to W\in \mathrm{LMod}$$
25	4 5 18	drnginvrcl	$$⊢\left(F\in \mathrm{DivRing}\wedge A\in K\wedge A\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(F\right)\left(A\right)\in K$$
26	13 14 15 25	syl3anc	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(F\right)\left(A\right)\in K$$
27	9	ad2antrr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to X\in V$$
28	1 3 2 4 16	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)$$
29	24 26 14 27 28	syl13anc	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\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)$$
30	1 3 2 17	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to 1_F\underset{\dot{}}{·}X=X$$
31	24 27 30	syl2anc	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to 1_F\underset{\dot{}}{·}X=X$$
32	21 29 31	3eqtr3rd	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to X={inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)$$
33	8	ad2antrr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to U\in S$$
34		simplr	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to A\underset{\dot{}}{·}X\in U$$
35	3 2 4 6	lssvscl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge U\in S\right)\wedge \left({inv}_r\left(F\right)\left(A\right)\in K\wedge A\underset{\dot{}}{·}X\in U\right)\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)\in U$$
36	24 33 26 34 35	syl22anc	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(F\right)\left(A\right)\underset{\dot{}}{·}\left(A\underset{\dot{}}{·}X\right)\in U$$
37	32 36	eqeltrd	$$⊢\left(\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\wedge A\ne \underset{\dot{}}{0}\right)\to X\in U$$
38	37	ex	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\to \left(A\ne \underset{\dot{}}{0}\to X\in U\right)$$
39	38	necon1bd	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\to \left(\neg X\in U\to A=\underset{\dot{}}{0}\right)$$
40	39	orrd	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\to \left(X\in U\vee A=\underset{\dot{}}{0}\right)$$
41	40	orcomd	$$⊢\left(\phi \wedge A\underset{\dot{}}{·}X\in U\right)\to \left(A=\underset{\dot{}}{0}\vee X\in U\right)$$
42		oveq1	$$⊢A=\underset{\dot{}}{0}\to A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\underset{\dot{}}{·}X$$
43	42	adantl	$$⊢\left(\phi \wedge A=\underset{\dot{}}{0}\right)\to A\underset{\dot{}}{·}X=\underset{\dot{}}{0}\underset{\dot{}}{·}X$$
44		eqid	$$⊢0_W=0_W$$
45	1 3 2 5 44	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}X=0_W$$
46	23 9 45	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}X=0_W$$
47	44 6	lss0cl	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to 0_W\in U$$
48	23 8 47	syl2anc	$$⊢\phi \to 0_W\in U$$
49	46 48	eqeltrd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{·}X\in U$$
50	49	adantr	$$⊢\left(\phi \wedge A=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{·}X\in U$$
51	43 50	eqeltrd	$$⊢\left(\phi \wedge A=\underset{\dot{}}{0}\right)\to A\underset{\dot{}}{·}X\in U$$
52	23	adantr	$$⊢\left(\phi \wedge X\in U\right)\to W\in \mathrm{LMod}$$
53	8	adantr	$$⊢\left(\phi \wedge X\in U\right)\to U\in S$$
54	10	adantr	$$⊢\left(\phi \wedge X\in U\right)\to A\in K$$
55		simpr	$$⊢\left(\phi \wedge X\in U\right)\to X\in U$$
56	3 2 4 6	lssvscl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge U\in S\right)\wedge \left(A\in K\wedge X\in U\right)\right)\to A\underset{\dot{}}{·}X\in U$$
57	52 53 54 55 56	syl22anc	$$⊢\left(\phi \wedge X\in U\right)\to A\underset{\dot{}}{·}X\in U$$
58	51 57	jaodan	$$⊢\left(\phi \wedge \left(A=\underset{\dot{}}{0}\vee X\in U\right)\right)\to A\underset{\dot{}}{·}X\in U$$
59	41 58	impbida	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\in U\leftrightarrow \left(A=\underset{\dot{}}{0}\vee X\in U\right)\right)$$