lspsneu

Description: Nonzero vectors with equal singleton spans have a unique proportionality constant. (Contributed by NM, 31-May-2015)

	Ref	Expression
Hypotheses	lspsneu.v	$⊢ V = {Base}_{W}$
	lspsneu.s	$⊢ S = Scalar (W)$
	lspsneu.k	$⊢ K = {Base}_{S}$
	lspsneu.o	$⊢ O = 0_{S}$
	lspsneu.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lspsneu.z	$⊢ \underset{˙}{0} = 0_{W}$
	lspsneu.n	$⊢ N = LSpan (W)$
	lspsneu.w	$⊢ φ \to W \in LVec$
	lspsneu.x	$⊢ φ \to X \in V$
	lspsneu.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
Assertion	lspsneu	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists! k \in (K ∖ \{O\}) X = k \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		lspsneu.v	$⊢ V = {Base}_{W}$
2		lspsneu.s	$⊢ S = Scalar (W)$
3		lspsneu.k	$⊢ K = {Base}_{S}$
4		lspsneu.o	$⊢ O = 0_{S}$
5		lspsneu.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lspsneu.z	$⊢ \underset{˙}{0} = 0_{W}$
7		lspsneu.n	$⊢ N = LSpan (W)$
8		lspsneu.w	$⊢ φ \to W \in LVec$
9		lspsneu.x	$⊢ φ \to X \in V$
10		lspsneu.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
11	10	eldifad	$⊢ φ \to Y \in V$
12	1 2 3 4 5 7 8 9 11	lspsneq	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y)$
13	12	biimpd	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to \exists j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y)$
14		eqtr2	$⊢ (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y) \to j \underset{˙}{\cdot} Y = i \underset{˙}{\cdot} Y$
15	14	3ad2ant3	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to j \underset{˙}{\cdot} Y = i \underset{˙}{\cdot} Y$
16		simp1l	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to φ$
17	16 8	syl	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to W \in LVec$
18		simp2l	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to j \in (K ∖ \{O\})$
19	18	eldifad	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to j \in K$
20		simp2r	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to i \in (K ∖ \{O\})$
21	20	eldifad	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to i \in K$
22	16 11	syl	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to Y \in V$
23		eldifsni	$⊢ Y \in (V ∖ \{\underset{˙}{0}\}) \to Y \neq \underset{˙}{0}$
24	16 10 23	3syl	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to Y \neq \underset{˙}{0}$
25	1 5 2 3 6 17 19 21 22 24	lvecvscan2	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to (j \underset{˙}{\cdot} Y = i \underset{˙}{\cdot} Y \leftrightarrow j = i)$
26	15 25	mpbid	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land (j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \land (X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y)) \to j = i$
27	26	3exp	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to ((j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \to ((X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y) \to j = i))$
28	27	ex	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to ((j \in (K ∖ \{O\}) \land i \in (K ∖ \{O\})) \to ((X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y) \to j = i)))$
29	28	ralrimdvv	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to \forall j \in (K ∖ \{O\}) \forall i \in (K ∖ \{O\}) ((X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y) \to j = i))$
30	13 29	jcad	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to (\exists j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y \land \forall j \in (K ∖ \{O\}) \forall i \in (K ∖ \{O\}) ((X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y) \to j = i)))$
31		oveq1	$⊢ j = i \to j \underset{˙}{\cdot} Y = i \underset{˙}{\cdot} Y$
32	31	eqeq2d	$⊢ j = i \to (X = j \underset{˙}{\cdot} Y \leftrightarrow X = i \underset{˙}{\cdot} Y)$
33	32	reu4	$⊢ \exists! j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y \leftrightarrow (\exists j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y \land \forall j \in (K ∖ \{O\}) \forall i \in (K ∖ \{O\}) ((X = j \underset{˙}{\cdot} Y \land X = i \underset{˙}{\cdot} Y) \to j = i))$
34	30 33	syl6ibr	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to \exists! j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y)$
35		reurex	$⊢ \exists! j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y \to \exists j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y$
36	35 12	syl5ibr	$⊢ φ \to (\exists! j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y \to N (\{X\}) = N (\{Y\}))$
37	34 36	impbid	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists! j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y)$
38		oveq1	$⊢ j = k \to j \underset{˙}{\cdot} Y = k \underset{˙}{\cdot} Y$
39	38	eqeq2d	$⊢ j = k \to (X = j \underset{˙}{\cdot} Y \leftrightarrow X = k \underset{˙}{\cdot} Y)$
40	39	cbvreuvw	$⊢ \exists! j \in (K ∖ \{O\}) X = j \underset{˙}{\cdot} Y \leftrightarrow \exists! k \in (K ∖ \{O\}) X = k \underset{˙}{\cdot} Y$
41	37 40	bitrdi	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists! k \in (K ∖ \{O\}) X = k \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem lspsneu

Proof