Theorem lvecvscan

Description: Cancellation law for scalar multiplication. ( hvmulcan analog.) (Contributed by NM, 2-Jul-2014)

	Ref	Expression
Hypotheses	lvecmulcan.v	$$⊢V={\mathrm{Base}}_W$$
	lvecmulcan.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lvecmulcan.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lvecmulcan.k	$$⊢K={\mathrm{Base}}_F$$
	lvecmulcan.o	$$⊢\underset{\dot{}}{0}=0_F$$
	lvecmulcan.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lvecmulcan.a	$$⊢\phi \to A\in K$$
	lvecmulcan.x	$$⊢\phi \to X\in V$$
	lvecmulcan.y	$$⊢\phi \to Y\in V$$
	lvecmulcan.n	$$⊢\phi \to A\ne \underset{\dot{}}{0}$$
Assertion	lvecvscan	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=A\underset{\dot{}}{·}Y\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		lvecmulcan.v	$$⊢V={\mathrm{Base}}_W$$
2		lvecmulcan.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lvecmulcan.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lvecmulcan.k	$$⊢K={\mathrm{Base}}_F$$
5		lvecmulcan.o	$$⊢\underset{\dot{}}{0}=0_F$$
6		lvecmulcan.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lvecmulcan.a	$$⊢\phi \to A\in K$$
8		lvecmulcan.x	$$⊢\phi \to X\in V$$
9		lvecmulcan.y	$$⊢\phi \to Y\in V$$
10		lvecmulcan.n	$$⊢\phi \to A\ne \underset{\dot{}}{0}$$
11		df-ne	$$⊢A\ne \underset{\dot{}}{0}\leftrightarrow \neg A=\underset{\dot{}}{0}$$
12		biorf	$$⊢\neg A=\underset{\dot{}}{0}\to \left(X{-}_{W}Y=0_W\leftrightarrow \left(A=\underset{\dot{}}{0}\vee X{-}_{W}Y=0_W\right)\right)$$
13	11 12	sylbi	$$⊢A\ne \underset{\dot{}}{0}\to \left(X{-}_{W}Y=0_W\leftrightarrow \left(A=\underset{\dot{}}{0}\vee X{-}_{W}Y=0_W\right)\right)$$
14	10 13	syl	$$⊢\phi \to \left(X{-}_{W}Y=0_W\leftrightarrow \left(A=\underset{\dot{}}{0}\vee X{-}_{W}Y=0_W\right)\right)$$
15		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
16	6 15	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
17		eqid	$$⊢0_W=0_W$$
18		eqid	$$⊢{-}_W={-}_W$$
19	1 17 18	lmodsubeq0	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to \left(X{-}_{W}Y=0_W\leftrightarrow X=Y\right)$$
20	16 8 9 19	syl3anc	$$⊢\phi \to \left(X{-}_{W}Y=0_W\leftrightarrow X=Y\right)$$
21	1 2 3 4 18 16 7 8 9	lmodsubdi	$$⊢\phi \to A\underset{\dot{}}{·}\left(X{-}_{W}Y\right)=\left(A\underset{\dot{}}{·}X\right){-}_W\left(A\underset{\dot{}}{·}Y\right)$$
22	21	eqeq1d	$$⊢\phi \to \left(A\underset{\dot{}}{·}\left(X{-}_{W}Y\right)=0_W\leftrightarrow \left(A\underset{\dot{}}{·}X\right){-}_W\left(A\underset{\dot{}}{·}Y\right)=0_W\right)$$
23	1 18	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X{-}_{W}Y\in V$$
24	16 8 9 23	syl3anc	$$⊢\phi \to X{-}_{W}Y\in V$$
25	1 2 3 4 5 17 6 7 24	lvecvs0or	$$⊢\phi \to \left(A\underset{\dot{}}{·}\left(X{-}_{W}Y\right)=0_W\leftrightarrow \left(A=\underset{\dot{}}{0}\vee X{-}_{W}Y=0_W\right)\right)$$
26	1 3 2 4	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in K\wedge X\in V\right)\to A\underset{\dot{}}{·}X\in V$$
27	16 7 8 26	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}X\in V$$
28	1 3 2 4	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in K\wedge Y\in V\right)\to A\underset{\dot{}}{·}Y\in V$$
29	16 7 9 28	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}Y\in V$$
30	1 17 18	lmodsubeq0	$$⊢\left(W\in \mathrm{LMod}\wedge A\underset{\dot{}}{·}X\in V\wedge A\underset{\dot{}}{·}Y\in V\right)\to \left(\left(A\underset{\dot{}}{·}X\right){-}_W\left(A\underset{\dot{}}{·}Y\right)=0_W\leftrightarrow A\underset{\dot{}}{·}X=A\underset{\dot{}}{·}Y\right)$$
31	16 27 29 30	syl3anc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{·}X\right){-}_W\left(A\underset{\dot{}}{·}Y\right)=0_W\leftrightarrow A\underset{\dot{}}{·}X=A\underset{\dot{}}{·}Y\right)$$
32	22 25 31	3bitr3d	$$⊢\phi \to \left(\left(A=\underset{\dot{}}{0}\vee X{-}_{W}Y=0_W\right)\leftrightarrow A\underset{\dot{}}{·}X=A\underset{\dot{}}{·}Y\right)$$
33	14 20 32	3bitr3rd	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=A\underset{\dot{}}{·}Y\leftrightarrow X=Y\right)$$