subrdom

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

	Ref	Expression
Hypotheses	subrdom.1	$⊢ φ \to R \in Domn$
	subrdom.2	$⊢ φ \to S \in SubRing (R)$
Assertion	subrdom	$⊢ φ \to R ↾_{𝑠} S \in Domn$

Proof

Step	Hyp	Ref	Expression
1		subrdom.1	$⊢ φ \to R \in Domn$
2		subrdom.2	$⊢ φ \to S \in SubRing (R)$
3		domnnzr	$⊢ R \in Domn \to R \in NzRing$
4	1 3	syl	$⊢ φ \to R \in NzRing$
5		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
6	5	subrgnzr	$⊢ (R \in NzRing \land S \in SubRing (R)) \to R ↾_{𝑠} S \in NzRing$
7	4 2 6	syl2anc	$⊢ φ \to R ↾_{𝑠} S \in NzRing$
8	1	ad3antrrr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to R \in Domn$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	9	subrgss	$⊢ S \in SubRing (R) \to S \subseteq {Base}_{R}$
11	2 10	syl	$⊢ φ \to S \subseteq {Base}_{R}$
12	11	ad3antrrr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to S \subseteq {Base}_{R}$
13		simpllr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to x \in {Base}_{(R ↾_{𝑠} S)}$
14	5 9	ressbas2	$⊢ S \subseteq {Base}_{R} \to S = {Base}_{(R ↾_{𝑠} S)}$
15	11 14	syl	$⊢ φ \to S = {Base}_{(R ↾_{𝑠} S)}$
16	15	ad3antrrr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to S = {Base}_{(R ↾_{𝑠} S)}$
17	13 16	eleqtrrd	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to x \in S$
18	12 17	sseldd	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to x \in {Base}_{R}$
19		simplr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to y \in {Base}_{(R ↾_{𝑠} S)}$
20	19 16	eleqtrrd	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to y \in S$
21	12 20	sseldd	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to y \in {Base}_{R}$
22		simpr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}$
23	2	elexd	$⊢ φ \to S \in V$
24		eqid	$⊢ \cdot_{R} = \cdot_{R}$
25	5 24	ressmulr	$⊢ S \in V \to \cdot_{R} = \cdot_{(R ↾_{𝑠} S)}$
26	23 25	syl	$⊢ φ \to \cdot_{R} = \cdot_{(R ↾_{𝑠} S)}$
27	26	oveqd	$⊢ φ \to x \cdot_{R} y = x \cdot_{(R ↾_{𝑠} S)} y$
28	27	ad3antrrr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to x \cdot_{R} y = x \cdot_{(R ↾_{𝑠} S)} y$
29		subrgrcl	$⊢ S \in SubRing (R) \to R \in Ring$
30		ringmnd	$⊢ R \in Ring \to R \in Mnd$
31	2 29 30	3syl	$⊢ φ \to R \in Mnd$
32		subrgsubg	$⊢ S \in SubRing (R) \to S \in SubGrp (R)$
33		eqid	$⊢ 0_{R} = 0_{R}$
34	33	subg0cl	$⊢ S \in SubGrp (R) \to 0_{R} \in S$
35	2 32 34	3syl	$⊢ φ \to 0_{R} \in S$
36	5 9 33	ress0g	$⊢ (R \in Mnd \land 0_{R} \in S \land S \subseteq {Base}_{R}) \to 0_{R} = 0_{(R ↾_{𝑠} S)}$
37	31 35 11 36	syl3anc	$⊢ φ \to 0_{R} = 0_{(R ↾_{𝑠} S)}$
38	37	ad3antrrr	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to 0_{R} = 0_{(R ↾_{𝑠} S)}$
39	22 28 38	3eqtr4d	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to x \cdot_{R} y = 0_{R}$
40	9 24 33	domneq0	$⊢ (R \in Domn \land x \in {Base}_{R} \land y \in {Base}_{R}) \to (x \cdot_{R} y = 0_{R} \leftrightarrow (x = 0_{R} \lor y = 0_{R}))$
41	40	biimpa	$⊢ ((R \in Domn \land x \in {Base}_{R} \land y \in {Base}_{R}) \land x \cdot_{R} y = 0_{R}) \to (x = 0_{R} \lor y = 0_{R})$
42	8 18 21 39 41	syl31anc	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to (x = 0_{R} \lor y = 0_{R})$
43	38	eqeq2d	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to (x = 0_{R} \leftrightarrow x = 0_{(R ↾_{𝑠} S)})$
44	38	eqeq2d	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to (y = 0_{R} \leftrightarrow y = 0_{(R ↾_{𝑠} S)})$
45	43 44	orbi12d	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to ((x = 0_{R} \lor y = 0_{R}) \leftrightarrow (x = 0_{(R ↾_{𝑠} S)} \lor y = 0_{(R ↾_{𝑠} S)}))$
46	42 45	mpbid	$⊢ (((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \land x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)}) \to (x = 0_{(R ↾_{𝑠} S)} \lor y = 0_{(R ↾_{𝑠} S)})$
47	46	ex	$⊢ ((φ \land x \in {Base}_{(R ↾_{𝑠} S)}) \land y \in {Base}_{(R ↾_{𝑠} S)}) \to (x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)} \to (x = 0_{(R ↾_{𝑠} S)} \lor y = 0_{(R ↾_{𝑠} S)}))$
48	47	anasss	$⊢ (φ \land (x \in {Base}_{(R ↾_{𝑠} S)} \land y \in {Base}_{(R ↾_{𝑠} S)})) \to (x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)} \to (x = 0_{(R ↾_{𝑠} S)} \lor y = 0_{(R ↾_{𝑠} S)}))$
49	48	ralrimivva	$⊢ φ \to \forall x \in {Base}_{(R ↾_{𝑠} S)} \forall y \in {Base}_{(R ↾_{𝑠} S)} (x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)} \to (x = 0_{(R ↾_{𝑠} S)} \lor y = 0_{(R ↾_{𝑠} S)}))$
50		eqid	$⊢ {Base}_{(R ↾_{𝑠} S)} = {Base}_{(R ↾_{𝑠} S)}$
51		eqid	$⊢ \cdot_{(R ↾_{𝑠} S)} = \cdot_{(R ↾_{𝑠} S)}$
52		eqid	$⊢ 0_{(R ↾_{𝑠} S)} = 0_{(R ↾_{𝑠} S)}$
53	50 51 52	isdomn	$⊢ R ↾_{𝑠} S \in Domn \leftrightarrow (R ↾_{𝑠} S \in NzRing \land \forall x \in {Base}_{(R ↾_{𝑠} S)} \forall y \in {Base}_{(R ↾_{𝑠} S)} (x \cdot_{(R ↾_{𝑠} S)} y = 0_{(R ↾_{𝑠} S)} \to (x = 0_{(R ↾_{𝑠} S)} \lor y = 0_{(R ↾_{𝑠} S)})))$
54	7 49 53	sylanbrc	$⊢ φ \to R ↾_{𝑠} S \in Domn$

Metamath Proof Explorer

Theorem subrdom

Proof