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

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 bitrdi ⊢ ( 𝑅 ∈ 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 bitrdi ⊢ ( 𝑀 ∈ 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 ‘ 𝑀 ) ) ) )