intlidl

Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024)

		Ref	Expression
	Assertion	intlidl	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋂ C \in LIdeal (R)$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to C \subseteq LIdeal (R)$
2	1	sselda	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land i \in C) \to i \in LIdeal (R)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ LIdeal (R) = LIdeal (R)$
5	3 4	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq {Base}_{R}$
6	2 5	syl	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land i \in C) \to i \subseteq {Base}_{R}$
7	6	ralrimiva	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to \forall i \in C i \subseteq {Base}_{R}$
8		pwssb	$⊢ C \subseteq 𝒫 {Base}_{R} \leftrightarrow \forall i \in C i \subseteq {Base}_{R}$
9	7 8	sylibr	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to C \subseteq 𝒫 {Base}_{R}$
10		simp2	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to C \neq \emptyset$
11		intss2	$⊢ C \subseteq 𝒫 {Base}_{R} \to (C \neq \emptyset \to ⋂ C \subseteq {Base}_{R})$
12	11	imp	$⊢ (C \subseteq 𝒫 {Base}_{R} \land C \neq \emptyset) \to ⋂ C \subseteq {Base}_{R}$
13	9 10 12	syl2anc	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋂ C \subseteq {Base}_{R}$
14		simpl1	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land i \in C) \to R \in Ring$
15		eqid	$⊢ 0_{R} = 0_{R}$
16	4 15	lidl0cl	$⊢ (R \in Ring \land i \in LIdeal (R)) \to 0_{R} \in i$
17	14 2 16	syl2anc	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land i \in C) \to 0_{R} \in i$
18	17	ralrimiva	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to \forall i \in C 0_{R} \in i$
19		fvex	$⊢ 0_{R} \in V$
20	19	elint2	$⊢ 0_{R} \in ⋂ C \leftrightarrow \forall i \in C 0_{R} \in i$
21	18 20	sylibr	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to 0_{R} \in ⋂ C$
22	21	ne0d	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋂ C \neq \emptyset$
23	14	ad5ant15	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to R \in Ring$
24	2	ad5ant15	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to i \in LIdeal (R)$
25		simp-4r	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to x \in {Base}_{R}$
26		simpllr	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to a \in ⋂ C$
27		simpr	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to i \in C$
28		elinti	$⊢ a \in ⋂ C \to (i \in C \to a \in i)$
29	28	imp	$⊢ (a \in ⋂ C \land i \in C) \to a \in i$
30	26 27 29	syl2anc	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to a \in i$
31		eqid	$⊢ \cdot_{R} = \cdot_{R}$
32	4 3 31	lidlmcl	$⊢ ((R \in Ring \land i \in LIdeal (R)) \land (x \in {Base}_{R} \land a \in i)) \to x \cdot_{R} a \in i$
33	23 24 25 30 32	syl22anc	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to x \cdot_{R} a \in i$
34		elinti	$⊢ b \in ⋂ C \to (i \in C \to b \in i)$
35	34	imp	$⊢ (b \in ⋂ C \land i \in C) \to b \in i$
36	35	adantll	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to b \in i$
37		eqid	$⊢ +_{R} = +_{R}$
38	4 37	lidlacl	$⊢ ((R \in Ring \land i \in LIdeal (R)) \land (x \cdot_{R} a \in i \land b \in i)) \to (x \cdot_{R} a) +_{R} b \in i$
39	23 24 33 36 38	syl22anc	$⊢ (((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \land i \in C) \to (x \cdot_{R} a) +_{R} b \in i$
40	39	ralrimiva	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \to \forall i \in C (x \cdot_{R} a) +_{R} b \in i$
41		ovex	$⊢ (x \cdot_{R} a) +_{R} b \in V$
42	41	elint2	$⊢ (x \cdot_{R} a) +_{R} b \in ⋂ C \leftrightarrow \forall i \in C (x \cdot_{R} a) +_{R} b \in i$
43	40 42	sylibr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \land b \in ⋂ C) \to (x \cdot_{R} a) +_{R} b \in ⋂ C$
44	43	ralrimiva	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land x \in {Base}_{R}) \land a \in ⋂ C) \to \forall b \in ⋂ C (x \cdot_{R} a) +_{R} b \in ⋂ C$
45	44	anasss	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (x \in {Base}_{R} \land a \in ⋂ C)) \to \forall b \in ⋂ C (x \cdot_{R} a) +_{R} b \in ⋂ C$
46	45	ralrimivva	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to \forall x \in {Base}_{R} \forall a \in ⋂ C \forall b \in ⋂ C (x \cdot_{R} a) +_{R} b \in ⋂ C$
47	4 3 37 31	islidl	$⊢ ⋂ C \in LIdeal (R) \leftrightarrow (⋂ C \subseteq {Base}_{R} \land ⋂ C \neq \emptyset \land \forall x \in {Base}_{R} \forall a \in ⋂ C \forall b \in ⋂ C (x \cdot_{R} a) +_{R} b \in ⋂ C)$
48	13 22 46 47	syl3anbrc	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋂ C \in LIdeal (R)$

Metamath Proof Explorer

Theorem intlidl

Proof