prjsprellsp

Description: Two vectors are equivalent iff their spans are equal. (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}$
	prjsprellsp.n	$⊢ N = LSpan (V)$
Assertion	prjsprellsp	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (X \underset{˙}{\sim} Y \leftrightarrow N (\{X\}) = N (\{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		prjsprellsp.n	$⊢ N = LSpan (V)$
7		ibar	$⊢ (X \in B \land Y \in B) \to (\exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y))$
8	7	bicomd	$⊢ (X \in B \land Y \in B) \to (((X \in B \land Y \in B) \land \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y) \leftrightarrow \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y)$
9	8	adantl	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (((X \in B \land Y \in B) \land \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y) \leftrightarrow \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y)$
10		eqid	$⊢ 0_{S} = 0_{S}$
11	1 2 3 4 5 10	prjspreln0	$⊢ V \in LVec \to (X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y))$
12	11	adantr	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y))$
13		eqid	$⊢ {Base}_{V} = {Base}_{V}$
14		simpl	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to V \in LVec$
15		eldifi	$⊢ X \in ({Base}_{V} ∖ \{0_{V}\}) \to X \in {Base}_{V}$
16	15 2	eleq2s	$⊢ X \in B \to X \in {Base}_{V}$
17	16	ad2antrl	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to X \in {Base}_{V}$
18		eldifi	$⊢ Y \in ({Base}_{V} ∖ \{0_{V}\}) \to Y \in {Base}_{V}$
19	18 2	eleq2s	$⊢ Y \in B \to Y \in {Base}_{V}$
20	19	ad2antll	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to Y \in {Base}_{V}$
21	13 3 5 10 4 6 14 17 20	lspsneq	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists m \in (K ∖ \{0_{S}\}) X = m \underset{˙}{\cdot} Y)$
22	9 12 21	3bitr4d	$⊢ (V \in LVec \land (X \in B \land Y \in B)) \to (X \underset{˙}{\sim} Y \leftrightarrow N (\{X\}) = N (\{Y\}))$

Metamath Proof Explorer

Theorem prjsprellsp

Proof