intidl

Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

		Ref	Expression
	Assertion	intidl	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to ⋂ C \in Idl (R)$

Proof

Step	Hyp	Ref	Expression
1		intssuni	$⊢ C \neq \emptyset \to ⋂ C \subseteq ⋃ C$
2	1	3ad2ant2	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to ⋂ C \subseteq ⋃ C$
3		ssel2	$⊢ (C \subseteq Idl (R) \land i \in C) \to i \in Idl (R)$
4		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
5		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
6	4 5	idlss	$⊢ (R \in RingOps \land i \in Idl (R)) \to i \subseteq ran 1^{st} (R)$
7	3 6	sylan2	$⊢ (R \in RingOps \land (C \subseteq Idl (R) \land i \in C)) \to i \subseteq ran 1^{st} (R)$
8	7	anassrs	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land i \in C) \to i \subseteq ran 1^{st} (R)$
9	8	ralrimiva	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to \forall i \in C i \subseteq ran 1^{st} (R)$
10	9	3adant2	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to \forall i \in C i \subseteq ran 1^{st} (R)$
11		unissb	$⊢ ⋃ C \subseteq ran 1^{st} (R) \leftrightarrow \forall i \in C i \subseteq ran 1^{st} (R)$
12	10 11	sylibr	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to ⋃ C \subseteq ran 1^{st} (R)$
13	2 12	sstrd	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to ⋂ C \subseteq ran 1^{st} (R)$
14		eqid	$⊢ GId (1^{st} (R)) = GId (1^{st} (R))$
15	4 14	idl0cl	$⊢ (R \in RingOps \land i \in Idl (R)) \to GId (1^{st} (R)) \in i$
16	3 15	sylan2	$⊢ (R \in RingOps \land (C \subseteq Idl (R) \land i \in C)) \to GId (1^{st} (R)) \in i$
17	16	anassrs	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land i \in C) \to GId (1^{st} (R)) \in i$
18	17	ralrimiva	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to \forall i \in C GId (1^{st} (R)) \in i$
19		fvex	$⊢ GId (1^{st} (R)) \in V$
20	19	elint2	$⊢ GId (1^{st} (R)) \in ⋂ C \leftrightarrow \forall i \in C GId (1^{st} (R)) \in i$
21	18 20	sylibr	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to GId (1^{st} (R)) \in ⋂ C$
22	21	3adant2	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to GId (1^{st} (R)) \in ⋂ C$
23		vex	$⊢ x \in V$
24	23	elint2	$⊢ x \in ⋂ C \leftrightarrow \forall i \in C x \in i$
25		vex	$⊢ y \in V$
26	25	elint2	$⊢ y \in ⋂ C \leftrightarrow \forall i \in C y \in i$
27		r19.26	$⊢ \forall i \in C (x \in i \land y \in i) \leftrightarrow (\forall i \in C x \in i \land \forall i \in C y \in i)$
28	4	idladdcl	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (x \in i \land y \in i)) \to x 1^{st} (R) y \in i$
29	28	ex	$⊢ (R \in RingOps \land i \in Idl (R)) \to ((x \in i \land y \in i) \to x 1^{st} (R) y \in i)$
30	3 29	sylan2	$⊢ (R \in RingOps \land (C \subseteq Idl (R) \land i \in C)) \to ((x \in i \land y \in i) \to x 1^{st} (R) y \in i)$
31	30	anassrs	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land i \in C) \to ((x \in i \land y \in i) \to x 1^{st} (R) y \in i)$
32	31	ralimdva	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to (\forall i \in C (x \in i \land y \in i) \to \forall i \in C x 1^{st} (R) y \in i)$
33		ovex	$⊢ x 1^{st} (R) y \in V$
34	33	elint2	$⊢ x 1^{st} (R) y \in ⋂ C \leftrightarrow \forall i \in C x 1^{st} (R) y \in i$
35	32 34	imbitrrdi	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to (\forall i \in C (x \in i \land y \in i) \to x 1^{st} (R) y \in ⋂ C)$
36	27 35	biimtrrid	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to ((\forall i \in C x \in i \land \forall i \in C y \in i) \to x 1^{st} (R) y \in ⋂ C)$
37	36	expdimp	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land \forall i \in C x \in i) \to (\forall i \in C y \in i \to x 1^{st} (R) y \in ⋂ C)$
38	26 37	biimtrid	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land \forall i \in C x \in i) \to (y \in ⋂ C \to x 1^{st} (R) y \in ⋂ C)$
39	38	ralrimiv	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land \forall i \in C x \in i) \to \forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C$
40		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
41	4 40 5	idllmulcl	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (x \in i \land z \in ran 1^{st} (R))) \to z 2^{nd} (R) x \in i$
42	41	anass1rs	$⊢ (((R \in RingOps \land i \in Idl (R)) \land z \in ran 1^{st} (R)) \land x \in i) \to z 2^{nd} (R) x \in i$
43	42	ex	$⊢ ((R \in RingOps \land i \in Idl (R)) \land z \in ran 1^{st} (R)) \to (x \in i \to z 2^{nd} (R) x \in i)$
44	43	an32s	$⊢ ((R \in RingOps \land z \in ran 1^{st} (R)) \land i \in Idl (R)) \to (x \in i \to z 2^{nd} (R) x \in i)$
45	3 44	sylan2	$⊢ ((R \in RingOps \land z \in ran 1^{st} (R)) \land (C \subseteq Idl (R) \land i \in C)) \to (x \in i \to z 2^{nd} (R) x \in i)$
46	45	an4s	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land (z \in ran 1^{st} (R) \land i \in C)) \to (x \in i \to z 2^{nd} (R) x \in i)$
47	46	anassrs	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land i \in C) \to (x \in i \to z 2^{nd} (R) x \in i)$
48	47	ralimdva	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \to (\forall i \in C x \in i \to \forall i \in C z 2^{nd} (R) x \in i)$
49	48	imp	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land \forall i \in C x \in i) \to \forall i \in C z 2^{nd} (R) x \in i$
50		ovex	$⊢ z 2^{nd} (R) x \in V$
51	50	elint2	$⊢ z 2^{nd} (R) x \in ⋂ C \leftrightarrow \forall i \in C z 2^{nd} (R) x \in i$
52	49 51	sylibr	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land \forall i \in C x \in i) \to z 2^{nd} (R) x \in ⋂ C$
53	4 40 5	idlrmulcl	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (x \in i \land z \in ran 1^{st} (R))) \to x 2^{nd} (R) z \in i$
54	53	anass1rs	$⊢ (((R \in RingOps \land i \in Idl (R)) \land z \in ran 1^{st} (R)) \land x \in i) \to x 2^{nd} (R) z \in i$
55	54	ex	$⊢ ((R \in RingOps \land i \in Idl (R)) \land z \in ran 1^{st} (R)) \to (x \in i \to x 2^{nd} (R) z \in i)$
56	55	an32s	$⊢ ((R \in RingOps \land z \in ran 1^{st} (R)) \land i \in Idl (R)) \to (x \in i \to x 2^{nd} (R) z \in i)$
57	3 56	sylan2	$⊢ ((R \in RingOps \land z \in ran 1^{st} (R)) \land (C \subseteq Idl (R) \land i \in C)) \to (x \in i \to x 2^{nd} (R) z \in i)$
58	57	an4s	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land (z \in ran 1^{st} (R) \land i \in C)) \to (x \in i \to x 2^{nd} (R) z \in i)$
59	58	anassrs	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land i \in C) \to (x \in i \to x 2^{nd} (R) z \in i)$
60	59	ralimdva	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \to (\forall i \in C x \in i \to \forall i \in C x 2^{nd} (R) z \in i)$
61	60	imp	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land \forall i \in C x \in i) \to \forall i \in C x 2^{nd} (R) z \in i$
62		ovex	$⊢ x 2^{nd} (R) z \in V$
63	62	elint2	$⊢ x 2^{nd} (R) z \in ⋂ C \leftrightarrow \forall i \in C x 2^{nd} (R) z \in i$
64	61 63	sylibr	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land \forall i \in C x \in i) \to x 2^{nd} (R) z \in ⋂ C$
65	52 64	jca	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land z \in ran 1^{st} (R)) \land \forall i \in C x \in i) \to (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C)$
66	65	an32s	$⊢ (((R \in RingOps \land C \subseteq Idl (R)) \land \forall i \in C x \in i) \land z \in ran 1^{st} (R)) \to (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C)$
67	66	ralrimiva	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land \forall i \in C x \in i) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C)$
68	39 67	jca	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land \forall i \in C x \in i) \to (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C))$
69	68	ex	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to (\forall i \in C x \in i \to (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C)))$
70	24 69	biimtrid	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to (x \in ⋂ C \to (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C)))$
71	70	ralrimiv	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to \forall x \in ⋂ C (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C))$
72	71	3adant2	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to \forall x \in ⋂ C (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C))$
73	4 40 5 14	isidl	$⊢ R \in RingOps \to (⋂ C \in Idl (R) \leftrightarrow (⋂ C \subseteq ran 1^{st} (R) \land GId (1^{st} (R)) \in ⋂ C \land \forall x \in ⋂ C (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C))))$
74	73	3ad2ant1	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to (⋂ C \in Idl (R) \leftrightarrow (⋂ C \subseteq ran 1^{st} (R) \land GId (1^{st} (R)) \in ⋂ C \land \forall x \in ⋂ C (\forall y \in ⋂ C x 1^{st} (R) y \in ⋂ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋂ C \land x 2^{nd} (R) z \in ⋂ C))))$
75	13 22 72 74	mpbir3and	$⊢ (R \in RingOps \land C \neq \emptyset \land C \subseteq Idl (R)) \to ⋂ C \in Idl (R)$

Metamath Proof Explorer

Theorem intidl

Proof