lbsextg

Description: For any linearly independent subset C of V , there is a basis containing the vectors in C . (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypotheses	lbsex.j	$⊢ J = LBasis (W)$
	lbsex.v	$⊢ V = {Base}_{W}$
	lbsex.n	$⊢ N = LSpan (W)$
Assertion	lbsextg	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to \exists s \in J C \subseteq s$

Proof

Step	Hyp	Ref	Expression
1		lbsex.j	$⊢ J = LBasis (W)$
2		lbsex.v	$⊢ V = {Base}_{W}$
3		lbsex.n	$⊢ N = LSpan (W)$
4		simp1l	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to W \in LVec$
5		simp2	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to C \subseteq V$
6		simp3	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to \forall x \in C \neg x \in N (C ∖ \{x\})$
7		id	$⊢ x = y \to x = y$
8		sneq	$⊢ x = y \to \{x\} = \{y\}$
9	8	difeq2d	$⊢ x = y \to C ∖ \{x\} = C ∖ \{y\}$
10	9	fveq2d	$⊢ x = y \to N (C ∖ \{x\}) = N (C ∖ \{y\})$
11	7 10	eleq12d	$⊢ x = y \to (x \in N (C ∖ \{x\}) \leftrightarrow y \in N (C ∖ \{y\}))$
12	11	notbid	$⊢ x = y \to (\neg x \in N (C ∖ \{x\}) \leftrightarrow \neg y \in N (C ∖ \{y\}))$
13	12	cbvralvw	$⊢ \forall x \in C \neg x \in N (C ∖ \{x\}) \leftrightarrow \forall y \in C \neg y \in N (C ∖ \{y\})$
14	6 13	sylib	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to \forall y \in C \neg y \in N (C ∖ \{y\})$
15	8	difeq2d	$⊢ x = y \to z ∖ \{x\} = z ∖ \{y\}$
16	15	fveq2d	$⊢ x = y \to N (z ∖ \{x\}) = N (z ∖ \{y\})$
17	7 16	eleq12d	$⊢ x = y \to (x \in N (z ∖ \{x\}) \leftrightarrow y \in N (z ∖ \{y\}))$
18	17	notbid	$⊢ x = y \to (\neg x \in N (z ∖ \{x\}) \leftrightarrow \neg y \in N (z ∖ \{y\}))$
19	18	cbvralvw	$⊢ \forall x \in z \neg x \in N (z ∖ \{x\}) \leftrightarrow \forall y \in z \neg y \in N (z ∖ \{y\})$
20	19	anbi2i	$⊢ (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \leftrightarrow (C \subseteq z \land \forall y \in z \neg y \in N (z ∖ \{y\}))$
21	20	rabbii	$⊢ \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\} = \{z \in 𝒫 V \| (C \subseteq z \land \forall y \in z \neg y \in N (z ∖ \{y\}))\}$
22		simp1r	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to 𝒫 V \in dom card$
23	2 1 3 4 5 14 21 22	lbsextlem4	$⊢ ((W \in LVec \land 𝒫 V \in dom card) \land C \subseteq V \land \forall x \in C \neg x \in N (C ∖ \{x\})) \to \exists s \in J C \subseteq s$

Metamath Proof Explorer

Theorem lbsextg

Proof