lss1d

Description: One-dimensional subspace (or zero-dimensional if X is the zero vector). (Contributed by NM, 14-Jan-2014) (Proof shortened by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lss1d.v	$⊢ V = {Base}_{W}$
	lss1d.f	$⊢ F = Scalar (W)$
	lss1d.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lss1d.k	$⊢ K = {Base}_{F}$
	lss1d.s	$⊢ S = LSubSp (W)$
Assertion	lss1d	$⊢ (W \in LMod \land X \in V) \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \in S$

Proof

Step	Hyp	Ref	Expression
1		lss1d.v	$⊢ V = {Base}_{W}$
2		lss1d.f	$⊢ F = Scalar (W)$
3		lss1d.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lss1d.k	$⊢ K = {Base}_{F}$
5		lss1d.s	$⊢ S = LSubSp (W)$
6	2	a1i	$⊢ (W \in LMod \land X \in V) \to F = Scalar (W)$
7	4	a1i	$⊢ (W \in LMod \land X \in V) \to K = {Base}_{F}$
8	1	a1i	$⊢ (W \in LMod \land X \in V) \to V = {Base}_{W}$
9		eqidd	$⊢ (W \in LMod \land X \in V) \to +_{W} = +_{W}$
10	3	a1i	$⊢ (W \in LMod \land X \in V) \to \underset{˙}{\cdot} = \cdot_{W}$
11	5	a1i	$⊢ (W \in LMod \land X \in V) \to S = LSubSp (W)$
12	1 2 3 4	lmodvscl	$⊢ (W \in LMod \land k \in K \land X \in V) \to k \underset{˙}{\cdot} X \in V$
13	12	3expa	$⊢ ((W \in LMod \land k \in K) \land X \in V) \to k \underset{˙}{\cdot} X \in V$
14	13	an32s	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to k \underset{˙}{\cdot} X \in V$
15		eleq1a	$⊢ k \underset{˙}{\cdot} X \in V \to (v = k \underset{˙}{\cdot} X \to v \in V)$
16	14 15	syl	$⊢ ((W \in LMod \land X \in V) \land k \in K) \to (v = k \underset{˙}{\cdot} X \to v \in V)$
17	16	rexlimdva	$⊢ (W \in LMod \land X \in V) \to (\exists k \in K v = k \underset{˙}{\cdot} X \to v \in V)$
18	17	abssdv	$⊢ (W \in LMod \land X \in V) \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \subseteq V$
19		eqid	$⊢ 0_{F} = 0_{F}$
20	2 4 19	lmod0cl	$⊢ W \in LMod \to 0_{F} \in K$
21	20	adantr	$⊢ (W \in LMod \land X \in V) \to 0_{F} \in K$
22		nfcv	$⊢ \underline{Ⅎ} k 0_{F}$
23		nfre1	$⊢ Ⅎ k \exists k \in K v = k \underset{˙}{\cdot} X$
24	23	nfab	$⊢ \underline{Ⅎ} k \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$
25		nfcv	$⊢ \underline{Ⅎ} k \emptyset$
26	24 25	nfne	$⊢ Ⅎ k \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \neq \emptyset$
27		biidd	$⊢ k = 0_{F} \to (\{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \neq \emptyset \leftrightarrow \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \neq \emptyset)$
28		ovex	$⊢ k \underset{˙}{\cdot} X \in V$
29	28	elabrex	$⊢ k \in K \to k \underset{˙}{\cdot} X \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$
30	29	ne0d	$⊢ k \in K \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \neq \emptyset$
31	22 26 27 30	vtoclgaf	$⊢ 0_{F} \in K \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \neq \emptyset$
32	21 31	syl	$⊢ (W \in LMod \land X \in V) \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \neq \emptyset$
33		vex	$⊢ a \in V$
34		eqeq1	$⊢ v = a \to (v = k \underset{˙}{\cdot} X \leftrightarrow a = k \underset{˙}{\cdot} X)$
35	34	rexbidv	$⊢ v = a \to (\exists k \in K v = k \underset{˙}{\cdot} X \leftrightarrow \exists k \in K a = k \underset{˙}{\cdot} X)$
36	33 35	elab	$⊢ a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists k \in K a = k \underset{˙}{\cdot} X$
37		oveq1	$⊢ k = y \to k \underset{˙}{\cdot} X = y \underset{˙}{\cdot} X$
38	37	eqeq2d	$⊢ k = y \to (a = k \underset{˙}{\cdot} X \leftrightarrow a = y \underset{˙}{\cdot} X)$
39	38	cbvrexvw	$⊢ \exists k \in K a = k \underset{˙}{\cdot} X \leftrightarrow \exists y \in K a = y \underset{˙}{\cdot} X$
40	36 39	bitri	$⊢ a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists y \in K a = y \underset{˙}{\cdot} X$
41		vex	$⊢ b \in V$
42		eqeq1	$⊢ v = b \to (v = k \underset{˙}{\cdot} X \leftrightarrow b = k \underset{˙}{\cdot} X)$
43	42	rexbidv	$⊢ v = b \to (\exists k \in K v = k \underset{˙}{\cdot} X \leftrightarrow \exists k \in K b = k \underset{˙}{\cdot} X)$
44	41 43	elab	$⊢ b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists k \in K b = k \underset{˙}{\cdot} X$
45		oveq1	$⊢ k = z \to k \underset{˙}{\cdot} X = z \underset{˙}{\cdot} X$
46	45	eqeq2d	$⊢ k = z \to (b = k \underset{˙}{\cdot} X \leftrightarrow b = z \underset{˙}{\cdot} X)$
47	46	cbvrexvw	$⊢ \exists k \in K b = k \underset{˙}{\cdot} X \leftrightarrow \exists z \in K b = z \underset{˙}{\cdot} X$
48	44 47	bitri	$⊢ b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists z \in K b = z \underset{˙}{\cdot} X$
49	40 48	anbi12i	$⊢ (a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \land b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}) \leftrightarrow (\exists y \in K a = y \underset{˙}{\cdot} X \land \exists z \in K b = z \underset{˙}{\cdot} X)$
50		reeanv	$⊢ \exists y \in K \exists z \in K (a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \leftrightarrow (\exists y \in K a = y \underset{˙}{\cdot} X \land \exists z \in K b = z \underset{˙}{\cdot} X)$
51	49 50	bitr4i	$⊢ (a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \land b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}) \leftrightarrow \exists y \in K \exists z \in K (a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X)$
52		simpll	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to W \in LMod$
53		simprr	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to x \in K$
54		simprll	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to y \in K$
55		eqid	$⊢ \cdot_{F} = \cdot_{F}$
56	2 4 55	lmodmcl	$⊢ (W \in LMod \land x \in K \land y \in K) \to x \cdot_{F} y \in K$
57	52 53 54 56	syl3anc	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to x \cdot_{F} y \in K$
58		simprlr	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to z \in K$
59		eqid	$⊢ +_{F} = +_{F}$
60	2 4 59	lmodacl	$⊢ (W \in LMod \land x \cdot_{F} y \in K \land z \in K) \to (x \cdot_{F} y) +_{F} z \in K$
61	52 57 58 60	syl3anc	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to (x \cdot_{F} y) +_{F} z \in K$
62		simplr	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to X \in V$
63		eqid	$⊢ +_{W} = +_{W}$
64	1 63 2 3 4 59	lmodvsdir	$⊢ (W \in LMod \land (x \cdot_{F} y \in K \land z \in K \land X \in V)) \to ((x \cdot_{F} y) +_{F} z) \underset{˙}{\cdot} X = ((x \cdot_{F} y) \underset{˙}{\cdot} X) +_{W} (z \underset{˙}{\cdot} X)$
65	52 57 58 62 64	syl13anc	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to ((x \cdot_{F} y) +_{F} z) \underset{˙}{\cdot} X = ((x \cdot_{F} y) \underset{˙}{\cdot} X) +_{W} (z \underset{˙}{\cdot} X)$
66	1 2 3 4 55	lmodvsass	$⊢ (W \in LMod \land (x \in K \land y \in K \land X \in V)) \to (x \cdot_{F} y) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)$
67	52 53 54 62 66	syl13anc	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to (x \cdot_{F} y) \underset{˙}{\cdot} X = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)$
68	67	oveq1d	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to ((x \cdot_{F} y) \underset{˙}{\cdot} X) +_{W} (z \underset{˙}{\cdot} X) = (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X)$
69	65 68	eqtr2d	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X) = ((x \cdot_{F} y) +_{F} z) \underset{˙}{\cdot} X$
70		oveq1	$⊢ k = (x \cdot_{F} y) +_{F} z \to k \underset{˙}{\cdot} X = ((x \cdot_{F} y) +_{F} z) \underset{˙}{\cdot} X$
71	70	rspceeqv	$⊢ ((x \cdot_{F} y) +_{F} z \in K \land (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X) = ((x \cdot_{F} y) +_{F} z) \underset{˙}{\cdot} X) \to \exists k \in K (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X) = k \underset{˙}{\cdot} X$
72	61 69 71	syl2anc	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to \exists k \in K (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X) = k \underset{˙}{\cdot} X$
73		oveq2	$⊢ a = y \underset{˙}{\cdot} X \to x \underset{˙}{\cdot} a = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)$
74		oveq12	$⊢ (x \underset{˙}{\cdot} a = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X) \land b = z \underset{˙}{\cdot} X) \to (x \underset{˙}{\cdot} a) +_{W} b = (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X)$
75	73 74	sylan	$⊢ (a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to (x \underset{˙}{\cdot} a) +_{W} b = (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X)$
76	75	eqeq1d	$⊢ (a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to ((x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X \leftrightarrow (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X) = k \underset{˙}{\cdot} X)$
77	76	rexbidv	$⊢ (a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to (\exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X \leftrightarrow \exists k \in K (x \underset{˙}{\cdot} (y \underset{˙}{\cdot} X)) +_{W} (z \underset{˙}{\cdot} X) = k \underset{˙}{\cdot} X)$
78	72 77	syl5ibrcom	$⊢ ((W \in LMod \land X \in V) \land ((y \in K \land z \in K) \land x \in K)) \to ((a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X)$
79	78	expr	$⊢ ((W \in LMod \land X \in V) \land (y \in K \land z \in K)) \to (x \in K \to ((a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X))$
80	79	com23	$⊢ ((W \in LMod \land X \in V) \land (y \in K \land z \in K)) \to ((a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to (x \in K \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X))$
81	80	rexlimdvva	$⊢ (W \in LMod \land X \in V) \to (\exists y \in K \exists z \in K (a = y \underset{˙}{\cdot} X \land b = z \underset{˙}{\cdot} X) \to (x \in K \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X))$
82	51 81	syl5bi	$⊢ (W \in LMod \land X \in V) \to ((a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \land b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}) \to (x \in K \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X))$
83	82	expcomd	$⊢ (W \in LMod \land X \in V) \to (b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \to (a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \to (x \in K \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X)))$
84	83	com24	$⊢ (W \in LMod \land X \in V) \to (x \in K \to (a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \to (b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X)))$
85	84	3imp2	$⊢ ((W \in LMod \land X \in V) \land (x \in K \land a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \land b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\})) \to \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X$
86		ovex	$⊢ (x \underset{˙}{\cdot} a) +_{W} b \in V$
87		eqeq1	$⊢ v = (x \underset{˙}{\cdot} a) +_{W} b \to (v = k \underset{˙}{\cdot} X \leftrightarrow (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X)$
88	87	rexbidv	$⊢ v = (x \underset{˙}{\cdot} a) +_{W} b \to (\exists k \in K v = k \underset{˙}{\cdot} X \leftrightarrow \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X)$
89	86 88	elab	$⊢ (x \underset{˙}{\cdot} a) +_{W} b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \leftrightarrow \exists k \in K (x \underset{˙}{\cdot} a) +_{W} b = k \underset{˙}{\cdot} X$
90	85 89	sylibr	$⊢ ((W \in LMod \land X \in V) \land (x \in K \land a \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \land b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\})) \to (x \underset{˙}{\cdot} a) +_{W} b \in \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\}$
91	6 7 8 9 10 11 18 32 90	islssd	$⊢ (W \in LMod \land X \in V) \to \{v \| \exists k \in K v = k \underset{˙}{\cdot} X\} \in S$

Metamath Proof Explorer

Theorem lss1d

Proof