issubrg2

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

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

Proof

Step	Hyp	Ref	Expression
1		issubrg2.b	$⊢ B = {Base}_{R}$
2		issubrg2.o	$⊢ \underset{˙}{1} = 1_{R}$
3		issubrg2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		subrgsubg	$⊢ A \in SubRing (R) \to A \in SubGrp (R)$
5	2	subrg1cl	$⊢ A \in SubRing (R) \to \underset{˙}{1} \in A$
6	3	subrgmcl	$⊢ (A \in SubRing (R) \land x \in A \land y \in A) \to x \underset{˙}{\cdot} y \in A$
7	6	3expb	$⊢ (A \in SubRing (R) \land (x \in A \land y \in A)) \to x \underset{˙}{\cdot} y \in A$
8	7	ralrimivva	$⊢ A \in SubRing (R) \to \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A$
9	4 5 8	3jca	$⊢ A \in SubRing (R) \to (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)$
10		simpl	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to R \in Ring$
11		simpr1	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A \in SubGrp (R)$
12		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
13	12	subgbas	$⊢ A \in SubGrp (R) \to A = {Base}_{(R ↾_{𝑠} A)}$
14	11 13	syl	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A = {Base}_{(R ↾_{𝑠} A)}$
15		eqid	$⊢ +_{R} = +_{R}$
16	12 15	ressplusg	$⊢ A \in SubGrp (R) \to +_{R} = +_{(R ↾_{𝑠} A)}$
17	11 16	syl	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to +_{R} = +_{(R ↾_{𝑠} A)}$
18	12 3	ressmulr	$⊢ A \in SubGrp (R) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
19	11 18	syl	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
20	12	subggrp	$⊢ A \in SubGrp (R) \to R ↾_{𝑠} A \in Grp$
21	11 20	syl	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to R ↾_{𝑠} A \in Grp$
22		simpr3	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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$
23		oveq1	$⊢ x = u \to x \underset{˙}{\cdot} y = u \underset{˙}{\cdot} y$
24	23	eleq1d	$⊢ x = u \to (x \underset{˙}{\cdot} y \in A \leftrightarrow u \underset{˙}{\cdot} y \in A)$
25		oveq2	$⊢ y = v \to u \underset{˙}{\cdot} y = u \underset{˙}{\cdot} v$
26	25	eleq1d	$⊢ y = v \to (u \underset{˙}{\cdot} y \in A \leftrightarrow u \underset{˙}{\cdot} v \in A)$
27	24 26	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)$
28	22 27	syl5com	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
29	28	3impib	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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$
30	1	subgss	$⊢ A \in SubGrp (R) \to A \subseteq B$
31	11 30	syl	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A \subseteq B$
32	31	sseld	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (u \in A \to u \in B)$
33	31	sseld	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (v \in A \to v \in B)$
34	31	sseld	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (w \in A \to w \in B)$
35	32 33 34	3anim123d	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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))$
36	35	imp	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
37	1 3	ringass	$⊢ (R \in Ring \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	37	adantlr	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
39	36 38	syldan	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
40	1 15 3	ringdi	$⊢ (R \in Ring \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	40	adantlr	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
42	36 41	syldan	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
43	1 15 3	ringdir	$⊢ (R \in Ring \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	43	adantlr	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
45	36 44	syldan	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \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)$
46		simpr2	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to \underset{˙}{1} \in A$
47	32	imp	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land u \in A) \to u \in B$
48	1 3 2	ringlidm	$⊢ (R \in Ring \land u \in B) \to \underset{˙}{1} \underset{˙}{\cdot} u = u$
49	48	adantlr	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land u \in B) \to \underset{˙}{1} \underset{˙}{\cdot} u = u$
50	47 49	syldan	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land u \in A) \to \underset{˙}{1} \underset{˙}{\cdot} u = u$
51	1 3 2	ringridm	$⊢ (R \in Ring \land u \in B) \to u \underset{˙}{\cdot} \underset{˙}{1} = u$
52	51	adantlr	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land u \in B) \to u \underset{˙}{\cdot} \underset{˙}{1} = u$
53	47 52	syldan	$⊢ ((R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \land u \in A) \to u \underset{˙}{\cdot} \underset{˙}{1} = u$
54	14 17 19 21 29 39 42 45 46 50 53	isringd	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to R ↾_{𝑠} A \in Ring$
55	31 46	jca	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to (A \subseteq B \land \underset{˙}{1} \in A)$
56	1 2	issubrg	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A))$
57	10 54 55 56	syl21anbrc	$⊢ (R \in Ring \land (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A)) \to A \in SubRing (R)$
58	57	ex	$⊢ R \in Ring \to ((A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A) \to A \in SubRing (R))$
59	9 58	impbid2	$⊢ R \in Ring \to (A \in SubRing (R) \leftrightarrow (A \in SubGrp (R) \land \underset{˙}{1} \in A \land \forall x \in A \forall y \in A x \underset{˙}{\cdot} y \in A))$

Metamath Proof Explorer

Theorem issubrg2

Proof