Metamath Proof Explorer

Theorem 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 ∈ LMod ∧ U ∈ S → V ∈ T ↔ V ∈ S ∧ V ⊆ 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 ∈ LMod ∧ U ∈ S → X ∈ LMod
5 eqid ⊢ X ↾ 𝑠 V = X ↾ 𝑠 V
6 eqid ⊢ Base X = Base X
7 5 6 3 islss3 ⊢ X ∈ LMod → V ∈ T ↔ V ⊆ Base X ∧ X ↾ 𝑠 V ∈ LMod
8 4 7 syl ⊢ W ∈ LMod ∧ U ∈ S → V ∈ T ↔ V ⊆ Base X ∧ X ↾ 𝑠 V ∈ LMod
9 eqid ⊢ Base W = Base W
10 9 2 lssss ⊢ U ∈ S → U ⊆ Base W
11 10 adantl ⊢ W ∈ LMod ∧ U ∈ S → U ⊆ Base W
12 1 9 ressbas2 ⊢ U ⊆ Base W → U = Base X
13 11 12 syl ⊢ W ∈ LMod ∧ U ∈ S → U = Base X
14 13 sseq2d ⊢ W ∈ LMod ∧ U ∈ S → V ⊆ U ↔ V ⊆ Base X
15 14 anbi1d ⊢ W ∈ LMod ∧ U ∈ S → V ⊆ U ∧ X ↾ 𝑠 V ∈ LMod ↔ V ⊆ Base X ∧ X ↾ 𝑠 V ∈ LMod
16 sstr2 ⊢ V ⊆ U → U ⊆ Base W → V ⊆ Base W
17 11 16 mpan9 ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → V ⊆ Base W
18 17 biantrurd ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → W ↾ 𝑠 V ∈ LMod ↔ V ⊆ Base W ∧ W ↾ 𝑠 V ∈ LMod
19 1 oveq1i ⊢ X ↾ 𝑠 V = W ↾ 𝑠 U ↾ 𝑠 V
20 ressabs ⊢ U ∈ S ∧ V ⊆ U → W ↾ 𝑠 U ↾ 𝑠 V = W ↾ 𝑠 V
21 20 adantll ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → W ↾ 𝑠 U ↾ 𝑠 V = W ↾ 𝑠 V
22 19 21 syl5eq ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → X ↾ 𝑠 V = W ↾ 𝑠 V
23 22 eleq1d ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → X ↾ 𝑠 V ∈ LMod ↔ W ↾ 𝑠 V ∈ LMod
24 eqid ⊢ W ↾ 𝑠 V = W ↾ 𝑠 V
25 24 9 2 islss3 ⊢ W ∈ LMod → V ∈ S ↔ V ⊆ Base W ∧ W ↾ 𝑠 V ∈ LMod
26 25 ad2antrr ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → V ∈ S ↔ V ⊆ Base W ∧ W ↾ 𝑠 V ∈ LMod
27 18 23 26 3bitr4d ⊢ W ∈ LMod ∧ U ∈ S ∧ V ⊆ U → X ↾ 𝑠 V ∈ LMod ↔ V ∈ S
28 27 pm5.32da ⊢ W ∈ LMod ∧ U ∈ S → V ⊆ U ∧ X ↾ 𝑠 V ∈ LMod ↔ V ⊆ U ∧ V ∈ S
29 28 biancomd ⊢ W ∈ LMod ∧ U ∈ S → V ⊆ U ∧ X ↾ 𝑠 V ∈ LMod ↔ V ∈ S ∧ V ⊆ U
30 8 15 29 3bitr2d ⊢ W ∈ LMod ∧ U ∈ S → V ∈ T ↔ V ∈ S ∧ V ⊆ U