Theorem aspid

Description: The algebraic span of a subalgebra is itself. ( spanid analog.) (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
	aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	aspval.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion	aspid	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝐴 ‘ 𝑆 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		aspval.a	⊢ 𝐴 = ( AlgSpan ‘ 𝑊 )
2		aspval.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		aspval.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
4		simp1	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → 𝑊 ∈ AssAlg )
5	2	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ 𝑉 )
6	5	3ad2ant2	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → 𝑆 ⊆ 𝑉 )
7	1 2 3	aspval	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )
8	4 6 7	syl2anc	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝐴 ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } )
9		3simpc	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) )
10		elin	⊢ ( 𝑆 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ↔ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) )
11	9 10	sylibr	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → 𝑆 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) )
12		intmin	⊢ ( 𝑆 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } = 𝑆 )
13	11 12	syl	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → ∩ { 𝑡 ∈ ( ( SubRing ‘ 𝑊 ) ∩ 𝐿 ) ∣ 𝑆 ⊆ 𝑡 } = 𝑆 )
14	8 13	eqtrd	⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝐴 ‘ 𝑆 ) = 𝑆 )