islbs3

Description: An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014)

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

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	8	3ad2ant1	$⊢ (W \in LVec \land B \in J \land s \subset B) \to W \in LMod$
10		pssss	$⊢ s \subset B \to s \subseteq B$
11	10 4	sylan9ssr	$⊢ (B \in J \land s \subset B) \to s \subseteq V$
12	11	3adant1	$⊢ (W \in LVec \land B \in J \land s \subset B) \to s \subseteq V$
13	1 3	lspssv	$⊢ (W \in LMod \land s \subseteq V) \to N (s) \subseteq V$
14	9 12 13	syl2anc	$⊢ (W \in LVec \land B \in J \land s \subset B) \to N (s) \subseteq V$
15		eqid	$⊢ Scalar (W) = Scalar (W)$
16	15	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
17		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
18		eqid	$⊢ 1_{Scalar (W)} = 1_{Scalar (W)}$
19	17 18	drngunz	$⊢ Scalar (W) \in DivRing \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
20	16 19	syl	$⊢ W \in LVec \to 1_{Scalar (W)} \neq 0_{Scalar (W)}$
21	8 20	jca	$⊢ W \in LVec \to (W \in LMod \land 1_{Scalar (W)} \neq 0_{Scalar (W)})$
22	2 3 15 18 17 1	lbspss	$⊢ ((W \in LMod \land 1_{Scalar (W)} \neq 0_{Scalar (W)}) \land B \in J \land s \subset B) \to N (s) \neq V$
23	21 22	syl3an1	$⊢ (W \in LVec \land B \in J \land s \subset B) \to N (s) \neq V$
24		df-pss	$⊢ N (s) \subset V \leftrightarrow (N (s) \subseteq V \land N (s) \neq V)$
25	14 23 24	sylanbrc	$⊢ (W \in LVec \land B \in J \land s \subset B) \to N (s) \subset V$
26	25	3expia	$⊢ (W \in LVec \land B \in J) \to (s \subset B \to N (s) \subset V)$
27	26	alrimiv	$⊢ (W \in LVec \land B \in J) \to \forall s (s \subset B \to N (s) \subset V)$
28	5 7 27	3jca	$⊢ (W \in LVec \land B \in J) \to (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))$
29		simpr1	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \to B \subseteq V$
30		simpr2	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \to N (B) = V$
31		simplr1	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B \subseteq V$
32	31	ssdifssd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B ∖ \{x\} \subseteq V$
33	1	fvexi	$⊢ V \in V$
34		ssexg	$⊢ (B ∖ \{x\} \subseteq V \land V \in V) \to B ∖ \{x\} \in V$
35	32 33 34	sylancl	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B ∖ \{x\} \in V$
36		simplr3	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to \forall s (s \subset B \to N (s) \subset V)$
37		difssd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B ∖ \{x\} \subseteq B$
38		simpr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to x \in B$
39		neldifsn	$⊢ \neg x \in (B ∖ \{x\})$
40		nelne1	$⊢ (x \in B \land \neg x \in (B ∖ \{x\})) \to B \neq B ∖ \{x\}$
41	38 39 40	sylancl	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B \neq B ∖ \{x\}$
42	41	necomd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B ∖ \{x\} \neq B$
43		df-pss	$⊢ B ∖ \{x\} \subset B \leftrightarrow (B ∖ \{x\} \subseteq B \land B ∖ \{x\} \neq B)$
44	37 42 43	sylanbrc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to B ∖ \{x\} \subset B$
45		psseq1	$⊢ s = B ∖ \{x\} \to (s \subset B \leftrightarrow B ∖ \{x\} \subset B)$
46		fveq2	$⊢ s = B ∖ \{x\} \to N (s) = N (B ∖ \{x\})$
47	46	psseq1d	$⊢ s = B ∖ \{x\} \to (N (s) \subset V \leftrightarrow N (B ∖ \{x\}) \subset V)$
48	45 47	imbi12d	$⊢ s = B ∖ \{x\} \to ((s \subset B \to N (s) \subset V) \leftrightarrow (B ∖ \{x\} \subset B \to N (B ∖ \{x\}) \subset V))$
49	48	spcgv	$⊢ B ∖ \{x\} \in V \to (\forall s (s \subset B \to N (s) \subset V) \to (B ∖ \{x\} \subset B \to N (B ∖ \{x\}) \subset V))$
50	35 36 44 49	syl3c	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to N (B ∖ \{x\}) \subset V$
51		dfpss3	$⊢ N (B ∖ \{x\}) \subset V \leftrightarrow (N (B ∖ \{x\}) \subseteq V \land \neg V \subseteq N (B ∖ \{x\}))$
52	51	simprbi	$⊢ N (B ∖ \{x\}) \subset V \to \neg V \subseteq N (B ∖ \{x\})$
53	50 52	syl	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to \neg V \subseteq N (B ∖ \{x\})$
54		simplr2	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to N (B) = V$
55	8	ad2antrr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to W \in LMod$
56	32	adantrr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to B ∖ \{x\} \subseteq V$
57		eqid	$⊢ LSubSp (W) = LSubSp (W)$
58	1 57 3	lspcl	$⊢ (W \in LMod \land B ∖ \{x\} \subseteq V) \to N (B ∖ \{x\}) \in LSubSp (W)$
59	55 56 58	syl2anc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to N (B ∖ \{x\}) \in LSubSp (W)$
60		ssun1	$⊢ B \subseteq B \cup \{x\}$
61		undif1	$⊢ (B ∖ \{x\}) \cup \{x\} = B \cup \{x\}$
62	60 61	sseqtrri	$⊢ B \subseteq (B ∖ \{x\}) \cup \{x\}$
63	1 3	lspssid	$⊢ (W \in LMod \land B ∖ \{x\} \subseteq V) \to B ∖ \{x\} \subseteq N (B ∖ \{x\})$
64	55 56 63	syl2anc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to B ∖ \{x\} \subseteq N (B ∖ \{x\})$
65		simprr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to x \in N (B ∖ \{x\})$
66	65	snssd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to \{x\} \subseteq N (B ∖ \{x\})$
67	64 66	unssd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to (B ∖ \{x\}) \cup \{x\} \subseteq N (B ∖ \{x\})$
68	62 67	sstrid	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to B \subseteq N (B ∖ \{x\})$
69	57 3	lspssp	$⊢ (W \in LMod \land N (B ∖ \{x\}) \in LSubSp (W) \land B \subseteq N (B ∖ \{x\})) \to N (B) \subseteq N (B ∖ \{x\})$
70	55 59 68 69	syl3anc	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to N (B) \subseteq N (B ∖ \{x\})$
71	54 70	eqsstrrd	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land (x \in B \land x \in N (B ∖ \{x\}))) \to V \subseteq N (B ∖ \{x\})$
72	71	expr	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to (x \in N (B ∖ \{x\}) \to V \subseteq N (B ∖ \{x\}))$
73	53 72	mtod	$⊢ ((W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \land x \in B) \to \neg x \in N (B ∖ \{x\})$
74	73	ralrimiva	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \to \forall x \in B \neg x \in N (B ∖ \{x\})$
75	1 2 3	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\})))$
76	75	adantr	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall x \in B \neg x \in N (B ∖ \{x\})))$
77	29 30 74 76	mpbir3and	$⊢ (W \in LVec \land (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V))) \to B \in J$
78	28 77	impbida	$⊢ W \in LVec \to (B \in J \leftrightarrow (B \subseteq V \land N (B) = V \land \forall s (s \subset B \to N (s) \subset V)))$

Metamath Proof Explorer

Theorem islbs3

Proof