Theorem lvecvscan2

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

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

Proof

Step	Hyp	Ref	Expression
1		lvecmulcan2.v	$$⊢V={\mathrm{Base}}_W$$
2		lvecmulcan2.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lvecmulcan2.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lvecmulcan2.k	$$⊢K={\mathrm{Base}}_F$$
5		lvecmulcan2.o	$$⊢\underset{\dot{}}{0}=0_W$$
6		lvecmulcan2.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		lvecmulcan2.a	$$⊢\phi \to A\in K$$
8		lvecmulcan2.b	$$⊢\phi \to B\in K$$
9		lvecmulcan2.x	$$⊢\phi \to X\in V$$
10		lvecmulcan2.n	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
11	10	neneqd	$$⊢\phi \to \neg X=\underset{\dot{}}{0}$$
12		biorf	$$⊢\neg X=\underset{\dot{}}{0}\to \left(A{-}_{F}B=0_F\leftrightarrow \left(X=\underset{\dot{}}{0}\vee A{-}_{F}B=0_F\right)\right)$$
13		orcom	$$⊢\left(X=\underset{\dot{}}{0}\vee A{-}_{F}B=0_F\right)\leftrightarrow \left(A{-}_{F}B=0_F\vee X=\underset{\dot{}}{0}\right)$$
14	12 13	bitrdi	$$⊢\neg X=\underset{\dot{}}{0}\to \left(A{-}_{F}B=0_F\leftrightarrow \left(A{-}_{F}B=0_F\vee X=\underset{\dot{}}{0}\right)\right)$$
15	11 14	syl	$$⊢\phi \to \left(A{-}_{F}B=0_F\leftrightarrow \left(A{-}_{F}B=0_F\vee X=\underset{\dot{}}{0}\right)\right)$$
16		eqid	$$⊢0_F=0_F$$
17		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
18	6 17	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
19	3	lmodfgrp	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Grp}$$
20	18 19	syl	$$⊢\phi \to F\in \mathrm{Grp}$$
21		eqid	$$⊢{-}_F={-}_F$$
22	4 21	grpsubcl	$$⊢\left(F\in \mathrm{Grp}\wedge A\in K\wedge B\in K\right)\to A{-}_{F}B\in K$$
23	20 7 8 22	syl3anc	$$⊢\phi \to A{-}_{F}B\in K$$
24	1 2 3 4 16 5 6 23 9	lvecvs0or	$$⊢\phi \to \left(\left(A{-}_{F}B\right)\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow \left(A{-}_{F}B=0_F\vee X=\underset{\dot{}}{0}\right)\right)$$
25		eqid	$$⊢{-}_W={-}_W$$
26	1 2 3 4 25 21 18 7 8 9	lmodsubdir	$$⊢\phi \to \left(A{-}_{F}B\right)\underset{\dot{}}{·}X=\left(A\underset{\dot{}}{·}X\right){-}_W\left(B\underset{\dot{}}{·}X\right)$$
27	26	eqeq1d	$$⊢\phi \to \left(\left(A{-}_{F}B\right)\underset{\dot{}}{·}X=\underset{\dot{}}{0}\leftrightarrow \left(A\underset{\dot{}}{·}X\right){-}_W\left(B\underset{\dot{}}{·}X\right)=\underset{\dot{}}{0}\right)$$
28	15 24 27	3bitr2rd	$$⊢\phi \to \left(\left(A\underset{\dot{}}{·}X\right){-}_W\left(B\underset{\dot{}}{·}X\right)=\underset{\dot{}}{0}\leftrightarrow A{-}_{F}B=0_F\right)$$
29	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$$
30	18 7 9 29	syl3anc	$$⊢\phi \to A\underset{\dot{}}{·}X\in V$$
31	1 3 2 4	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge B\in K\wedge X\in V\right)\to B\underset{\dot{}}{·}X\in V$$
32	18 8 9 31	syl3anc	$$⊢\phi \to B\underset{\dot{}}{·}X\in V$$
33	1 5 25	lmodsubeq0	$$⊢\left(W\in \mathrm{LMod}\wedge A\underset{\dot{}}{·}X\in V\wedge B\underset{\dot{}}{·}X\in V\right)\to \left(\left(A\underset{\dot{}}{·}X\right){-}_W\left(B\underset{\dot{}}{·}X\right)=\underset{\dot{}}{0}\leftrightarrow A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}X\right)$$
34	18 30 32 33	syl3anc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{·}X\right){-}_W\left(B\underset{\dot{}}{·}X\right)=\underset{\dot{}}{0}\leftrightarrow A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}X\right)$$
35	4 16 21	grpsubeq0	$$⊢\left(F\in \mathrm{Grp}\wedge A\in K\wedge B\in K\right)\to \left(A{-}_{F}B=0_F\leftrightarrow A=B\right)$$
36	20 7 8 35	syl3anc	$$⊢\phi \to \left(A{-}_{F}B=0_F\leftrightarrow A=B\right)$$
37	28 34 36	3bitr3d	$$⊢\phi \to \left(A\underset{\dot{}}{·}X=B\underset{\dot{}}{·}X\leftrightarrow A=B\right)$$