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	$⊢ A = subringAlg (W) (S)$
	Assertion	sraassa	$⊢ (W \in CRing \land S \in SubRing (W)) \to A \in AssAlg$

Proof

Step	Hyp	Ref	Expression
1		sraassa.a	$⊢ A = subringAlg (W) (S)$
2		eqid	$⊢ {Base}_{W} = {Base}_{W}$
3	2	subrgss	$⊢ S \in SubRing (W) \to S \subseteq {Base}_{W}$
4	3	adantl	$⊢ (W \in CRing \land S \in SubRing (W)) \to S \subseteq {Base}_{W}$
5		eqid	$⊢ Cntr ({mulGrp}_{W}) = Cntr ({mulGrp}_{W})$
6	2 5	crngbascntr	$⊢ W \in CRing \to {Base}_{W} = Cntr ({mulGrp}_{W})$
7	6	adantr	$⊢ (W \in CRing \land S \in SubRing (W)) \to {Base}_{W} = Cntr ({mulGrp}_{W})$
8	4 7	sseqtrd	$⊢ (W \in CRing \land S \in SubRing (W)) \to S \subseteq Cntr ({mulGrp}_{W})$
9		crngring	$⊢ W \in CRing \to W \in Ring$
10	9	adantr	$⊢ (W \in CRing \land S \in SubRing (W)) \to W \in Ring$
11		simpr	$⊢ (W \in CRing \land S \in SubRing (W)) \to S \in SubRing (W)$
12	1 5 10 11	sraassab	$⊢ (W \in CRing \land S \in SubRing (W)) \to (A \in AssAlg \leftrightarrow S \subseteq Cntr ({mulGrp}_{W}))$
13	8 12	mpbird	$⊢ (W \in CRing \land S \in SubRing (W)) \to A \in AssAlg$