Theorem zarclsiin 34261

Description: In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024.)

Hypotheses

Ref	Expression
zarclsx.1	⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})
zarclsiin.1	⊢ 𝐾 = (RSpan‘𝑅)

Assertion

Ref	Expression
zarclsiin	⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) = (𝑉‘(𝐾‘∪ 𝑇)))

Distinct variable groups:   𝑅,𝑖,𝑗,𝑙   𝑉,𝑙   𝑖,𝐾,𝑗,𝑙   𝑇,𝑖,𝑗,𝑙

Allowed substitution hints:   𝑉(𝑖,𝑗)

Proof of Theorem zarclsiin

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 3963	. . . . 5 ⊢ (𝑗 = 𝑝 → ((𝐾‘∪ 𝑇) ⊆ 𝑗 ↔ (𝐾‘∪ 𝑇) ⊆ 𝑝))
2		simpl3 1212	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑇 ≠ ∅)
3		zarclsx.1	. . . . . . . . . . . 12 ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})
4	3	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}))
5		sseq1 3962	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑙 → (𝑖 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑗))
6	5	rabbidv 3423	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑙 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
7	6	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) ∧ 𝑖 = 𝑙) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
8		simp2 1155	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑇 ⊆ (LIdeal‘𝑅))
9	8	sselda 3937	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → 𝑙 ∈ (LIdeal‘𝑅))
10		fvex 6894	. . . . . . . . . . . . 13 ⊢ (PrmIdeal‘𝑅) ∈ V
11	10	rabex 5309	. . . . . . . . . . . 12 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ∈ V
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ∈ V)
13	4, 7, 9, 12	fvmptd 6997	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
14		ssrab2 4034	. . . . . . . . . . 11 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ⊆ (PrmIdeal‘𝑅)
15	14	a1i 11	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ⊆ (PrmIdeal‘𝑅))
16	13, 15	eqsstrd 3971	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) ⊆ (PrmIdeal‘𝑅))
17	16	sseld 3936	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → (𝑝 ∈ (𝑉‘𝑙) → 𝑝 ∈ (PrmIdeal‘𝑅)))
18	17	ralimdva 3177	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅)))
19		eliin 4961	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) ↔ ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙)))
20	19	elv 3460	. . . . . . . 8 ⊢ (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) ↔ ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
21	20	biimpi 219	. . . . . . 7 ⊢ (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
22	18, 21	impel 514	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅))
23		rspn0 4311	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → (∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅) → 𝑝 ∈ (PrmIdeal‘𝑅)))
24	23	imp 411	. . . . . 6 ⊢ ((𝑇 ≠ ∅ ∧ ∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅)) → 𝑝 ∈ (PrmIdeal‘𝑅))
25	2, 22, 24	syl2anc 595	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ (PrmIdeal‘𝑅))
26		simp1 1154	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑅 ∈ Ring)
27	26	adantr 485	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑅 ∈ Ring)
28		prmidlidl 21469	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑝 ∈ (PrmIdeal‘𝑅)) → 𝑝 ∈ (LIdeal‘𝑅))
29	27, 25, 28	syl2anc 595	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ (LIdeal‘𝑅))
30		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑙(𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅)
31		nfcv 2925	. . . . . . . . . 10 ⊢ Ⅎ𝑙𝑝
32		nfii1 4993	. . . . . . . . . 10 ⊢ Ⅎ𝑙∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)
33	31, 32	nfel 2939	. . . . . . . . 9 ⊢ Ⅎ𝑙 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)
34	30, 33	nfan 1929	. . . . . . . 8 ⊢ Ⅎ𝑙((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙))
35	20	bilani 509	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
36	35	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
37		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → 𝑙 ∈ 𝑇)
38		rspa 3254	. . . . . . . . . . . . 13 ⊢ ((∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (𝑉‘𝑙))
39	36, 37, 38	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (𝑉‘𝑙))
40	13	adantlr 727	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
41	39, 40	eleqtrd 2865	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
42		sseq2 3963	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑝 → (𝑙 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑝))
43	42	elrab 3650	. . . . . . . . . . 11 ⊢ (𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ↔ (𝑝 ∈ (PrmIdeal‘𝑅) ∧ 𝑙 ⊆ 𝑝))
44	41, 43	sylib 221	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → (𝑝 ∈ (PrmIdeal‘𝑅) ∧ 𝑙 ⊆ 𝑝))
45	44	simprd 500	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ 𝑝)
46	45	ex 417	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → (𝑙 ∈ 𝑇 → 𝑙 ⊆ 𝑝))
47	34, 46	ralrimi 3263	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∀𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝)
48		unissb 4906	. . . . . . 7 ⊢ (∪ 𝑇 ⊆ 𝑝 ↔ ∀𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝)
49	47, 48	sylibr 237	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∪ 𝑇 ⊆ 𝑝)
50		zarclsiin.1	. . . . . . 7 ⊢ 𝐾 = (RSpan‘𝑅)
51		eqid 2763	. . . . . . 7 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
52	50, 51	rspssp 21368	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑝 ∈ (LIdeal‘𝑅) ∧ ∪ 𝑇 ⊆ 𝑝) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
53	27, 29, 49, 52	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
54	1, 25, 53	elrabd 3652	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
55	3	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}))
56		sseq1 3962	. . . . . . . . 9 ⊢ (𝑖 = (𝐾‘∪ 𝑇) → (𝑖 ⊆ 𝑗 ↔ (𝐾‘∪ 𝑇) ⊆ 𝑗))
57	56	rabbidv 3423	. . . . . . . 8 ⊢ (𝑖 = (𝐾‘∪ 𝑇) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
58	57	adantl 486	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑖 = (𝐾‘∪ 𝑇)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
59	8	sselda 3937	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑖 ∈ 𝑇) → 𝑖 ∈ (LIdeal‘𝑅))
60		eqid 2763	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
61	60, 51	lidlss 21336	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ (Base‘𝑅))
62	59, 61	syl 18	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑖 ∈ 𝑇) → 𝑖 ⊆ (Base‘𝑅))
63	62	ralrimiva 3157	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∀𝑖 ∈ 𝑇 𝑖 ⊆ (Base‘𝑅))
64		unissb 4906	. . . . . . . . 9 ⊢ (∪ 𝑇 ⊆ (Base‘𝑅) ↔ ∀𝑖 ∈ 𝑇 𝑖 ⊆ (Base‘𝑅))
65	63, 64	sylibr 237	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∪ 𝑇 ⊆ (Base‘𝑅))
66	50, 60, 51	rspcl 21364	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ (Base‘𝑅)) → (𝐾‘∪ 𝑇) ∈ (LIdeal‘𝑅))
67	26, 65, 66	syl2anc 595	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (𝐾‘∪ 𝑇) ∈ (LIdeal‘𝑅))
68	10	rabex 5309	. . . . . . . 8 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗} ∈ V
69	68	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗} ∈ V)
70	55, 58, 67, 69	fvmptd 6997	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (𝑉‘(𝐾‘∪ 𝑇)) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
71	70	eleq2d 2849	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇)) ↔ 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗}))
72	71	adantr 485	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → (𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇)) ↔ 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗}))
73	54, 72	mpbird 260	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇)))
74	71	biimpa 481	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
75	1	elrab 3650	. . . . . . . . . 10 ⊢ (𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗} ↔ (𝑝 ∈ (PrmIdeal‘𝑅) ∧ (𝐾‘∪ 𝑇) ⊆ 𝑝))
76	74, 75	sylib 221	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → (𝑝 ∈ (PrmIdeal‘𝑅) ∧ (𝐾‘∪ 𝑇) ⊆ 𝑝))
77	76	simpld 499	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → 𝑝 ∈ (PrmIdeal‘𝑅))
78	77	adantr 485	. . . . . . 7 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (PrmIdeal‘𝑅))
79		elssuni 4904	. . . . . . . . . 10 ⊢ (𝑙 ∈ 𝑇 → 𝑙 ⊆ ∪ 𝑇)
80	79	adantl 486	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ ∪ 𝑇)
81		simpll 778	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → (𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅))
82	50, 60	rspssid 21365	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ (Base‘𝑅)) → ∪ 𝑇 ⊆ (𝐾‘∪ 𝑇))
83	26, 65, 82	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∪ 𝑇 ⊆ (𝐾‘∪ 𝑇))
84	81, 83	syl 18	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → ∪ 𝑇 ⊆ (𝐾‘∪ 𝑇))
85	80, 84	sstrd 3947	. . . . . . . 8 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ (𝐾‘∪ 𝑇))
86	76	simprd 500	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
87	86	adantr 485	. . . . . . . 8 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
88	85, 87	sstrd 3947	. . . . . . 7 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ 𝑝)
89	42, 78, 88	elrabd 3652	. . . . . 6 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
90	8	adantr 485	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → 𝑇 ⊆ (LIdeal‘𝑅))
91	90	sselda 3937	. . . . . . 7 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ∈ (LIdeal‘𝑅))
92	3	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ (LIdeal‘𝑅)) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}))
93	6	adantl 486	. . . . . . . 8 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ (LIdeal‘𝑅)) ∧ 𝑖 = 𝑙) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
94		simpr 489	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ (LIdeal‘𝑅)) → 𝑙 ∈ (LIdeal‘𝑅))
95	11	a1i 11	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ (LIdeal‘𝑅)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ∈ V)
96	92, 93, 94, 95	fvmptd 6997	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ (LIdeal‘𝑅)) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
97	81, 91, 96	syl2anc 595	. . . . . 6 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
98	89, 97	eleqtrrd 2866	. . . . 5 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (𝑉‘𝑙))
99	98	ralrimiva 3157	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
100	20	a1i 11	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) ↔ ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙)))
101	99, 100	mpbird 260	. . 3 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙))
102	73, 101	impbida 812	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) ↔ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))))
103	102	eqrdv 2761	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) = (𝑉‘(𝐾‘∪ 𝑇)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  {crab 3416  Vcvv 3455   ⊆ wss 3905  ∅c0 4286  ∪ cuni 4872  ∩ ciin 4957   ↦ cmpt 5192  ‘cfv 6536  Basecbs 17264  Ringcrg 20310  LIdealclidl 21330  RSpancrsp 21331  PrmIdealcprmidl 21460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-sca 17321  df-vsca 17322  df-ip 17323  df-0g 17489  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-grp 18998  df-minusg 18999  df-sbg 19000  df-subg 19184  df-mgp 20212  df-ur 20259  df-ring 20312  df-subrg 20669  df-lmod 20983  df-lss 21053  df-lsp 21093  df-sra 21294  df-rgmod 21295  df-lidl 21332  df-rsp 21333  df-prmidl 21461

This theorem is referenced by:  zarclsint  34262  zarcmplem  34271