Theorem aspss

Description: Span preserves subset ordering. ( spanss analog.) (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
	aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion	aspss	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝐴 ‘ 𝑇 ) ⊆ ( 𝐴 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2		aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		simpl3	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ) → 𝑇 ⊆ 𝑆 )
4		sstr2	⊢ ( 𝑇 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑡 → 𝑇 ⊆ 𝑡 ) )
5	3 4	syl	⊢ ( ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ) → ( 𝑆 ⊆ 𝑡 → 𝑇 ⊆ 𝑡 ) )
6	5	ss2rabdv	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ⊆ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑇 ⊆ 𝑡 } )
7		intss	⊢ ( { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } ⊆ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑇 ⊆ 𝑡 } → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑇 ⊆ 𝑡 } ⊆ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } )
8	6 7	syl	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑇 ⊆ 𝑡 } ⊆ ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } )
9		simp1	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → 𝑊 ∈ AssAlg )
10		simp3	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑆 )
11		simp2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → 𝑆 ⊆ 𝑉 )
12	10 11	sstrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑉 )
13		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
14	1 2 13	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑇 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑇 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑇 ⊆ 𝑡 } )
15	9 12 14	syl2anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝐴 ‘ 𝑇 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑇 ⊆ 𝑡 } )
16	1 2 13	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } )
17	16	3adant3	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ ( LSubSp ‘ 𝑊 ) ) ∣ 𝑆 ⊆ 𝑡 } )
18	8 15 17	3sstr4d	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑆 ) → ( 𝐴 ‘ 𝑇 ) ⊆ ( 𝐴 ‘ 𝑆 ) )