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

Metamath Proof Explorer

Theorem sraassa

Description: The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015) (Proof shortened by SN, 21-Mar-2025)

Ref Expression
Hypothesis sraassa.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
Assertion sraassa ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 sraassa.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
2 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3 2 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑊 ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
4 3 adantl ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
5 eqid ⊢ ( Cntr ‘ ( mulGrp ‘ 𝑊 ) ) = ( Cntr ‘ ( mulGrp ‘ 𝑊 ) )
6 2 5 crngbascntr ⊢ ( 𝑊 ∈ CRing → ( Base ‘ 𝑊 ) = ( Cntr ‘ ( mulGrp ‘ 𝑊 ) ) )
7 6 adantr ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ( Cntr ‘ ( mulGrp ‘ 𝑊 ) ) )
8 4 7 sseqtrd ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 ⊆ ( Cntr ‘ ( mulGrp ‘ 𝑊 ) ) )
9 crngring ⊢ ( 𝑊 ∈ CRing → 𝑊 ∈ Ring )
10 9 adantr ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑊 ∈ Ring )
11 simpr ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑊 ) )
12 1 5 10 11 sraassab ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → ( 𝐴 ∈ AssAlg ↔ 𝑆 ⊆ ( Cntr ‘ ( mulGrp ‘ 𝑊 ) ) ) )
13 8 12 mpbird ⊢ ( ( 𝑊 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑊 ) ) → 𝐴 ∈ AssAlg )