Metamath Proof Explorer


Theorem lspss

Description: Span preserves subset ordering. ( spanss analog.) (Contributed by NM, 11-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspss.v 𝑉 = ( Base ‘ 𝑊 )
lspss.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspss ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → ( 𝑁𝑇 ) ⊆ ( 𝑁𝑈 ) )

Proof

Step Hyp Ref Expression
1 lspss.v 𝑉 = ( Base ‘ 𝑊 )
2 lspss.n 𝑁 = ( LSpan ‘ 𝑊 )
3 simpl3 ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) ∧ 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑇𝑈 )
4 sstr2 ( 𝑇𝑈 → ( 𝑈𝑡𝑇𝑡 ) )
5 3 4 syl ( ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) ∧ 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑈𝑡𝑇𝑡 ) )
6 5 ss2rabdv ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈𝑡 } ⊆ { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑇𝑡 } )
7 intss ( { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈𝑡 } ⊆ { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑇𝑡 } → { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑇𝑡 } ⊆ { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈𝑡 } )
8 6 7 syl ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑇𝑡 } ⊆ { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈𝑡 } )
9 simp1 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → 𝑊 ∈ LMod )
10 simp3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → 𝑇𝑈 )
11 simp2 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → 𝑈𝑉 )
12 10 11 sstrd ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → 𝑇𝑉 )
13 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
14 1 13 2 lspval ( ( 𝑊 ∈ LMod ∧ 𝑇𝑉 ) → ( 𝑁𝑇 ) = { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑇𝑡 } )
15 9 12 14 syl2anc ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → ( 𝑁𝑇 ) = { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑇𝑡 } )
16 1 13 2 lspval ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉 ) → ( 𝑁𝑈 ) = { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈𝑡 } )
17 16 3adant3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → ( 𝑁𝑈 ) = { 𝑡 ∈ ( LSubSp ‘ 𝑊 ) ∣ 𝑈𝑡 } )
18 8 15 17 3sstr4d ( ( 𝑊 ∈ LMod ∧ 𝑈𝑉𝑇𝑈 ) → ( 𝑁𝑇 ) ⊆ ( 𝑁𝑈 ) )