prjspreln0

Description: Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023)

	Ref	Expression
Hypotheses	prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
	prjspertr.b	$⊢ B = {Base}_{V} ∖ \{0_{V}\}$
	prjspertr.s	$⊢ S = Scalar (V)$
	prjspertr.x	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
	prjspertr.k	$⊢ K = {Base}_{S}$
	prjspreln0.z	$⊢ \underset{˙}{0} = 0_{S}$
Assertion	prjspreln0	$⊢ V \in LVec \to (X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y))$

Proof

Step	Hyp	Ref	Expression
1		prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
2		prjspertr.b	$⊢ B = {Base}_{V} ∖ \{0_{V}\}$
3		prjspertr.s	$⊢ S = Scalar (V)$
4		prjspertr.x	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
5		prjspertr.k	$⊢ K = {Base}_{S}$
6		prjspreln0.z	$⊢ \underset{˙}{0} = 0_{S}$
7	1	prjsprel	$⊢ X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y)$
8		simprl	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to m \in K$
9		simplrl	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to X \in B$
10		eldifsni	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \neq 0_{V}$
11	10 2	eleq2s	$⊢ X \in B \to X \neq 0_{V}$
12	9 11	syl	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to X \neq 0_{V}$
13		simplrr	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to X = m \underset{˙}{\cdot} Y$
14		simpr	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to m = \underset{˙}{0}$
15	14	oveq1d	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to m \underset{˙}{\cdot} Y = \underset{˙}{0} \underset{˙}{\cdot} Y$
16		lveclmod	$⊢ V \in LVec \to V \in LMod$
17	16	ad3antrrr	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to V \in LMod$
18		difss	$⊢ {Base}_{V} ∖ \{0_{V}\} \subseteq {Base}_{V}$
19	2 18	eqsstri	$⊢ B \subseteq {Base}_{V}$
20		simplrr	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land ((m \in K \land X = m \underset{˙}{\cdot} Y) \land m = \underset{˙}{0})) \to Y \in B$
21	20	anassrs	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to Y \in B$
22	19 21	sselid	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to Y \in {Base}_{V}$
23		eqid	$⊢ {Base}_{V} = {Base}_{V}$
24		eqid	$⊢ 0_{V} = 0_{V}$
25	23 3 4 6 24	lmod0vs	$⊢ (V \in LMod \land Y \in {Base}_{V}) \to \underset{˙}{0} \underset{˙}{\cdot} Y = 0_{V}$
26	17 22 25	syl2anc	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to \underset{˙}{0} \underset{˙}{\cdot} Y = 0_{V}$
27	13 15 26	3eqtrd	$⊢ (((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \land m = \underset{˙}{0}) \to X = 0_{V}$
28	12 27	mteqand	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to m \neq \underset{˙}{0}$
29		nelsn	$⊢ m \neq \underset{˙}{0} \to \neg m \in \{\underset{˙}{0}\}$
30	28 29	syl	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to \neg m \in \{\underset{˙}{0}\}$
31	8 30	eldifd	$⊢ ((V \in LVec \land (X \in B \land Y \in B)) \land (m \in K \land X = m \underset{˙}{\cdot} Y)) \to m \in (K ∖ \{\underset{˙}{0}\})$
32	31	ex	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to ((m \in K \land X = m \underset{˙}{\cdot} Y) \to m \in (K ∖ \{\underset{˙}{0}\}))$
33		simpr	$⊢ (m \in K \land X = m \underset{˙}{\cdot} Y) \to X = m \underset{˙}{\cdot} Y$
34	32 33	jca2	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to ((m \in K \land X = m \underset{˙}{\cdot} Y) \to (m \in (K ∖ \{\underset{˙}{0}\}) \land X = m \underset{˙}{\cdot} Y))$
35	34	reximdv2	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (\exists m \in K X = m \underset{˙}{\cdot} Y \to \exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y)$
36		difss	$⊢ K ∖ \{\underset{˙}{0}\} \subseteq K$
37		ssrexv	$⊢ K ∖ \{\underset{˙}{0}\} \subseteq K \to (\exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y \to \exists m \in K X = m \underset{˙}{\cdot} Y)$
38	36 37	mp1i	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (\exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y \to \exists m \in K X = m \underset{˙}{\cdot} Y)$
39	35 38	impbid	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (\exists m \in K X = m \underset{˙}{\cdot} Y \leftrightarrow \exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y)$
40	39	pm5.32da	$⊢ V \in LVec \to (((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y) \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y))$
41	7 40	bitrid	$⊢ V \in LVec \to (X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in (K ∖ \{\underset{˙}{0}\}) X = m \underset{˙}{\cdot} Y))$

Metamath Proof Explorer

Theorem prjspreln0

Proof