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