Metamath Proof Explorer

Theorem subrdom

Description: A subring of a domain is a domain. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses subrdom.1 ⊢ ( 𝜑 → 𝑅 ∈ Domn )
subrdom.2 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion subrdom ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Domn )

Proof

Step Hyp Ref Expression
1 subrdom.1 ⊢ ( 𝜑 → 𝑅 ∈ Domn )
2 subrdom.2 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
3 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
4 1 3 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
5 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
6 5 subrgnzr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑆 ) ∈ NzRing )
7 4 2 6 syl2anc ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ NzRing )
8 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑅 ∈ Domn )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
11 2 10 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
12 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑅 ) )
13 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
14 5 9 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑅 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
15 11 14 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
16 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
17 13 16 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑥 ∈ 𝑆 )
18 12 17 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
20 19 16 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑦 ∈ 𝑆 )
21 12 20 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
22 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
23 2 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
24 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25 5 24 ressmulr ⊢ ( 𝑆 ∈ V → ( .r ‘ 𝑅 ) = ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) )
26 23 25 syl ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) )
27 26 oveqd ⊢ ( 𝜑 → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) )
28 27 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) )
29 subrgrcl ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
30 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
31 2 29 30 3syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
32 subrgsubg ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
33 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
34 33 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
35 2 32 34 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
36 5 9 33 ress0g ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
37 31 35 11 36 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
38 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
39 22 28 38 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) )
40 9 24 33 domneq0 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) )
41 40 biimpa ⊢ ( ( ( 𝑅 ∈ Domn ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) )
42 8 18 21 39 41 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) )
43 38 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ↔ 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
44 38 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ↔ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
45 43 44 orbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ↔ ( 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ∨ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
46 42 45 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ∨ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
47 46 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) → ( 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ∨ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
48 47 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) → ( ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) → ( 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ∨ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
49 48 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) → ( 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ∨ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
50 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
51 eqid ⊢ ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) = ( .r ‘ ( 𝑅 ↾s 𝑆 ) )
52 eqid ⊢ ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) )
53 50 51 52 isdomn ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Domn ↔ ( ( 𝑅 ↾s 𝑆 ) ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 𝑥 ( .r ‘ ( 𝑅 ↾s 𝑆 ) ) 𝑦 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) → ( 𝑥 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ∨ 𝑦 = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) )
54 7 49 53 sylanbrc ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Domn )