lspsneq

Description: Equal spans of singletons must have proportional vectors. See lspsnss2 for comparable span version. TODO: can proof be shortened? (Contributed by NM, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspsneq.v	$⊢ V = {Base}_{W}$
2		lspsneq.s	$⊢ S = Scalar (W)$
3		lspsneq.k	$⊢ K = {Base}_{S}$
4		lspsneq.o	$⊢ \underset{˙}{0} = 0_{S}$
5		lspsneq.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		lspsneq.n	$⊢ N = LSpan (W)$
7		lspsneq.w	$⊢ φ \to W \in LVec$
8		lspsneq.x	$⊢ φ \to X \in V$
9		lspsneq.y	$⊢ φ \to Y \in V$
10		lveclmod	$⊢ W \in LVec \to W \in LMod$
11	7 10	syl	$⊢ φ \to W \in LMod$
12	2	lmodring	$⊢ W \in LMod \to S \in Ring$
13		eqid	$⊢ 1_{S} = 1_{S}$
14	3 13	ringidcl	$⊢ S \in Ring \to 1_{S} \in K$
15	11 12 14	3syl	$⊢ φ \to 1_{S} \in K$
16	2	lvecdrng	$⊢ W \in LVec \to S \in DivRing$
17	4 13	drngunz	$⊢ S \in DivRing \to 1_{S} \neq \underset{˙}{0}$
18	7 16 17	3syl	$⊢ φ \to 1_{S} \neq \underset{˙}{0}$
19		eldifsn	$⊢ 1_{S} \in (K ∖ \{\underset{˙}{0}\}) \leftrightarrow (1_{S} \in K \land 1_{S} \neq \underset{˙}{0})$
20	15 18 19	sylanbrc	$⊢ φ \to 1_{S} \in (K ∖ \{\underset{˙}{0}\})$
21	20	ad2antrr	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y = 0_{W}) \to 1_{S} \in (K ∖ \{\underset{˙}{0}\})$
22		eqid	$⊢ 0_{W} = 0_{W}$
23	1 22	lmod0vcl	$⊢ W \in LMod \to 0_{W} \in V$
24	1 2 5 13	lmodvs1	$⊢ (W \in LMod \land 0_{W} \in V) \to 1_{S} \underset{˙}{\cdot} 0_{W} = 0_{W}$
25	11 23 24	syl2anc2	$⊢ φ \to 1_{S} \underset{˙}{\cdot} 0_{W} = 0_{W}$
26	25	ad2antrr	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y = 0_{W}) \to 1_{S} \underset{˙}{\cdot} 0_{W} = 0_{W}$
27		oveq2	$⊢ Y = 0_{W} \to 1_{S} \underset{˙}{\cdot} Y = 1_{S} \underset{˙}{\cdot} 0_{W}$
28	27	adantl	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y = 0_{W}) \to 1_{S} \underset{˙}{\cdot} Y = 1_{S} \underset{˙}{\cdot} 0_{W}$
29	11	adantr	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to W \in LMod$
30	8	adantr	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to X \in V$
31	9	adantr	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to Y \in V$
32		simpr	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to N (\{X\}) = N (\{Y\})$
33	1 22 6 29 30 31 32	lspsneq0b	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to (X = 0_{W} \leftrightarrow Y = 0_{W})$
34	33	biimpar	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y = 0_{W}) \to X = 0_{W}$
35	26 28 34	3eqtr4rd	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y = 0_{W}) \to X = 1_{S} \underset{˙}{\cdot} Y$
36		oveq1	$⊢ j = 1_{S} \to j \underset{˙}{\cdot} Y = 1_{S} \underset{˙}{\cdot} Y$
37	36	rspceeqv	$⊢ (1_{S} \in (K ∖ \{\underset{˙}{0}\}) \land X = 1_{S} \underset{˙}{\cdot} Y) \to \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y$
38	21 35 37	syl2anc	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y = 0_{W}) \to \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y$
39		eqimss	$⊢ N (\{X\}) = N (\{Y\}) \to N (\{X\}) \subseteq N (\{Y\})$
40	39	adantl	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to N (\{X\}) \subseteq N (\{Y\})$
41		eqid	$⊢ LSubSp (W) = LSubSp (W)$
42	1 41 6	lspsncl	$⊢ (W \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (W)$
43	11 9 42	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (W)$
44	43	adantr	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to N (\{Y\}) \in LSubSp (W)$
45	1 41 6 29 44 30	ellspsn5b	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to (X \in N (\{Y\}) \leftrightarrow N (\{X\}) \subseteq N (\{Y\}))$
46	40 45	mpbird	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to X \in N (\{Y\})$
47	2 3 1 5 6	ellspsn	$⊢ (W \in LMod \land Y \in V) \to (X \in N (\{Y\}) \leftrightarrow \exists j \in K X = j \underset{˙}{\cdot} Y)$
48	29 31 47	syl2anc	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to (X \in N (\{Y\}) \leftrightarrow \exists j \in K X = j \underset{˙}{\cdot} Y)$
49	46 48	mpbid	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to \exists j \in K X = j \underset{˙}{\cdot} Y$
50	49	adantr	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \to \exists j \in K X = j \underset{˙}{\cdot} Y$
51		simprl	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to j \in K$
52		simpr	$⊢ (j \in K \land X = j \underset{˙}{\cdot} Y) \to X = j \underset{˙}{\cdot} Y$
53	52	adantl	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to X = j \underset{˙}{\cdot} Y$
54	33	biimpd	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to (X = 0_{W} \to Y = 0_{W})$
55	54	necon3d	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to (Y \neq 0_{W} \to X \neq 0_{W})$
56	55	imp	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \to X \neq 0_{W}$
57	56	adantr	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to X \neq 0_{W}$
58	53 57	eqnetrrd	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to j \underset{˙}{\cdot} Y \neq 0_{W}$
59	7	adantr	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to W \in LVec$
60	59	ad2antrr	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to W \in LVec$
61	31	ad2antrr	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to Y \in V$
62	1 5 2 3 4 22 60 51 61	lvecvsn0	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to (j \underset{˙}{\cdot} Y \neq 0_{W} \leftrightarrow (j \neq \underset{˙}{0} \land Y \neq 0_{W}))$
63	58 62	mpbid	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to (j \neq \underset{˙}{0} \land Y \neq 0_{W})$
64	63	simpld	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to j \neq \underset{˙}{0}$
65		eldifsn	$⊢ j \in (K ∖ \{\underset{˙}{0}\}) \leftrightarrow (j \in K \land j \neq \underset{˙}{0})$
66	51 64 65	sylanbrc	$⊢ (((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \land (j \in K \land X = j \underset{˙}{\cdot} Y)) \to j \in (K ∖ \{\underset{˙}{0}\})$
67	50 66 53	reximssdv	$⊢ ((φ \land N (\{X\}) = N (\{Y\})) \land Y \neq 0_{W}) \to \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y$
68	38 67	pm2.61dane	$⊢ (φ \land N (\{X\}) = N (\{Y\})) \to \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y$
69	68	ex	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \to \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y)$
70	7	adantr	$⊢ (φ \land j \in (K ∖ \{\underset{˙}{0}\})) \to W \in LVec$
71		eldifi	$⊢ j \in (K ∖ \{\underset{˙}{0}\}) \to j \in K$
72	71	adantl	$⊢ (φ \land j \in (K ∖ \{\underset{˙}{0}\})) \to j \in K$
73		eldifsni	$⊢ j \in (K ∖ \{\underset{˙}{0}\}) \to j \neq \underset{˙}{0}$
74	73	adantl	$⊢ (φ \land j \in (K ∖ \{\underset{˙}{0}\})) \to j \neq \underset{˙}{0}$
75	9	adantr	$⊢ (φ \land j \in (K ∖ \{\underset{˙}{0}\})) \to Y \in V$
76	1 2 5 3 4 6	lspsnvs	$⊢ (W \in LVec \land (j \in K \land j \neq \underset{˙}{0}) \land Y \in V) \to N (\{j \underset{˙}{\cdot} Y\}) = N (\{Y\})$
77	70 72 74 75 76	syl121anc	$⊢ (φ \land j \in (K ∖ \{\underset{˙}{0}\})) \to N (\{j \underset{˙}{\cdot} Y\}) = N (\{Y\})$
78	77	ex	$⊢ φ \to (j \in (K ∖ \{\underset{˙}{0}\}) \to N (\{j \underset{˙}{\cdot} Y\}) = N (\{Y\}))$
79		sneq	$⊢ X = j \underset{˙}{\cdot} Y \to \{X\} = \{j \underset{˙}{\cdot} Y\}$
80	79	fveqeq2d	$⊢ X = j \underset{˙}{\cdot} Y \to (N (\{X\}) = N (\{Y\}) \leftrightarrow N (\{j \underset{˙}{\cdot} Y\}) = N (\{Y\}))$
81	80	biimprcd	$⊢ N (\{j \underset{˙}{\cdot} Y\}) = N (\{Y\}) \to (X = j \underset{˙}{\cdot} Y \to N (\{X\}) = N (\{Y\}))$
82	78 81	syl6	$⊢ φ \to (j \in (K ∖ \{\underset{˙}{0}\}) \to (X = j \underset{˙}{\cdot} Y \to N (\{X\}) = N (\{Y\})))$
83	82	rexlimdv	$⊢ φ \to (\exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y \to N (\{X\}) = N (\{Y\}))$
84	69 83	impbid	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y)$
85		oveq1	$⊢ j = k \to j \underset{˙}{\cdot} Y = k \underset{˙}{\cdot} Y$
86	85	eqeq2d	$⊢ j = k \to (X = j \underset{˙}{\cdot} Y \leftrightarrow X = k \underset{˙}{\cdot} Y)$
87	86	cbvrexvw	$⊢ \exists j \in (K ∖ \{\underset{˙}{0}\}) X = j \underset{˙}{\cdot} Y \leftrightarrow \exists k \in (K ∖ \{\underset{˙}{0}\}) X = k \underset{˙}{\cdot} Y$
88	84 87	bitrdi	$⊢ φ \to (N (\{X\}) = N (\{Y\}) \leftrightarrow \exists k \in (K ∖ \{\underset{˙}{0}\}) X = k \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem lspsneq

Proof