issubrng2

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

	Ref	Expression
Hypotheses	issubrng2.b	$⊢ B = {Base}_{R}$
	issubrng2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	issubrng2	$⊢ R \in Rng \to (A \in SubRng (R) \leftrightarrow (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A))$

Proof

Step	Hyp	Ref	Expression
1		issubrng2.b	$⊢ B = {Base}_{R}$
2		issubrng2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		subrngsubg	$⊢ A \in SubRng (R) \to A \in SubGrp (R)$
4	2	subrngmcl	$⊢ (A \in SubRng (R) \land x \in A \land y \in A) \to x \underset{˙}{\cdot} y \in A$
5	4	3expb	$⊢ (A \in SubRng (R) \land (x \in A \land y \in A)) \to x \underset{˙}{\cdot} y \in A$
6	5	ralrimivva	$⊢ A \in SubRng (R) \to \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A$
7	3 6	jca	$⊢ A \in SubRng (R) \to (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)$
8		simpl	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to R \in Rng$
9		simprl	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A \in SubGrp (R)$
10		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
11	10	subgbas	$⊢ A \in SubGrp (R) \to A = {Base}_{(R ↾_{𝑠} A)}$
12	9 11	syl	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A = {Base}_{(R ↾_{𝑠} A)}$
13		eqid	$⊢ +_{R} = +_{R}$
14	10 13	ressplusg	$⊢ A \in SubGrp (R) \to +_{R} = +_{(R ↾_{𝑠} A)}$
15	9 14	syl	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to +_{R} = +_{(R ↾_{𝑠} A)}$
16	10 2	ressmulr	$⊢ A \in SubGrp (R) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
17	9 16	syl	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
18		rngabl	$⊢ R \in Rng \to R \in Abel$
19	10	subgabl	$⊢ (R \in Abel \land A \in SubGrp (R)) \to R ↾_{𝑠} A \in Abel$
20	18 9 19	syl2an2r	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to R ↾_{𝑠} A \in Abel$
21		simprr	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A$
22		oveq1	$⊢ x = u \to x \underset{˙}{\cdot} y = u \underset{˙}{\cdot} y$
23	22	eleq1d	$⊢ x = u \to (x \underset{˙}{\cdot} y \in A \leftrightarrow u \underset{˙}{\cdot} y \in A)$
24		oveq2	$⊢ y = v \to u \underset{˙}{\cdot} y = u \underset{˙}{\cdot} v$
25	24	eleq1d	$⊢ y = v \to (u \underset{˙}{\cdot} y \in A \leftrightarrow u \underset{˙}{\cdot} v \in A)$
26	23 25	rspc2v	$⊢ (u \in A \land v \in A) \to (\forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A \to u \underset{˙}{\cdot} v \in A)$
27	21 26	syl5com	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to ((u \in A \land v \in A) \to u \underset{˙}{\cdot} v \in A)$
28	27	3impib	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land u \in A \land v \in A) \to u \underset{˙}{\cdot} v \in A$
29	1	subgss	$⊢ A \in SubGrp (R) \to A \subseteq B$
30	9 29	syl	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A \subseteq B$
31	30	sseld	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (u \in A \to u \in B)$
32	30	sseld	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (v \in A \to v \in B)$
33	30	sseld	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (w \in A \to w \in B)$
34	31 32 33	3anim123d	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to ((u \in A \land v \in A \land w \in A) \to (u \in B \land v \in B \land w \in B))$
35	34	imp	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in A \land v \in A \land w \in A)) \to (u \in B \land v \in B \land w \in B)$
36	1 2	rngass	$⊢ (R \in Rng \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{\cdot} v) \underset{˙}{\cdot} w = u \underset{˙}{\cdot} (v \underset{˙}{\cdot} w)$
37	36	adantlr	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{\cdot} v) \underset{˙}{\cdot} w = u \underset{˙}{\cdot} (v \underset{˙}{\cdot} w)$
38	35 37	syldan	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in A \land v \in A \land w \in A)) \to (u \underset{˙}{\cdot} v) \underset{˙}{\cdot} w = u \underset{˙}{\cdot} (v \underset{˙}{\cdot} w)$
39	1 13 2	rngdi	$⊢ (R \in Rng \land (u \in B \land v \in B \land w \in B)) \to u \underset{˙}{\cdot} (v +_{R} w) = (u \underset{˙}{\cdot} v) +_{R} (u \underset{˙}{\cdot} w)$
40	39	adantlr	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in B \land v \in B \land w \in B)) \to u \underset{˙}{\cdot} (v +_{R} w) = (u \underset{˙}{\cdot} v) +_{R} (u \underset{˙}{\cdot} w)$
41	35 40	syldan	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in A \land v \in A \land w \in A)) \to u \underset{˙}{\cdot} (v +_{R} w) = (u \underset{˙}{\cdot} v) +_{R} (u \underset{˙}{\cdot} w)$
42	1 13 2	rngdir	$⊢ (R \in Rng \land (u \in B \land v \in B \land w \in B)) \to (u +_{R} v) \underset{˙}{\cdot} w = (u \underset{˙}{\cdot} w) +_{R} (v \underset{˙}{\cdot} w)$
43	42	adantlr	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in B \land v \in B \land w \in B)) \to (u +_{R} v) \underset{˙}{\cdot} w = (u \underset{˙}{\cdot} w) +_{R} (v \underset{˙}{\cdot} w)$
44	35 43	syldan	$⊢ ((R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land (u \in A \land v \in A \land w \in A)) \to (u +_{R} v) \underset{˙}{\cdot} w = (u \underset{˙}{\cdot} w) +_{R} (v \underset{˙}{\cdot} w)$
45	12 15 17 20 28 38 41 44	isrngd	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to R ↾_{𝑠} A \in Rng$
46	1	issubrng	$⊢ A \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B)$
47	8 45 30 46	syl3anbrc	$⊢ (R \in Rng \land (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A \in SubRng (R)$
48	47	ex	$⊢ R \in Rng \to ((A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A) \to A \in SubRng (R))$
49	7 48	impbid2	$⊢ R \in Rng \to (A \in SubRng (R) \leftrightarrow (A \in SubGrp (R) \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A))$

Metamath Proof Explorer

Theorem issubrng2

Proof