lsslss

Description: The subspaces of a subspace are the smaller subspaces. (Contributed by Stefan O'Rear, 12-Dec-2014)

	Ref	Expression
Hypotheses	lsslss.x	$⊢ X = W ↾_{𝑠} U$
	lsslss.s	$⊢ S = LSubSp (W)$
	lsslss.t	$⊢ T = LSubSp (X)$
Assertion	lsslss	$⊢ (W \in LMod \land U \in S) \to (V \in T \leftrightarrow (V \in S \land V \subseteq U))$

Proof

Step	Hyp	Ref	Expression
1		lsslss.x	$⊢ X = W ↾_{𝑠} U$
2		lsslss.s	$⊢ S = LSubSp (W)$
3		lsslss.t	$⊢ T = LSubSp (X)$
4	1 2	lsslmod	$⊢ (W \in LMod \land U \in S) \to X \in LMod$
5		eqid	$⊢ X ↾_{𝑠} V = X ↾_{𝑠} V$
6		eqid	$⊢ {Base}_{X} = {Base}_{X}$
7	5 6 3	islss3	$⊢ X \in LMod \to (V \in T \leftrightarrow (V \subseteq {Base}_{X} \land X ↾_{𝑠} V \in LMod))$
8	4 7	syl	$⊢ (W \in LMod \land U \in S) \to (V \in T \leftrightarrow (V \subseteq {Base}_{X} \land X ↾_{𝑠} V \in LMod))$
9		eqid	$⊢ {Base}_{W} = {Base}_{W}$
10	9 2	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
11	10	adantl	$⊢ (W \in LMod \land U \in S) \to U \subseteq {Base}_{W}$
12	1 9	ressbas2	$⊢ U \subseteq {Base}_{W} \to U = {Base}_{X}$
13	11 12	syl	$⊢ (W \in LMod \land U \in S) \to U = {Base}_{X}$
14	13	sseq2d	$⊢ (W \in LMod \land U \in S) \to (V \subseteq U \leftrightarrow V \subseteq {Base}_{X})$
15	14	anbi1d	$⊢ (W \in LMod \land U \in S) \to ((V \subseteq U \land X ↾_{𝑠} V \in LMod) \leftrightarrow (V \subseteq {Base}_{X} \land X ↾_{𝑠} V \in LMod))$
16		sstr2	$⊢ V \subseteq U \to (U \subseteq {Base}_{W} \to V \subseteq {Base}_{W})$
17	11 16	mpan9	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to V \subseteq {Base}_{W}$
18	17	biantrurd	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to (W ↾_{𝑠} V \in LMod \leftrightarrow (V \subseteq {Base}_{W} \land W ↾_{𝑠} V \in LMod))$
19	1	oveq1i	$⊢ X ↾_{𝑠} V = (W ↾_{𝑠} U) ↾_{𝑠} V$
20		ressabs	$⊢ (U \in S \land V \subseteq U) \to (W ↾_{𝑠} U) ↾_{𝑠} V = W ↾_{𝑠} V$
21	20	adantll	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to (W ↾_{𝑠} U) ↾_{𝑠} V = W ↾_{𝑠} V$
22	19 21	eqtrid	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to X ↾_{𝑠} V = W ↾_{𝑠} V$
23	22	eleq1d	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to (X ↾_{𝑠} V \in LMod \leftrightarrow W ↾_{𝑠} V \in LMod)$
24		eqid	$⊢ W ↾_{𝑠} V = W ↾_{𝑠} V$
25	24 9 2	islss3	$⊢ W \in LMod \to (V \in S \leftrightarrow (V \subseteq {Base}_{W} \land W ↾_{𝑠} V \in LMod))$
26	25	ad2antrr	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to (V \in S \leftrightarrow (V \subseteq {Base}_{W} \land W ↾_{𝑠} V \in LMod))$
27	18 23 26	3bitr4d	$⊢ ((W \in LMod \land U \in S) \land V \subseteq U) \to (X ↾_{𝑠} V \in LMod \leftrightarrow V \in S)$
28	27	pm5.32da	$⊢ (W \in LMod \land U \in S) \to ((V \subseteq U \land X ↾_{𝑠} V \in LMod) \leftrightarrow (V \subseteq U \land V \in S))$
29	28	biancomd	$⊢ (W \in LMod \land U \in S) \to ((V \subseteq U \land X ↾_{𝑠} V \in LMod) \leftrightarrow (V \in S \land V \subseteq U))$
30	8 15 29	3bitr2d	$⊢ (W \in LMod \land U \in S) \to (V \in T \leftrightarrow (V \in S \land V \subseteq U))$

Metamath Proof Explorer

Theorem lsslss

Proof