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 ⊢ M = mulGrp R
Assertion issubrg3 ⊢ R ∈ Ring → S ∈ SubRing ⁡ R ↔ S ∈ SubGrp ⁡ R ∧ S ∈ SubMnd ⁡ M

Proof

Step Hyp Ref Expression
1 issubrg3.m ⊢ M = mulGrp R
2 eqid ⊢ Base R = Base R
3 eqid ⊢ 1 R = 1 R
4 eqid ⊢ ⋅ R = ⋅ R
5 2 3 4 issubrg2 ⊢ R ∈ Ring → S ∈ SubRing ⁡ R ↔ S ∈ SubGrp ⁡ R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
6 3anass ⊢ S ∈ SubGrp ⁡ R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S ↔ S ∈ SubGrp ⁡ R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
7 5 6 syl6bb ⊢ R ∈ Ring → S ∈ SubRing ⁡ R ↔ S ∈ SubGrp ⁡ R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
8 1 ringmgp ⊢ R ∈ Ring → M ∈ Mnd
9 2 subgss ⊢ S ∈ SubGrp ⁡ R → S ⊆ Base R
10 1 2 mgpbas ⊢ Base R = Base M
11 1 3 ringidval ⊢ 1 R = 0 M
12 1 4 mgpplusg ⊢ ⋅ R = + M
13 10 11 12 issubm ⊢ M ∈ Mnd → S ∈ SubMnd ⁡ M ↔ S ⊆ Base R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
14 3anass ⊢ S ⊆ Base R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S ↔ S ⊆ Base R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
15 13 14 syl6bb ⊢ M ∈ Mnd → S ∈ SubMnd ⁡ M ↔ S ⊆ Base R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
16 15 baibd ⊢ M ∈ Mnd ∧ S ⊆ Base R → S ∈ SubMnd ⁡ M ↔ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
17 8 9 16 syl2an ⊢ R ∈ Ring ∧ S ∈ SubGrp ⁡ R → S ∈ SubMnd ⁡ M ↔ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
18 17 pm5.32da ⊢ R ∈ Ring → S ∈ SubGrp ⁡ R ∧ S ∈ SubMnd ⁡ M ↔ S ∈ SubGrp ⁡ R ∧ 1 R ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ R y ∈ S
19 7 18 bitr4d ⊢ R ∈ Ring → S ∈ SubRing ⁡ R ↔ S ∈ SubGrp ⁡ R ∧ S ∈ SubMnd ⁡ M