lsslinds

Description: Linear independence is unchanged by working in a subspace. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypotheses	lsslindf.u	$⊢ U = LSubSp (W)$
	lsslindf.x	$⊢ X = W ↾_{𝑠} S$
Assertion	lsslinds	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \in LIndS (X) \leftrightarrow F \in LIndS (W))$

Proof

Step	Hyp	Ref	Expression
1		lsslindf.u	$⊢ U = LSubSp (W)$
2		lsslindf.x	$⊢ X = W ↾_{𝑠} S$
3		eqid	$⊢ {Base}_{W} = {Base}_{W}$
4	3 1	lssss	$⊢ S \in U \to S \subseteq {Base}_{W}$
5	2 3	ressbas2	$⊢ S \subseteq {Base}_{W} \to S = {Base}_{X}$
6	4 5	syl	$⊢ S \in U \to S = {Base}_{X}$
7	6	3ad2ant2	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to S = {Base}_{X}$
8	7	sseq2d	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \subseteq S \leftrightarrow F \subseteq {Base}_{X})$
9	4	3ad2ant2	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to S \subseteq {Base}_{W}$
10		sstr2	$⊢ F \subseteq S \to (S \subseteq {Base}_{W} \to F \subseteq {Base}_{W})$
11	9 10	mpan9	$⊢ ((W \in LMod \land S \in U \land F \subseteq S) \land F \subseteq S) \to F \subseteq {Base}_{W}$
12		simpl3	$⊢ ((W \in LMod \land S \in U \land F \subseteq S) \land F \subseteq {Base}_{W}) \to F \subseteq S$
13	11 12	impbida	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \subseteq S \leftrightarrow F \subseteq {Base}_{W})$
14	8 13	bitr3d	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \subseteq {Base}_{X} \leftrightarrow F \subseteq {Base}_{W})$
15		rnresi	$⊢ ran ({I ↾}_{F}) = F$
16	15	sseq1i	$⊢ ran ({I ↾}_{F}) \subseteq S \leftrightarrow F \subseteq S$
17	1 2	lsslindf	$⊢ (W \in LMod \land S \in U \land ran ({I ↾}_{F}) \subseteq S) \to (({I ↾}_{F}) LIndF X \leftrightarrow ({I ↾}_{F}) LIndF W)$
18	16 17	syl3an3br	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (({I ↾}_{F}) LIndF X \leftrightarrow ({I ↾}_{F}) LIndF W)$
19	14 18	anbi12d	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to ((F \subseteq {Base}_{X} \land ({I ↾}_{F}) LIndF X) \leftrightarrow (F \subseteq {Base}_{W} \land ({I ↾}_{F}) LIndF W))$
20	2	ovexi	$⊢ X \in V$
21		eqid	$⊢ {Base}_{X} = {Base}_{X}$
22	21	islinds	$⊢ X \in V \to (F \in LIndS (X) \leftrightarrow (F \subseteq {Base}_{X} \land ({I ↾}_{F}) LIndF X))$
23	20 22	mp1i	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \in LIndS (X) \leftrightarrow (F \subseteq {Base}_{X} \land ({I ↾}_{F}) LIndF X))$
24	3	islinds	$⊢ W \in LMod \to (F \in LIndS (W) \leftrightarrow (F \subseteq {Base}_{W} \land ({I ↾}_{F}) LIndF W))$
25	24	3ad2ant1	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \in LIndS (W) \leftrightarrow (F \subseteq {Base}_{W} \land ({I ↾}_{F}) LIndF W))$
26	19 23 25	3bitr4d	$⊢ (W \in LMod \land S \in U \land F \subseteq S) \to (F \in LIndS (X) \leftrightarrow F \in LIndS (W))$

Metamath Proof Explorer

Theorem lsslinds

Proof