lspsnss2

Description: Comparable spans of singletons must have proportional vectors. See lspsneq for equal span version. (Contributed by NM, 7-Jun-2015)

	Ref	Expression
Hypotheses	lspsnss2.v	$⊢ V = {Base}_{W}$
	lspsnss2.s	$⊢ S = Scalar (W)$
	lspsnss2.k	$⊢ K = {Base}_{S}$
	lspsnss2.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lspsnss2.n	$⊢ N = LSpan (W)$
	lspsnss2.w	$⊢ φ \to W \in LMod$
	lspsnss2.x	$⊢ φ \to X \in V$
	lspsnss2.y	$⊢ φ \to Y \in V$
Assertion	lspsnss2	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y\}) \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} Y)$

Step	Hyp	Ref	Expression
1		lspsnss2.v	$⊢ V = {Base}_{W}$
2		lspsnss2.s	$⊢ S = Scalar (W)$
3		lspsnss2.k	$⊢ K = {Base}_{S}$
4		lspsnss2.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		lspsnss2.n	$⊢ N = LSpan (W)$
6		lspsnss2.w	$⊢ φ \to W \in LMod$
7		lspsnss2.x	$⊢ φ \to X \in V$
8		lspsnss2.y	$⊢ φ \to Y \in V$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	1 9 5	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
11	6 8 10	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
12	1 9 5 6 11 7	ellspsn5b	$⊢ φ \to (X \in N (\{Y\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y\}))$
13	2 3 1 4 5	ellspsn	$⊢ (W \in LMod \land Y \in V) \to (X \in N (\{Y\}) \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} Y)$
14	6 8 13	syl2anc	$⊢ φ \to (X \in N (\{Y\}) \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} Y)$
15	12 14	bitr3d	$⊢ φ \to (N (\{X\}) \subseteq N (\{Y\}) \leftrightarrow \exists k \in K X = k \underset{˙}{\cdot} Y)$

Metamath Proof Explorer