islbs2

Description: An equivalent formulation of the basis predicate in a vector space: a subset is a basis iff no element is in the span of the rest of the set. (Contributed by Mario Carneiro, 14-Jan-2015)

	Ref	Expression
Hypotheses	islbs2.v	$⊢ V = {Base}_{W}$
	islbs2.j	$⊢ J = LBasis (W)$
	islbs2.n	$⊢ N = LSpan (W)$
Assertion	islbs2	$⊢ W \in LVec \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\})))$

Proof

Step	Hyp	Ref	Expression
1		islbs2.v	$⊢ V = {Base}_{W}$
2		islbs2.j	$⊢ J = LBasis (W)$
3		islbs2.n	$⊢ N = LSpan (W)$
4	1 2	lbsss	$⊢ B \in J \to B \subseteq V$
5	4	adantl	$⊢ (W \in LVec \land B \in J) \to B \subseteq V$
6	1 2 3	lbssp	$⊢ B \in J \to N (B) = V$
7	6	adantl	$⊢ (W \in LVec \land B \in J) \to N (B) = V$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9		eqid	$⊢ Scalar (W) = Scalar (W)$
10	9	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
11		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
12		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
13	11 12	drngunz	$⊢ Scalar (W) \in DivRing \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
14	10 13	syl	$⊢ W \in LVec \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
15	8 14	jca	$⊢ W \in LVec \to (W \in LMod \land 1_{Scalar (W)} \neq 0_{Scalar (W)})$
16	2 3 9 12 11	lbsind2	$⊢ ((W \in LMod \land 1_{Scalar (W)} \neq 0_{Scalar (W)}) \land B \in J \land x \in B) \to \neg x \in N (B ∖ \{x\})$
17	15 16	syl3an1	$⊢ (W \in LVec \land B \in J \land x \in B) \to \neg x \in N (B ∖ \{x\})$
18	17	3expa	$⊢ ((W \in LVec \land B \in J) \land x \in B) \to \neg x \in N (B ∖ \{x\})$
19	18	ralrimiva	$⊢ (W \in LVec \land B \in J) \to \forall x \in B \neg x \in N (B ∖ \{x\})$
20	5 7 19	3jca	$⊢ (W \in LVec \land B \in J) \to (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))$
21		simpr1	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \to B \subseteq V$
22		simpr2	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \to N (B) = V$
23		id	$⊢ x = y \to x = y$
24		sneq	$⊢ x = y \to \{x\} = \{y\}$
25	24	difeq2d	$⊢ x = y \to B ∖ \{x\} = B ∖ \{y\}$
26	25	fveq2d	$⊢ x = y \to N (B ∖ \{x\}) = N (B ∖ \{y\})$
27	23 26	eleq12d	$⊢ x = y \to (x \in N (B ∖ \{x\}) \leftrightarrow y \in N (B ∖ \{y\}))$
28	27	notbid	$⊢ x = y \to (\neg x \in N (B ∖ \{x\}) \leftrightarrow \neg y \in N (B ∖ \{y\}))$
29		simplr3	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \forall x \in B \neg x \in N (B ∖ \{x\})$
30		simprl	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to y \in B$
31	28 29 30	rspcdva	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg y \in N (B ∖ \{y\})$
32		simpll	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to W \in LVec$
33		simprr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\})$
34		eldifsn	$⊢ z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \leftrightarrow (z \in {Base}_{Scalar (W)} \land z \neq 0_{Scalar (W)})$
35	33 34	sylib	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (z \in {Base}_{Scalar (W)} \land z \neq 0_{Scalar (W)})$
36	21	adantr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to B \subseteq V$
37	36 30	sseldd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to y \in V$
38		eqid	$⊢ \cdot_{W} = \cdot_{W}$
39		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
40	1 9 38 39 11 3	lspsnvs	$⊢ (W \in LVec \land (z \in {Base}_{Scalar (W)} \land z \neq 0_{Scalar (W)}) \land y \in V) \to N (\{z \cdot_{W} y\}) = N (\{y\})$
41	32 35 37 40	syl3anc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to N (\{z \cdot_{W} y\}) = N (\{y\})$
42	41	sseq1d	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (N (\{z \cdot_{W} y\}) \subseteq N (B ∖ \{y\}) \leftrightarrow N (\{y\}) \subseteq N (B ∖ \{y\}))$
43		eqid	$⊢ LSubSp (W) = LSubSp (W)$
44	8	adantr	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \to W \in LMod$
45	44	adantr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to W \in LMod$
46	36	ssdifssd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to B ∖ \{y\} \subseteq V$
47	1 43 3	lspcl	$⊢ (W \in LMod \land B ∖ \{y\} \subseteq V) \to N (B ∖ \{y\}) \in LSubSp (W)$
48	45 46 47	syl2anc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to N (B ∖ \{y\}) \in LSubSp (W)$
49	35	simpld	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to z \in {Base}_{Scalar (W)}$
50	1 9 38 39	lmodvscl	$⊢ (W \in LMod \land z \in {Base}_{Scalar (W)} \land y \in V) \to z \cdot_{W} y \in V$
51	45 49 37 50	syl3anc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to z \cdot_{W} y \in V$
52	1 43 3 45 48 51	ellspsn5b	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (z \cdot_{W} y \in N (B ∖ \{y\}) \leftrightarrow N (\{z \cdot_{W} y\}) \subseteq N (B ∖ \{y\}))$
53	1 43 3 45 48 37	ellspsn5b	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (y \in N (B ∖ \{y\}) \leftrightarrow N (\{y\}) \subseteq N (B ∖ \{y\}))$
54	42 52 53	3bitr4d	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to (z \cdot_{W} y \in N (B ∖ \{y\}) \leftrightarrow y \in N (B ∖ \{y\}))$
55	31 54	mtbird	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \land (y \in B \land z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}))) \to \neg z \cdot_{W} y \in N (B ∖ \{y\})$
56	55	ralrimivva	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \to \forall y \in B \forall z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg z \cdot_{W} y \in N (B ∖ \{y\})$
57	1 9 38 39 2 3 11	islbs	$⊢ W \in LVec \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall y \in B \forall z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg z \cdot_{W} y \in N (B ∖ \{y\})))$
58	57	adantr	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall y \in B \forall z \in ({Base}_{Scalar (W)} ∖ \{0_{Scalar (W)}\}) \neg z \cdot_{W} y \in N (B ∖ \{y\})))$
59	21 22 56 58	mpbir3and	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\}))) \to B \in J$
60	20 59	impbida	$⊢ W \in LVec \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\})))$

Metamath Proof Explorer

Theorem islbs2

Proof