idlinsubrg

Description: The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024)

	Ref	Expression
Hypotheses	idlinsubrg.s	$⊢ S = R ↾_{𝑠} A$
	idlinsubrg.u	$⊢ U = LIdeal (R)$
	idlinsubrg.v	$⊢ V = LIdeal (S)$
Assertion	idlinsubrg	$⊢ (A \in SubRing (R) \land I \in U) \to I \cap A \in V$

Proof

Step	Hyp	Ref	Expression
1		idlinsubrg.s	$⊢ S = R ↾_{𝑠} A$
2		idlinsubrg.u	$⊢ U = LIdeal (R)$
3		idlinsubrg.v	$⊢ V = LIdeal (S)$
4		inss2	$⊢ I \cap A \subseteq A$
5	1	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{S}$
6	4 5	sseqtrid	$⊢ A \in SubRing (R) \to I \cap A \subseteq {Base}_{S}$
7	6	adantr	$⊢ (A \in SubRing (R) \land I \in U) \to I \cap A \subseteq {Base}_{S}$
8		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
9		eqid	$⊢ 0_{R} = 0_{R}$
10	2 9	lidl0cl	$⊢ (R \in Ring \land I \in U) \to 0_{R} \in I$
11	8 10	sylan	$⊢ (A \in SubRing (R) \land I \in U) \to 0_{R} \in I$
12		subrgsubg	$⊢ A \in SubRing (R) \to A \in SubGrp (R)$
13		subgsubm	$⊢ A \in SubGrp (R) \to A \in SubMnd (R)$
14	9	subm0cl	$⊢ A \in SubMnd (R) \to 0_{R} \in A$
15	12 13 14	3syl	$⊢ A \in SubRing (R) \to 0_{R} \in A$
16	15	adantr	$⊢ (A \in SubRing (R) \land I \in U) \to 0_{R} \in A$
17	11 16	elind	$⊢ (A \in SubRing (R) \land I \in U) \to 0_{R} \in (I \cap A)$
18	17	ne0d	$⊢ (A \in SubRing (R) \land I \in U) \to I \cap A \neq \emptyset$
19		eqid	$⊢ +_{R} = +_{R}$
20	1 19	ressplusg	$⊢ A \in SubRing (R) \to +_{R} = +_{S}$
21		eqid	$⊢ \cdot_{R} = \cdot_{R}$
22	1 21	ressmulr	$⊢ A \in SubRing (R) \to \cdot_{R} = \cdot_{S}$
23	22	oveqd	$⊢ A \in SubRing (R) \to x \cdot_{R} a = x \cdot_{S} a$
24		eqidd	$⊢ A \in SubRing (R) \to b = b$
25	20 23 24	oveq123d	$⊢ A \in SubRing (R) \to (x \cdot_{R} a) +_{R} b = (x \cdot_{S} a) +_{S} b$
26	25	ad4antr	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to (x \cdot_{R} a) +_{R} b = (x \cdot_{S} a) +_{S} b$
27	8	ad4antr	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to R \in Ring$
28		simp-4r	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to I \in U$
29		eqid	$⊢ {Base}_{R} = {Base}_{R}$
30	29	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
31	5 30	eqsstrrd	$⊢ A \in SubRing (R) \to {Base}_{S} \subseteq {Base}_{R}$
32	31	adantr	$⊢ (A \in SubRing (R) \land I \in U) \to {Base}_{S} \subseteq {Base}_{R}$
33	32	sselda	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to x \in {Base}_{R}$
34	33	ad2antrr	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to x \in {Base}_{R}$
35		inss1	$⊢ I \cap A \subseteq I$
36	35	a1i	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to I \cap A \subseteq I$
37	36	sselda	$⊢ (((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \to a \in I$
38	37	adantr	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to a \in I$
39	2 29 21	lidlmcl	$⊢ ((R \in Ring \land I \in U) \land (x \in {Base}_{R} \land a \in I)) \to x \cdot_{R} a \in I$
40	27 28 34 38 39	syl22anc	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to x \cdot_{R} a \in I$
41	35	a1i	$⊢ (((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \to I \cap A \subseteq I$
42	41	sselda	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to b \in I$
43	2 19	lidlacl	$⊢ ((R \in Ring \land I \in U) \land (x \cdot_{R} a \in I \land b \in I)) \to (x \cdot_{R} a) +_{R} b \in I$
44	27 28 40 42 43	syl22anc	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to (x \cdot_{R} a) +_{R} b \in I$
45		simp-4l	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to A \in SubRing (R)$
46		simpr	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to x \in {Base}_{S}$
47	5	ad2antrr	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to A = {Base}_{S}$
48	46 47	eleqtrrd	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to x \in A$
49	48	ad2antrr	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to x \in A$
50	4	a1i	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to I \cap A \subseteq A$
51	50	sselda	$⊢ (((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \to a \in A$
52	51	adantr	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to a \in A$
53	21	subrgmcl	$⊢ (A \in SubRing (R) \land x \in A \land a \in A) \to x \cdot_{R} a \in A$
54	45 49 52 53	syl3anc	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to x \cdot_{R} a \in A$
55	4	a1i	$⊢ (((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \to I \cap A \subseteq A$
56	55	sselda	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to b \in A$
57	19	subrgacl	$⊢ (A \in SubRing (R) \land x \cdot_{R} a \in A \land b \in A) \to (x \cdot_{R} a) +_{R} b \in A$
58	45 54 56 57	syl3anc	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to (x \cdot_{R} a) +_{R} b \in A$
59	44 58	elind	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to (x \cdot_{R} a) +_{R} b \in (I \cap A)$
60	26 59	eqeltrrd	$⊢ ((((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land a \in (I \cap A)) \land b \in (I \cap A)) \to (x \cdot_{S} a) +_{S} b \in (I \cap A)$
61	60	anasss	$⊢ (((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \land (a \in (I \cap A) \land b \in (I \cap A))) \to (x \cdot_{S} a) +_{S} b \in (I \cap A)$
62	61	ralrimivva	$⊢ ((A \in SubRing (R) \land I \in U) \land x \in {Base}_{S}) \to \forall a \in (I \cap A) \forall b \in (I \cap A) (x \cdot_{S} a) +_{S} b \in (I \cap A)$
63	62	ralrimiva	$⊢ (A \in SubRing (R) \land I \in U) \to \forall x \in {Base}_{S} \forall a \in (I \cap A) \forall b \in (I \cap A) (x \cdot_{S} a) +_{S} b \in (I \cap A)$
64		eqid	$⊢ {Base}_{S} = {Base}_{S}$
65		eqid	$⊢ +_{S} = +_{S}$
66		eqid	$⊢ \cdot_{S} = \cdot_{S}$
67	3 64 65 66	islidl	$⊢ I \cap A \in V \leftrightarrow (I \cap A \subseteq {Base}_{S} \land I \cap A \neq \emptyset \land \forall x \in {Base}_{S} \forall a \in (I \cap A) \forall b \in (I \cap A) (x \cdot_{S} a) +_{S} b \in (I \cap A))$
68	7 18 63 67	syl3anbrc	$⊢ (A \in SubRing (R) \land I \in U) \to I \cap A \in V$

Metamath Proof Explorer

Theorem idlinsubrg

Proof