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 ∧ 𝑈 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ 𝑈 ) )