lbspss

Description: No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	lbsind2.j	$⊢ J = LBasis (W)$
	lbsind2.n	$⊢ N = LSpan (W)$
	lbsind2.f	$⊢ F = Scalar (W)$
	lbsind2.o	$⊢ \underset{˙}{1} = 1_{F}$
	lbsind2.z	$⊢ \underset{˙}{0} = 0_{F}$
	lbspss.v	$⊢ V = {Base}_{W}$
Assertion	lbspss	$⊢ ((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \to N (C) \neq V$

Proof

Step	Hyp	Ref	Expression
1		lbsind2.j	$⊢ J = LBasis (W)$
2		lbsind2.n	$⊢ N = LSpan (W)$
3		lbsind2.f	$⊢ F = Scalar (W)$
4		lbsind2.o	$⊢ \underset{˙}{1} = 1_{F}$
5		lbsind2.z	$⊢ \underset{˙}{0} = 0_{F}$
6		lbspss.v	$⊢ V = {Base}_{W}$
7		pssnel	$⊢ C \subset B \to \exists x (x \in B \land \neg x \in C)$
8	7	3ad2ant3	$⊢ ((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \to \exists x (x \in B \land \neg x \in C)$
9		simpl2	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to B \in J$
10	6 1	lbsss	$⊢ B \in J \to B \subseteq V$
11	9 10	syl	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to B \subseteq V$
12		simprl	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to x \in B$
13	11 12	sseldd	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to x \in V$
14		simpl1l	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to W \in LMod$
15	11	ssdifssd	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to B ∖ \{x\} \subseteq V$
16		simpl3	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to C \subset B$
17	16	pssssd	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to C \subseteq B$
18	17	sseld	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to (y \in C \to y \in B)$
19		simprr	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to \neg x \in C$
20		eleq1w	$⊢ y = x \to (y \in C \leftrightarrow x \in C)$
21	20	notbid	$⊢ y = x \to (\neg y \in C \leftrightarrow \neg x \in C)$
22	19 21	syl5ibrcom	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to (y = x \to \neg y \in C)$
23	22	necon2ad	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to (y \in C \to y \neq x)$
24	18 23	jcad	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to (y \in C \to (y \in B \land y \neq x))$
25		eldifsn	$⊢ y \in (B ∖ \{x\}) \leftrightarrow (y \in B \land y \neq x)$
26	24 25	syl6ibr	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to (y \in C \to y \in (B ∖ \{x\}))$
27	26	ssrdv	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to C \subseteq B ∖ \{x\}$
28	6 2	lspss	$⊢ (W \in LMod \land B ∖ \{x\} \subseteq V \land C \subseteq B ∖ \{x\}) \to N (C) \subseteq N (B ∖ \{x\})$
29	14 15 27 28	syl3anc	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to N (C) \subseteq N (B ∖ \{x\})$
30		simpl1r	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to \underset{˙}{1} \neq \underset{˙}{0}$
31	1 2 3 4 5	lbsind2	$⊢ ((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land x \in B) \to \neg x \in N (B ∖ \{x\})$
32	14 30 9 12 31	syl211anc	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to \neg x \in N (B ∖ \{x\})$
33	29 32	ssneldd	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to \neg x \in N (C)$
34		nelne1	$⊢ (x \in V \land \neg x \in N (C)) \to V \neq N (C)$
35	13 33 34	syl2anc	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to V \neq N (C)$
36	35	necomd	$⊢ (((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \land (x \in B \land \neg x \in C)) \to N (C) \neq V$
37	8 36	exlimddv	$⊢ ((W \in LMod \land \underset{˙}{1} \neq \underset{˙}{0}) \land B \in J \land C \subset B) \to N (C) \neq V$

Metamath Proof Explorer

Theorem lbspss

Proof