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 )