islinds3

Description: A subset is linearly independent iff it is a basis of its span. (Contributed by Stefan O'Rear, 25-Feb-2015)

	Ref	Expression
Hypotheses	islinds3.b	$⊢ B = {Base}_{W}$
	islinds3.k	$⊢ K = LSpan (W)$
	islinds3.x	$⊢ X = W ↾_{𝑠} K (Y)$
	islinds3.j	$⊢ J = LBasis (X)$
Assertion	islinds3	$⊢ W \in LMod \to (Y \in LIndS (W) \leftrightarrow Y \in J)$

Proof

Step	Hyp	Ref	Expression
1		islinds3.b	$⊢ B = {Base}_{W}$
2		islinds3.k	$⊢ K = LSpan (W)$
3		islinds3.x	$⊢ X = W ↾_{𝑠} K (Y)$
4		islinds3.j	$⊢ J = LBasis (X)$
5	1	linds1	$⊢ Y \in LIndS (W) \to Y \subseteq B$
6	5	a1i	$⊢ W \in LMod \to (Y \in LIndS (W) \to Y \subseteq B)$
7		eqid	$⊢ {Base}_{X} = {Base}_{X}$
8	7	linds1	$⊢ Y \in LIndS (X) \to Y \subseteq {Base}_{X}$
9	3 1	ressbasss	$⊢ {Base}_{X} \subseteq B$
10	8 9	sstrdi	$⊢ Y \in LIndS (X) \to Y \subseteq B$
11	10	adantr	$⊢ (Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X}) \to Y \subseteq B$
12	11	a1i	$⊢ W \in LMod \to ((Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X}) \to Y \subseteq B)$
13		simpl	$⊢ (W \in LMod \land Y \subseteq B) \to W \in LMod$
14		eqid	$⊢ LSubSp (W) = LSubSp (W)$
15	1 14 2	lspcl	$⊢ (W \in LMod \land Y \subseteq B) \to K (Y) \in LSubSp (W)$
16	1 2	lspssid	$⊢ (W \in LMod \land Y \subseteq B) \to Y \subseteq K (Y)$
17		eqid	$⊢ LSpan (X) = LSpan (X)$
18	3 2 17 14	lsslsp	$⊢ (W \in LMod \land K (Y) \in LSubSp (W) \land Y \subseteq K (Y)) \to K (Y) = LSpan (X) (Y)$
19	13 15 16 18	syl3anc	$⊢ (W \in LMod \land Y \subseteq B) \to K (Y) = LSpan (X) (Y)$
20	1 2	lspssv	$⊢ (W \in LMod \land Y \subseteq B) \to K (Y) \subseteq B$
21	3 1	ressbas2	$⊢ K (Y) \subseteq B \to K (Y) = {Base}_{X}$
22	20 21	syl	$⊢ (W \in LMod \land Y \subseteq B) \to K (Y) = {Base}_{X}$
23	19 22	eqtr3d	$⊢ (W \in LMod \land Y \subseteq B) \to LSpan (X) (Y) = {Base}_{X}$
24	23	biantrud	$⊢ (W \in LMod \land Y \subseteq B) \to (Y \in LIndS (W) \leftrightarrow (Y \in LIndS (W) \land LSpan (X) (Y) = {Base}_{X}))$
25	14 3	lsslinds	$⊢ (W \in LMod \land K (Y) \in LSubSp (W) \land Y \subseteq K (Y)) \to (Y \in LIndS (X) \leftrightarrow Y \in LIndS (W))$
26	13 15 16 25	syl3anc	$⊢ (W \in LMod \land Y \subseteq B) \to (Y \in LIndS (X) \leftrightarrow Y \in LIndS (W))$
27	26	bicomd	$⊢ (W \in LMod \land Y \subseteq B) \to (Y \in LIndS (W) \leftrightarrow Y \in LIndS (X))$
28	27	anbi1d	$⊢ (W \in LMod \land Y \subseteq B) \to ((Y \in LIndS (W) \land LSpan (X) (Y) = {Base}_{X}) \leftrightarrow (Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X}))$
29	24 28	bitrd	$⊢ (W \in LMod \land Y \subseteq B) \to (Y \in LIndS (W) \leftrightarrow (Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X}))$
30	29	ex	$⊢ W \in LMod \to (Y \subseteq B \to (Y \in LIndS (W) \leftrightarrow (Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X})))$
31	6 12 30	pm5.21ndd	$⊢ W \in LMod \to (Y \in LIndS (W) \leftrightarrow (Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X}))$
32	7 4 17	islbs4	$⊢ Y \in J \leftrightarrow (Y \in LIndS (X) \land LSpan (X) (Y) = {Base}_{X})$
33	31 32	bitr4di	$⊢ W \in LMod \to (Y \in LIndS (W) \leftrightarrow Y \in J)$

Metamath Proof Explorer

Theorem islinds3

Proof