lvecvscan

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

	Ref	Expression
Hypotheses	lvecmulcan.v	$⊢ V = {Base}_{W}$
	lvecmulcan.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lvecmulcan.f	$⊢ F = Scalar (W)$
	lvecmulcan.k	$⊢ K = {Base}_{F}$
	lvecmulcan.o	$⊢ \underset{˙}{0} = 0_{F}$
	lvecmulcan.w	$⊢ φ \to W \in LVec$
	lvecmulcan.a	$⊢ φ \to A \in K$
	lvecmulcan.x	$⊢ φ \to X \in V$
	lvecmulcan.y	$⊢ φ \to Y \in V$
	lvecmulcan.n	$⊢ φ \to A \neq \underset{˙}{0}$
Assertion	lvecvscan	$⊢ φ \to (A \underset{˙}{\cdot} X = A \underset{˙}{\cdot} Y \leftrightarrow X = Y)$

Proof

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

Metamath Proof Explorer

Theorem lvecvscan

Proof