suborng

Description: Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018)

		Ref	Expression
	Assertion	suborng	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A \in oRing$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A \in Ring$
2		ringgrp	$⊢ R ↾_{𝑠} A \in Ring \to R ↾_{𝑠} A \in Grp$
3	2	adantl	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A \in Grp$
4		orngogrp	$⊢ R \in oRing \to R \in oGrp$
5		isogrp	$⊢ R \in oGrp \leftrightarrow (R \in Grp \land R \in oMnd)$
6	5	simprbi	$⊢ R \in oGrp \to R \in oMnd$
7	4 6	syl	$⊢ R \in oRing \to R \in oMnd$
8		ringmnd	$⊢ R ↾_{𝑠} A \in Ring \to R ↾_{𝑠} A \in Mnd$
9		submomnd	$⊢ (R \in oMnd \land R ↾_{𝑠} A \in Mnd) \to R ↾_{𝑠} A \in oMnd$
10	7 8 9	syl2an	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A \in oMnd$
11		isogrp	$⊢ R ↾_{𝑠} A \in oGrp \leftrightarrow (R ↾_{𝑠} A \in Grp \land R ↾_{𝑠} A \in oMnd)$
12	3 10 11	sylanbrc	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A \in oGrp$
13		simp-4l	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to R \in oRing$
14		reldmress	$⊢ Rel dom ↾_{𝑠}$
15	14	ovprc2	$⊢ \neg A \in V \to R ↾_{𝑠} A = \emptyset$
16	15	fveq2d	$⊢ \neg A \in V \to {Base}_{(R ↾_{𝑠} A)} = {Base}_{\emptyset}$
17	16	adantl	$⊢ ((R \in oRing \land R ↾_{𝑠} A \in Ring) \land \neg A \in V) \to {Base}_{(R ↾_{𝑠} A)} = {Base}_{\emptyset}$
18		base0	$⊢ \emptyset = {Base}_{\emptyset}$
19	17 18	eqtr4di	$⊢ ((R \in oRing \land R ↾_{𝑠} A \in Ring) \land \neg A \in V) \to {Base}_{(R ↾_{𝑠} A)} = \emptyset$
20		eqid	$⊢ {Base}_{(R ↾_{𝑠} A)} = {Base}_{(R ↾_{𝑠} A)}$
21		eqid	$⊢ 1_{(R ↾_{𝑠} A)} = 1_{(R ↾_{𝑠} A)}$
22	20 21	ringidcl	$⊢ R ↾_{𝑠} A \in Ring \to 1_{(R ↾_{𝑠} A)} \in {Base}_{(R ↾_{𝑠} A)}$
23	22	ne0d	$⊢ R ↾_{𝑠} A \in Ring \to {Base}_{(R ↾_{𝑠} A)} \neq \emptyset$
24	23	ad2antlr	$⊢ ((R \in oRing \land R ↾_{𝑠} A \in Ring) \land \neg A \in V) \to {Base}_{(R ↾_{𝑠} A)} \neq \emptyset$
25	24	neneqd	$⊢ ((R \in oRing \land R ↾_{𝑠} A \in Ring) \land \neg A \in V) \to \neg {Base}_{(R ↾_{𝑠} A)} = \emptyset$
26	19 25	condan	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to A \in V$
27		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
28		eqid	$⊢ {Base}_{R} = {Base}_{R}$
29	27 28	ressbas	$⊢ A \in V \to A \cap {Base}_{R} = {Base}_{(R ↾_{𝑠} A)}$
30		inss2	$⊢ A \cap {Base}_{R} \subseteq {Base}_{R}$
31	29 30	eqsstrrdi	$⊢ A \in V \to {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R}$
32	26 31	syl	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R}$
33	32	ad3antrrr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R}$
34		simpllr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to a \in {Base}_{(R ↾_{𝑠} A)}$
35	33 34	sseldd	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to a \in {Base}_{R}$
36		simprl	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a$
37		orngring	$⊢ R \in oRing \to R \in Ring$
38		ringgrp	$⊢ R \in Ring \to R \in Grp$
39	37 38	syl	$⊢ R \in oRing \to R \in Grp$
40	39	adantr	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R \in Grp$
41	28	ressinbas	$⊢ A \in V \to R ↾_{𝑠} A = R ↾_{𝑠} (A \cap {Base}_{R})$
42	29	oveq2d	$⊢ A \in V \to R ↾_{𝑠} (A \cap {Base}_{R}) = R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)}$
43	41 42	eqtrd	$⊢ A \in V \to R ↾_{𝑠} A = R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)}$
44	26 43	syl	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A = R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)}$
45	44 3	eqeltrrd	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)} \in Grp$
46	28	issubg	$⊢ {Base}_{(R ↾_{𝑠} A)} \in SubGrp (R) \leftrightarrow (R \in Grp \land {Base}_{(R ↾_{𝑠} A)} \subseteq {Base}_{R} \land R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)} \in Grp)$
47	40 32 45 46	syl3anbrc	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to {Base}_{(R ↾_{𝑠} A)} \in SubGrp (R)$
48		eqid	$⊢ R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)} = R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)}$
49		eqid	$⊢ 0_{R} = 0_{R}$
50	48 49	subg0	$⊢ {Base}_{(R ↾_{𝑠} A)} \in SubGrp (R) \to 0_{R} = 0_{(R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)})}$
51	47 50	syl	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to 0_{R} = 0_{(R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)})}$
52	44	fveq2d	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to 0_{(R ↾_{𝑠} A)} = 0_{(R ↾_{𝑠} {Base}_{(R ↾_{𝑠} A)})}$
53	51 52	eqtr4d	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to 0_{R} = 0_{(R ↾_{𝑠} A)}$
54	53	ad2antrr	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to 0_{R} = 0_{(R ↾_{𝑠} A)}$
55	26	ad2antrr	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to A \in V$
56		eqid	$⊢ \leq_{R} = \leq_{R}$
57	27 56	ressle	$⊢ A \in V \to \leq_{R} = \leq_{(R ↾_{𝑠} A)}$
58	55 57	syl	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to \leq_{R} = \leq_{(R ↾_{𝑠} A)}$
59		eqidd	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to a = a$
60	54 58 59	breq123d	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to (0_{R} \leq_{R} a \leftrightarrow 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a)$
61	60	adantr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to (0_{R} \leq_{R} a \leftrightarrow 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a)$
62	36 61	mpbird	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{R} \leq_{R} a$
63		simplr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to b \in {Base}_{(R ↾_{𝑠} A)}$
64	33 63	sseldd	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to b \in {Base}_{R}$
65		simprr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b$
66		eqidd	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to b = b$
67	54 58 66	breq123d	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to (0_{R} \leq_{R} b \leftrightarrow 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)$
68	67	adantr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to (0_{R} \leq_{R} b \leftrightarrow 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)$
69	65 68	mpbird	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{R} \leq_{R} b$
70		eqid	$⊢ \cdot_{R} = \cdot_{R}$
71	28 56 49 70	orngmul	$⊢ (R \in oRing \land (a \in {Base}_{R} \land 0_{R} \leq_{R} a) \land (b \in {Base}_{R} \land 0_{R} \leq_{R} b)) \to 0_{R} \leq_{R} (a \cdot_{R} b)$
72	13 35 62 64 69 71	syl122anc	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{R} \leq_{R} (a \cdot_{R} b)$
73	54	adantr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{R} = 0_{(R ↾_{𝑠} A)}$
74	58	adantr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to \leq_{R} = \leq_{(R ↾_{𝑠} A)}$
75	55	adantr	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to A \in V$
76	27 70	ressmulr	$⊢ A \in V \to \cdot_{R} = \cdot_{(R ↾_{𝑠} A)}$
77	75 76	syl	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to \cdot_{R} = \cdot_{(R ↾_{𝑠} A)}$
78	77	oveqd	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to a \cdot_{R} b = a \cdot_{(R ↾_{𝑠} A)} b$
79	73 74 78	breq123d	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to (0_{R} \leq_{R} (a \cdot_{R} b) \leftrightarrow 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} (a \cdot_{(R ↾_{𝑠} A)} b))$
80	72 79	mpbid	$⊢ ((((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \land (0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b)) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} (a \cdot_{(R ↾_{𝑠} A)} b)$
81	80	ex	$⊢ (((R \in oRing \land R ↾_{𝑠} A \in Ring) \land a \in {Base}_{(R ↾_{𝑠} A)}) \land b \in {Base}_{(R ↾_{𝑠} A)}) \to ((0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} (a \cdot_{(R ↾_{𝑠} A)} b))$
82	81	anasss	$⊢ ((R \in oRing \land R ↾_{𝑠} A \in Ring) \land (a \in {Base}_{(R ↾_{𝑠} A)} \land b \in {Base}_{(R ↾_{𝑠} A)})) \to ((0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} (a \cdot_{(R ↾_{𝑠} A)} b))$
83	82	ralrimivva	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to \forall a \in {Base}_{(R ↾_{𝑠} A)} \forall b \in {Base}_{(R ↾_{𝑠} A)} ((0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} (a \cdot_{(R ↾_{𝑠} A)} b))$
84		eqid	$⊢ 0_{(R ↾_{𝑠} A)} = 0_{(R ↾_{𝑠} A)}$
85		eqid	$⊢ \cdot_{(R ↾_{𝑠} A)} = \cdot_{(R ↾_{𝑠} A)}$
86		eqid	$⊢ \leq_{(R ↾_{𝑠} A)} = \leq_{(R ↾_{𝑠} A)}$
87	20 84 85 86	isorng	$⊢ R ↾_{𝑠} A \in oRing \leftrightarrow (R ↾_{𝑠} A \in Ring \land R ↾_{𝑠} A \in oGrp \land \forall a \in {Base}_{(R ↾_{𝑠} A)} \forall b \in {Base}_{(R ↾_{𝑠} A)} ((0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} a \land 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} b) \to 0_{(R ↾_{𝑠} A)} \leq_{(R ↾_{𝑠} A)} (a \cdot_{(R ↾_{𝑠} A)} b)))$
88	1 12 83 87	syl3anbrc	$⊢ (R \in oRing \land R ↾_{𝑠} A \in Ring) \to R ↾_{𝑠} A \in oRing$

Metamath Proof Explorer

Theorem suborng

Proof