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

Metamath Proof Explorer

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 ‘ 𝐵 ) )