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 ⊢ V = Base W
lspss.n ⊢ N = LSpan ⁡ W
Assertion lspss ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → N ⁡ T ⊆ N ⁡ U

Proof

Step Hyp Ref Expression
1 lspss.v ⊢ V = Base W
2 lspss.n ⊢ N = LSpan ⁡ W
3 simpl3 ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U ∧ t ∈ LSubSp ⁡ W → T ⊆ U
4 sstr2 ⊢ T ⊆ U → U ⊆ t → T ⊆ t
5 3 4 syl ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U ∧ t ∈ LSubSp ⁡ W → U ⊆ t → T ⊆ t
6 5 ss2rabdv ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → t ∈ LSubSp ⁡ W | U ⊆ t ⊆ t ∈ LSubSp ⁡ W | T ⊆ t
7 intss ⊢ t ∈ LSubSp ⁡ W | U ⊆ t ⊆ t ∈ LSubSp ⁡ W | T ⊆ t → ⋂ t ∈ LSubSp ⁡ W | T ⊆ t ⊆ ⋂ t ∈ LSubSp ⁡ W | U ⊆ t
8 6 7 syl ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → ⋂ t ∈ LSubSp ⁡ W | T ⊆ t ⊆ ⋂ t ∈ LSubSp ⁡ W | U ⊆ t
9 simp1 ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → W ∈ LMod
10 simp3 ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → T ⊆ U
11 simp2 ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → U ⊆ V
12 10 11 sstrd ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → T ⊆ V
13 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
14 1 13 2 lspval ⊢ W ∈ LMod ∧ T ⊆ V → N ⁡ T = ⋂ t ∈ LSubSp ⁡ W | T ⊆ t
15 9 12 14 syl2anc ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → N ⁡ T = ⋂ t ∈ LSubSp ⁡ W | T ⊆ t
16 1 13 2 lspval ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U = ⋂ t ∈ LSubSp ⁡ W | U ⊆ t
17 16 3adant3 ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → N ⁡ U = ⋂ t ∈ LSubSp ⁡ W | U ⊆ t
18 8 15 17 3sstr4d ⊢ W ∈ LMod ∧ U ⊆ V ∧ T ⊆ U → N ⁡ T ⊆ N ⁡ U