Metamath Proof Explorer

Theorem issubrg2

Description: Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypotheses issubrg2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
issubrg2.o ⊢ 1 = ( 1r ‘ 𝑅 )
issubrg2.t ⊢ · = ( .r ‘ 𝑅 )
Assertion issubrg2 ( 𝑅 ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 issubrg2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 issubrg2.o ⊢ 1 = ( 1r ‘ 𝑅 )
3 issubrg2.t ⊢ · = ( .r ‘ 𝑅 )
4 subrgsubg ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
5 2 subrg1cl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 1 ∈ 𝐴 )
6 3 subrgmcl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
7 6 3expb ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
8 7 ralrimivva ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 )
9 4 5 8 3jca ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) )
10 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝑅 ∈ Ring )
11 simpr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
12 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
13 12 subgbas ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
14 11 13 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
15 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
16 12 15 ressplusg ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝐴 ) ) )
17 11 16 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝐴 ) ) )
18 12 3 ressmulr ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → · = ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) )
19 11 18 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → · = ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) )
20 12 subggrp ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → ( 𝑅 ↾s 𝐴 ) ∈ Grp )
21 11 20 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Grp )
22 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 )
23 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 · 𝑦 ) = ( 𝑢 · 𝑦 ) )
24 23 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 · 𝑦 ) ∈ 𝐴 ↔ ( 𝑢 · 𝑦 ) ∈ 𝐴 ) )
25 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 · 𝑦 ) = ( 𝑢 · 𝑣 ) )
26 25 eleq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 · 𝑦 ) ∈ 𝐴 ↔ ( 𝑢 · 𝑣 ) ∈ 𝐴 ) )
27 24 26 rspc2v ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 → ( 𝑢 · 𝑣 ) ∈ 𝐴 ) )
28 22 27 syl5com ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 · 𝑣 ) ∈ 𝐴 ) )
29 28 3impib ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 · 𝑣 ) ∈ 𝐴 )
30 1 subgss ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → 𝐴 ⊆ 𝐵 )
31 11 30 syl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 ⊆ 𝐵 )
32 31 sseld ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵 ) )
33 31 sseld ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑣 ∈ 𝐴 → 𝑣 ∈ 𝐵 ) )
34 31 sseld ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) )
35 32 33 34 3anim123d ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) )
36 35 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) )
37 1 3 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 · 𝑣 ) · 𝑤 ) = ( 𝑢 · ( 𝑣 · 𝑤 ) ) )
38 37 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 · 𝑣 ) · 𝑤 ) = ( 𝑢 · ( 𝑣 · 𝑤 ) ) )
39 36 38 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑢 · 𝑣 ) · 𝑤 ) = ( 𝑢 · ( 𝑣 · 𝑤 ) ) )
40 1 15 3 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑢 · ( 𝑣 ( +g ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝑢 · 𝑣 ) ( +g ‘ 𝑅 ) ( 𝑢 · 𝑤 ) ) )
41 40 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑢 · ( 𝑣 ( +g ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝑢 · 𝑣 ) ( +g ‘ 𝑅 ) ( 𝑢 · 𝑤 ) ) )
42 36 41 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑢 · ( 𝑣 ( +g ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝑢 · 𝑣 ) ( +g ‘ 𝑅 ) ( 𝑢 · 𝑤 ) ) )
43 1 15 3 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑣 ) · 𝑤 ) = ( ( 𝑢 · 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑣 · 𝑤 ) ) )
44 43 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑣 ) · 𝑤 ) = ( ( 𝑢 · 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑣 · 𝑤 ) ) )
45 36 44 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑣 ) · 𝑤 ) = ( ( 𝑢 · 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑣 · 𝑤 ) ) )
46 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 1 ∈ 𝐴 )
47 32 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ 𝐵 )
48 1 3 2 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ 𝐵 ) → ( 1 · 𝑢 ) = 𝑢 )
49 48 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 1 · 𝑢 ) = 𝑢 )
50 47 49 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 1 · 𝑢 ) = 𝑢 )
51 1 3 2 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 · 1 ) = 𝑢 )
52 51 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 · 1 ) = 𝑢 )
53 47 52 syldan ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ) → ( 𝑢 · 1 ) = 𝑢 )
54 14 17 19 21 29 39 42 45 46 50 53 isringd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Ring )
55 31 46 jca ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) )
56 1 2 issubrg ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴 ) ) )
57 10 54 55 56 syl21anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 ∈ ( SubRing ‘ 𝑅 ) )
58 57 ex ⊢ ( 𝑅 ∈ Ring → ( ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) → 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) )
59 9 58 impbid2 ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) )