prjspvs

Description: A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-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	prjspvs	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to (N \underset{˙}{\cdot} X) \underset{˙}{\sim} X$

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		eqid	$⊢ {Base}_{V} = {Base}_{V}$
8		lveclmod	$⊢ V \in LVec \to V \in LMod$
9	8	3ad2ant1	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to V \in LMod$
10		eldifi	$⊢ N \in (K ∖ \{\underset{˙}{0}\}) \to N \in K$
11	10	3ad2ant3	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to N \in K$
12		difss	$⊢ {Base}_{V} ∖ \{0_{V}\} \subseteq {Base}_{V}$
13	2 12	eqsstri	$⊢ B \subseteq {Base}_{V}$
14	13	sseli	$⊢ X \in B \to X \in {Base}_{V}$
15	14	3ad2ant2	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to X \in {Base}_{V}$
16	7 3 4 5 9 11 15	lmodvscld	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to N \underset{˙}{\cdot} X \in {Base}_{V}$
17		eldifsni	$⊢ N \in (K ∖ \{\underset{˙}{0}\}) \to N \neq \underset{˙}{0}$
18	17	3ad2ant3	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to N \neq \underset{˙}{0}$
19		eldifsni	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \neq 0_{V}$
20	19 2	eleq2s	$⊢ X \in B \to X \neq 0_{V}$
21	20	3ad2ant2	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to X \neq 0_{V}$
22		eqid	$⊢ 0_{V} = 0_{V}$
23		simp1	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to V \in LVec$
24	7 4 3 5 6 22 23 11 15	lvecvsn0	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to (N \underset{˙}{\cdot} X \neq 0_{V} \leftrightarrow (N \neq \underset{˙}{0} \land X \neq 0_{V}))$
25	18 21 24	mpbir2and	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to N \underset{˙}{\cdot} X \neq 0_{V}$
26	16 25	eldifsnd	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to N \underset{˙}{\cdot} X \in ({Base}_{V} ∖ \{0_{V}\})$
27	26 2	eleqtrrdi	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to N \underset{˙}{\cdot} X \in B$
28		simp2	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to X \in B$
29		oveq1	$⊢ N = m \to N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X$
30	29	eqcoms	$⊢ m = N \to N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X$
31		tbtru	$⊢ N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X \leftrightarrow (N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X \leftrightarrow ⊤)$
32	30 31	sylib	$⊢ m = N \to (N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X \leftrightarrow ⊤)$
33		trud	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to ⊤$
34	32 11 33	rspcedvdw	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to \exists m \in K N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X$
35	1	prjsprel	$⊢ (N \underset{˙}{\cdot} X) \underset{˙}{\sim} X \leftrightarrow ((N \underset{˙}{\cdot} X \in B \land X \in B) \land \exists m \in K N \underset{˙}{\cdot} X = m \underset{˙}{\cdot} X)$
36	27 28 34 35	syl21anbrc	$⊢ (V \in LVec \land X \in B \land N \in (K ∖ \{\underset{˙}{0}\})) \to (N \underset{˙}{\cdot} X) \underset{˙}{\sim} X$

Metamath Proof Explorer

Theorem prjspvs

Proof