lvecvscan2

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

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

Proof

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

Metamath Proof Explorer

Theorem lvecvscan2

Proof