subrgacs

Description: Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015)

		Ref	Expression
	Hypothesis	subrgacs.b	$⊢ B = {Base}_{R}$
	Assertion	subrgacs	$⊢ R \in Ring \to SubRing (R) \in ACS (B)$

Step	Hyp	Ref	Expression
1		subrgacs.b	$⊢ B = {Base}_{R}$
2		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
3	2	issubrg3	$⊢ R \in Ring \to (x \in SubRing (R) \leftrightarrow (x \in SubGrp (R) \land x \in SubMnd ({mulGrp}_{R})))$
4		elin	$⊢ x \in (SubGrp (R) \cap SubMnd ({mulGrp}_{R})) \leftrightarrow (x \in SubGrp (R) \land x \in SubMnd ({mulGrp}_{R}))$
5	3 4	bitr4di	$⊢ R \in Ring \to (x \in SubRing (R) \leftrightarrow x \in (SubGrp (R) \cap SubMnd ({mulGrp}_{R})))$
6	5	eqrdv	$⊢ R \in Ring \to SubRing (R) = SubGrp (R) \cap SubMnd ({mulGrp}_{R})$
7	1	fvexi	$⊢ B \in V$
8		mreacs	$⊢ B \in V \to ACS (B) \in Moore (𝒫 B)$
9	7 8	mp1i	$⊢ R \in Ring \to ACS (B) \in Moore (𝒫 B)$
10		ringgrp	$⊢ R \in Ring \to R \in Grp$
11	1	subgacs	$⊢ R \in Grp \to SubGrp (R) \in ACS (B)$
12	10 11	syl	$⊢ R \in Ring \to SubGrp (R) \in ACS (B)$
13	2	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
14	2 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
15	14	submacs	$⊢ {mulGrp}_{R} \in Mnd \to SubMnd ({mulGrp}_{R}) \in ACS (B)$
16	13 15	syl	$⊢ R \in Ring \to SubMnd ({mulGrp}_{R}) \in ACS (B)$
17		mreincl	$⊢ (ACS (B) \in Moore (𝒫 B) \land SubGrp (R) \in ACS (B) \land SubMnd ({mulGrp}_{R}) \in ACS (B)) \to SubGrp (R) \cap SubMnd ({mulGrp}_{R}) \in ACS (B)$
18	9 12 16 17	syl3anc	$⊢ R \in Ring \to SubGrp (R) \cap SubMnd ({mulGrp}_{R}) \in ACS (B)$
19	6 18	eqeltrd	$⊢ R \in Ring \to SubRing (R) \in ACS (B)$

Metamath Proof Explorer