This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑊 ) ∧ 𝑆 ∈ 𝐿 ) → ( 𝐴 ‘ 𝑆 ) = 𝑆 )