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 ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
lsslss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsslss.t ⊢ 𝑇 = ( LSubSp ‘ 𝑋 )
Assertion lsslss ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑉 ∈ 𝑇 ↔ ( 𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsslss.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 lsslss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsslss.t ⊢ 𝑇 = ( LSubSp ‘ 𝑋 )
4 1 2 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
5 eqid ⊢ ( 𝑋 ↾s 𝑉 ) = ( 𝑋 ↾s 𝑉 )
6 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
7 5 6 3 islss3 ⊢ ( 𝑋 ∈ LMod → ( 𝑉 ∈ 𝑇 ↔ ( 𝑉 ⊆ ( Base ‘ 𝑋 ) ∧ ( 𝑋 ↾s 𝑉 ) ∈ LMod ) ) )
8 4 7 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑉 ∈ 𝑇 ↔ ( 𝑉 ⊆ ( Base ‘ 𝑋 ) ∧ ( 𝑋 ↾s 𝑉 ) ∈ LMod ) ) )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 9 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
11 10 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
12 1 9 ressbas2 ⊢ ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑈 = ( Base ‘ 𝑋 ) )
13 11 12 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( Base ‘ 𝑋 ) )
14 13 sseq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑉 ⊆ 𝑈 ↔ 𝑉 ⊆ ( Base ‘ 𝑋 ) ) )
15 14 anbi1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑉 ⊆ 𝑈 ∧ ( 𝑋 ↾s 𝑉 ) ∈ LMod ) ↔ ( 𝑉 ⊆ ( Base ‘ 𝑋 ) ∧ ( 𝑋 ↾s 𝑉 ) ∈ LMod ) ) )
16 sstr2 ⊢ ( 𝑉 ⊆ 𝑈 → ( 𝑈 ⊆ ( Base ‘ 𝑊 ) → 𝑉 ⊆ ( Base ‘ 𝑊 ) ) )
17 11 16 mpan9 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ⊆ ( Base ‘ 𝑊 ) )
18 17 biantrurd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑊 ↾s 𝑉 ) ∈ LMod ↔ ( 𝑉 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑊 ↾s 𝑉 ) ∈ LMod ) ) )
19 1 oveq1i ⊢ ( 𝑋 ↾s 𝑉 ) = ( ( 𝑊 ↾s 𝑈 ) ↾s 𝑉 )
20 ressabs ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑊 ↾s 𝑈 ) ↾s 𝑉 ) = ( 𝑊 ↾s 𝑉 ) )
21 20 adantll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑊 ↾s 𝑈 ) ↾s 𝑉 ) = ( 𝑊 ↾s 𝑉 ) )
22 19 21 syl5eq ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑋 ↾s 𝑉 ) = ( 𝑊 ↾s 𝑉 ) )
23 22 eleq1d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑋 ↾s 𝑉 ) ∈ LMod ↔ ( 𝑊 ↾s 𝑉 ) ∈ LMod ) )
24 eqid ⊢ ( 𝑊 ↾s 𝑉 ) = ( 𝑊 ↾s 𝑉 )
25 24 9 2 islss3 ⊢ ( 𝑊 ∈ LMod → ( 𝑉 ∈ 𝑆 ↔ ( 𝑉 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑊 ↾s 𝑉 ) ∈ LMod ) ) )
26 25 ad2antrr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑉 ∈ 𝑆 ↔ ( 𝑉 ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑊 ↾s 𝑉 ) ∈ LMod ) ) )
27 18 23 26 3bitr4d ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑋 ↾s 𝑉 ) ∈ LMod ↔ 𝑉 ∈ 𝑆 ) )
28 27 pm5.32da ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑉 ⊆ 𝑈 ∧ ( 𝑋 ↾s 𝑉 ) ∈ LMod ) ↔ ( 𝑉 ⊆ 𝑈 ∧ 𝑉 ∈ 𝑆 ) ) )
29 28 biancomd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ( 𝑉 ⊆ 𝑈 ∧ ( 𝑋 ↾s 𝑉 ) ∈ LMod ) ↔ ( 𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈 ) ) )
30 8 15 29 3bitr2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑉 ∈ 𝑇 ↔ ( 𝑉 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑈 ) ) )