islinds4

Description: A set is independent in a vector space iff it is a subset of some basis. This is an axiom of choice equivalent. (Contributed by Stefan O'Rear, 24-Feb-2015)

		Ref	Expression
	Hypothesis	islinds4.j	$⊢ J = LBasis (W)$
	Assertion	islinds4	$⊢ W \in LVec \to (Y \in LIndS (W) \leftrightarrow \exists b \in J Y \subseteq b)$

Proof

Step	Hyp	Ref	Expression
1		islinds4.j	$⊢ J = LBasis (W)$
2		simpl	$⊢ (W \in LVec \land Y \in LIndS (W)) \to W \in LVec$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	3	linds1	$⊢ Y \in LIndS (W) \to Y \subseteq {Base}_{W}$
5	4	adantl	$⊢ (W \in LVec \land Y \in LIndS (W)) \to Y \subseteq {Base}_{W}$
6		lveclmod	$⊢ W \in LVec \to W \in LMod$
7	6	ad2antrr	$⊢ ((W \in LVec \land Y \in LIndS (W)) \land x \in Y) \to W \in LMod$
8		eqid	$⊢ Scalar (W) = Scalar (W)$
9	8	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
10		drngnzr	$⊢ Scalar (W) \in DivRing \to Scalar (W) \in NzRing$
11	9 10	syl	$⊢ W \in LVec \to Scalar (W) \in NzRing$
12	11	ad2antrr	$⊢ ((W \in LVec \land Y \in LIndS (W)) \land x \in Y) \to Scalar (W) \in NzRing$
13		simplr	$⊢ ((W \in LVec \land Y \in LIndS (W)) \land x \in Y) \to Y \in LIndS (W)$
14		simpr	$⊢ ((W \in LVec \land Y \in LIndS (W)) \land x \in Y) \to x \in Y$
15		eqid	$⊢ LSpan (W) = LSpan (W)$
16	15 8	lindsind2	$⊢ ((W \in LMod \land Scalar (W) \in NzRing) \land Y \in LIndS (W) \land x \in Y) \to \neg x \in LSpan (W) (Y ∖ \{x\})$
17	7 12 13 14 16	syl211anc	$⊢ ((W \in LVec \land Y \in LIndS (W)) \land x \in Y) \to \neg x \in LSpan (W) (Y ∖ \{x\})$
18	17	ralrimiva	$⊢ (W \in LVec \land Y \in LIndS (W)) \to \forall x \in Y \neg x \in LSpan (W) (Y ∖ \{x\})$
19	1 3 15	lbsext	$⊢ (W \in LVec \land Y \subseteq {Base}_{W} \land \forall x \in Y \neg x \in LSpan (W) (Y ∖ \{x\})) \to \exists b \in J Y \subseteq b$
20	2 5 18 19	syl3anc	$⊢ (W \in LVec \land Y \in LIndS (W)) \to \exists b \in J Y \subseteq b$
21	20	ex	$⊢ W \in LVec \to (Y \in LIndS (W) \to \exists b \in J Y \subseteq b)$
22	6	ad2antrr	$⊢ ((W \in LVec \land b \in J) \land Y \subseteq b) \to W \in LMod$
23	1	lbslinds	$⊢ J \subseteq LIndS (W)$
24	23	sseli	$⊢ b \in J \to b \in LIndS (W)$
25	24	ad2antlr	$⊢ ((W \in LVec \land b \in J) \land Y \subseteq b) \to b \in LIndS (W)$
26		simpr	$⊢ ((W \in LVec \land b \in J) \land Y \subseteq b) \to Y \subseteq b$
27		lindsss	$⊢ (W \in LMod \land b \in LIndS (W) \land Y \subseteq b) \to Y \in LIndS (W)$
28	22 25 26 27	syl3anc	$⊢ ((W \in LVec \land b \in J) \land Y \subseteq b) \to Y \in LIndS (W)$
29	28	rexlimdva2	$⊢ W \in LVec \to (\exists b \in J Y \subseteq b \to Y \in LIndS (W))$
30	21 29	impbid	$⊢ W \in LVec \to (Y \in LIndS (W) \leftrightarrow \exists b \in J Y \subseteq b)$

Metamath Proof Explorer

Theorem islinds4

Proof