Theorem subrgacs

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

	Ref	Expression
Hypothesis	subrgacs.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	subrgacs	⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgacs.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
3	2	issubrg3	⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑥 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) ) )
4		elin	⊢ ( 𝑥 ∈ ( ( SubGrp ‘ 𝑅 ) ∩ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑥 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) )
5	3 4	bitr4di	⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( SubRing ‘ 𝑅 ) ↔ 𝑥 ∈ ( ( SubGrp ‘ 𝑅 ) ∩ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) ) )
6	5	eqrdv	⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) = ( ( SubGrp ‘ 𝑅 ) ∩ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) )
7	1	fvexi	⊢ 𝐵 ∈ V
8		mreacs	⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
9	7 8	mp1i	⊢ ( 𝑅 ∈ Ring → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
10		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
11	1	subgacs	⊢ ( 𝑅 ∈ Grp → ( SubGrp ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )
12	10 11	syl	⊢ ( 𝑅 ∈ Ring → ( SubGrp ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )
13	2	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
14	2 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
15	14	submacs	⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( ACS ‘ 𝐵 ) )
16	13 15	syl	⊢ ( 𝑅 ∈ Ring → ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( ACS ‘ 𝐵 ) )
17		mreincl	⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubGrp ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) ∧ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubGrp ‘ 𝑅 ) ∩ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) ∈ ( ACS ‘ 𝐵 ) )
18	9 12 16 17	syl3anc	⊢ ( 𝑅 ∈ Ring → ( ( SubGrp ‘ 𝑅 ) ∩ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) ) ∈ ( ACS ‘ 𝐵 ) )
19	6 18	eqeltrd	⊢ ( 𝑅 ∈ Ring → ( SubRing ‘ 𝑅 ) ∈ ( ACS ‘ 𝐵 ) )