Metamath Proof Explorer


Theorem issubrg3

Description: A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis issubrg3.m 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion issubrg3 ( 𝑅 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 issubrg3.m 𝑀 = ( mulGrp ‘ 𝑅 )
2 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ( 1r𝑅 ) = ( 1r𝑅 )
4 eqid ( .r𝑅 ) = ( .r𝑅 )
5 2 3 4 issubrg2 ( 𝑅 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
6 3anass ( ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
7 5 6 syl6bb ( 𝑅 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) ) )
8 1 ringmgp ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
9 2 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
10 1 2 mgpbas ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
11 1 3 ringidval ( 1r𝑅 ) = ( 0g𝑀 )
12 1 4 mgpplusg ( .r𝑅 ) = ( +g𝑀 )
13 10 11 12 issubm ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
14 3anass ( ( 𝑆 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑅 ) ∧ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
15 13 14 syl6bb ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑅 ) ∧ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) ) )
16 15 baibd ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
17 8 9 16 syl2an ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) )
18 17 pm5.32da ( 𝑅 ∈ Ring → ( ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( 1r𝑅 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝑅 ) 𝑦 ) ∈ 𝑆 ) ) ) )
19 7 18 bitr4d ( 𝑅 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ) ) )