Metamath Proof Explorer

Theorem issubrng2

Description: Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypotheses issubrng2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
issubrng2.t ⊢ · = ( .r ‘ 𝑅 )
Assertion issubrng2 ( 𝑅 ∈ Rng → ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 issubrng2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 issubrng2.t ⊢ · = ( .r ‘ 𝑅 )
3 subrngsubg ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
4 2 subrngmcl ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
5 4 3expb ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
6 5 ralrimivva ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 )
7 3 6 jca ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) )
8 simpl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝑅 ∈ Rng )
9 simprl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
10 eqid ⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
11 10 subgbas ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
12 9 11 syl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
13 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14 10 13 ressplusg ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝐴 ) ) )
15 9 14 syl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( 𝑅 ↾s 𝐴 ) ) )
16 10 2 ressmulr ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → · = ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) )
17 9 16 syl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → · = ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) )
18 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
19 10 subgabl ⊢ ( ( 𝑅 ∈ Abel ∧ 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Abel )
20 18 9 19 syl2an2r ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Abel )
21 simprr ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 )
22 oveq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 · 𝑦 ) = ( 𝑢 · 𝑦 ) )
23 22 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 · 𝑦 ) ∈ 𝐴 ↔ ( 𝑢 · 𝑦 ) ∈ 𝐴 ) )
24 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 · 𝑦 ) = ( 𝑢 · 𝑣 ) )
25 24 eleq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 · 𝑦 ) ∈ 𝐴 ↔ ( 𝑢 · 𝑣 ) ∈ 𝐴 ) )
26 23 25 rspc2v ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 → ( 𝑢 · 𝑣 ) ∈ 𝐴 ) )
27 21 26 syl5com ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 · 𝑣 ) ∈ 𝐴 ) )
28 27 3impib ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) → ( 𝑢 · 𝑣 ) ∈ 𝐴 )
29 1 subgss ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → 𝐴 ⊆ 𝐵 )
30 9 29 syl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 ⊆ 𝐵 )
31 30 sseld ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝐴 → 𝑢 ∈ 𝐵 ) )
32 30 sseld ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑣 ∈ 𝐴 → 𝑣 ∈ 𝐵 ) )
33 30 sseld ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) )
34 31 32 33 3anim123d ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) )
35 34 imp ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) )
36 1 2 rngass ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 · 𝑣 ) · 𝑤 ) = ( 𝑢 · ( 𝑣 · 𝑤 ) ) )
37 36 adantlr ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 · 𝑣 ) · 𝑤 ) = ( 𝑢 · ( 𝑣 · 𝑤 ) ) )
38 35 37 syldan ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑢 · 𝑣 ) · 𝑤 ) = ( 𝑢 · ( 𝑣 · 𝑤 ) ) )
39 1 13 2 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑢 · ( 𝑣 ( +g ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝑢 · 𝑣 ) ( +g ‘ 𝑅 ) ( 𝑢 · 𝑤 ) ) )
40 39 adantlr ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑢 · ( 𝑣 ( +g ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝑢 · 𝑣 ) ( +g ‘ 𝑅 ) ( 𝑢 · 𝑤 ) ) )
41 35 40 syldan ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑢 · ( 𝑣 ( +g ‘ 𝑅 ) 𝑤 ) ) = ( ( 𝑢 · 𝑣 ) ( +g ‘ 𝑅 ) ( 𝑢 · 𝑤 ) ) )
42 1 13 2 rngdir ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑣 ) · 𝑤 ) = ( ( 𝑢 · 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑣 · 𝑤 ) ) )
43 42 adantlr ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑣 ) · 𝑤 ) = ( ( 𝑢 · 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑣 · 𝑤 ) ) )
44 35 43 syldan ⊢ ( ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑢 ( +g ‘ 𝑅 ) 𝑣 ) · 𝑤 ) = ( ( 𝑢 · 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑣 · 𝑤 ) ) )
45 12 15 17 20 28 38 41 44 isrngd ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
46 1 issubrng ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ 𝐵 ) )
47 8 45 30 46 syl3anbrc ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )
48 47 ex ⊢ ( 𝑅 ∈ Rng → ( ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) ) )
49 7 48 impbid2 ⊢ ( 𝑅 ∈ Rng → ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) )