Theorem zarclsiin 34205

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 3971	. . . . 5 ⊢ (𝑗 = 𝑝 → ((𝐾‘∪ 𝑇) ⊆ 𝑗 ↔ (𝐾‘∪ 𝑇) ⊆ 𝑝))
2		simpl3 1210	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑇 ≠ ∅)
3		zarclsx.1	. . . . . . . . . . . 12 ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})
4	3	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}))
5		sseq1 3970	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑙 → (𝑖 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑗))
6	5	rabbidv 3430	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑙 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
7	6	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) ∧ 𝑖 = 𝑙) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
8		simp2 1153	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑇 ⊆ (LIdeal‘𝑅))
9	8	sselda 3945	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → 𝑙 ∈ (LIdeal‘𝑅))
10		fvex 6895	. . . . . . . . . . . . 13 ⊢ (PrmIdeal‘𝑅) ∈ V
11	10	rabex 5310	. . . . . . . . . . . 12 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ∈ V
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ∈ V)
13	4, 7, 9, 12	fvmptd 6998	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
14		ssrab2 4042	. . . . . . . . . . 11 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ⊆ (PrmIdeal‘𝑅)
15	14	a1i 11	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗} ⊆ (PrmIdeal‘𝑅))
16	13, 15	eqsstrd 3979	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) ⊆ (PrmIdeal‘𝑅))
17	16	sseld 3944	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ 𝑇) → (𝑝 ∈ (𝑉‘𝑙) → 𝑝 ∈ (PrmIdeal‘𝑅)))
18	17	ralimdva 3183	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅)))
19		eliin 4965	. . . . . . . . 9 ⊢ (𝑝 ∈ V → (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) ↔ ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙)))
20	19	elv 3468	. . . . . . . 8 ⊢ (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) ↔ ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
21	20	biimpi 219	. . . . . . 7 ⊢ (𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙))
22	18, 21	impel 514	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅))
23		rspn0 4319	. . . . . . 7 ⊢ (𝑇 ≠ ∅ → (∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅) → 𝑝 ∈ (PrmIdeal‘𝑅)))
24	23	imp 411	. . . . . 6 ⊢ ((𝑇 ≠ ∅ ∧ ∀𝑙 ∈ 𝑇 𝑝 ∈ (PrmIdeal‘𝑅)) → 𝑝 ∈ (PrmIdeal‘𝑅))
25	2, 22, 24	syl2anc 595	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ (PrmIdeal‘𝑅))
26		simp1 1152	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑅 ∈ Ring)
27	26	adantr 485	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑅 ∈ Ring)
28		prmidlidl 21439	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑝 ∈ (PrmIdeal‘𝑅)) → 𝑝 ∈ (LIdeal‘𝑅))
29	27, 25, 28	syl2anc 595	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ (LIdeal‘𝑅))
30		nfv 1941	. . . . . . . . 9 ⊢ Ⅎ𝑙(𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅)
31		nfcv 2931	. . . . . . . . . 10 ⊢ Ⅎ𝑙𝑝
32		nfii1 4997	. . . . . . . . . 10 ⊢ Ⅎ𝑙∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)
33	31, 32	nfel 2945	. . . . . . . . 9 ⊢ Ⅎ𝑙 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)
34	30, 33	nfan 1926	. . . . . . . 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 3260	. . . . . . . . . . . . 13 ⊢ ((∀𝑙 ∈ 𝑇 𝑝 ∈ (𝑉‘𝑙) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (𝑉‘𝑙))
39	36, 37, 38	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (𝑉‘𝑙))
40	13	adantlr 727	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
41	39, 40	eleqtrd 2871	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
42		sseq2 3971	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑝 → (𝑙 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑝))
43	42	elrab 3659	. . . . . . . . . . 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 3269	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∀𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝)
48		unissb 4910	. . . . . . 7 ⊢ (∪ 𝑇 ⊆ 𝑝 ↔ ∀𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝)
49	47, 48	sylibr 237	. . . . . 6 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → ∪ 𝑇 ⊆ 𝑝)
50		zarclsiin.1	. . . . . . 7 ⊢ 𝐾 = (RSpan‘𝑅)
51		eqid 2769	. . . . . . 7 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
52	50, 51	rspssp 21345	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑝 ∈ (LIdeal‘𝑅) ∧ ∪ 𝑇 ⊆ 𝑝) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
53	27, 29, 49, 52	syl3anc 1396	. . . . 5 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
54	1, 25, 53	elrabd 3661	. . . 4 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙)) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
55	3	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}))
56		sseq1 3970	. . . . . . . . 9 ⊢ (𝑖 = (𝐾‘∪ 𝑇) → (𝑖 ⊆ 𝑗 ↔ (𝐾‘∪ 𝑇) ⊆ 𝑗))
57	56	rabbidv 3430	. . . . . . . 8 ⊢ (𝑖 = (𝐾‘∪ 𝑇) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
58	57	adantl 486	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑖 = (𝐾‘∪ 𝑇)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
59	8	sselda 3945	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑖 ∈ 𝑇) → 𝑖 ∈ (LIdeal‘𝑅))
60		eqid 2769	. . . . . . . . . . . 12 ⊢ (Base‘𝑅) = (Base‘𝑅)
61	60, 51	lidlss 21313	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ (Base‘𝑅))
62	59, 61	syl 18	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑖 ∈ 𝑇) → 𝑖 ⊆ (Base‘𝑅))
63	62	ralrimiva 3163	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∀𝑖 ∈ 𝑇 𝑖 ⊆ (Base‘𝑅))
64		unissb 4910	. . . . . . . . 9 ⊢ (∪ 𝑇 ⊆ (Base‘𝑅) ↔ ∀𝑖 ∈ 𝑇 𝑖 ⊆ (Base‘𝑅))
65	63, 64	sylibr 237	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∪ 𝑇 ⊆ (Base‘𝑅))
66	50, 60, 51	rspcl 21341	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ (Base‘𝑅)) → (𝐾‘∪ 𝑇) ∈ (LIdeal‘𝑅))
67	26, 65, 66	syl2anc 595	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (𝐾‘∪ 𝑇) ∈ (LIdeal‘𝑅))
68	10	rabex 5310	. . . . . . . 8 ⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗} ∈ V
69	68	a1i 11	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗} ∈ V)
70	55, 58, 67, 69	fvmptd 6998	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → (𝑉‘(𝐾‘∪ 𝑇)) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ (𝐾‘∪ 𝑇) ⊆ 𝑗})
71	70	eleq2d 2855	. . . . 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 3659	. . . . . . . . . 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 4908	. . . . . . . . . 10 ⊢ (𝑙 ∈ 𝑇 → 𝑙 ⊆ ∪ 𝑇)
80	79	adantl 486	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ ∪ 𝑇)
81		simpll 778	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → (𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅))
82	50, 60	rspssid 21342	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ (Base‘𝑅)) → ∪ 𝑇 ⊆ (𝐾‘∪ 𝑇))
83	26, 65, 82	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∪ 𝑇 ⊆ (𝐾‘∪ 𝑇))
84	81, 83	syl 18	. . . . . . . . 9 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → ∪ 𝑇 ⊆ (𝐾‘∪ 𝑇))
85	80, 84	sstrd 3955	. . . . . . . 8 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ (𝐾‘∪ 𝑇))
86	76	simprd 500	. . . . . . . . 9 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
87	86	adantr 485	. . . . . . . 8 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → (𝐾‘∪ 𝑇) ⊆ 𝑝)
88	85, 87	sstrd 3955	. . . . . . 7 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑙 ⊆ 𝑝)
89	42, 78, 88	elrabd 3661	. . . . . 6 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
90	8	adantr 485	. . . . . . . 8 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) → 𝑇 ⊆ (LIdeal‘𝑅))
91	90	sselda 3945	. . . . . . 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 6998	. . . . . . 7 ⊢ (((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑙 ∈ (LIdeal‘𝑅)) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
97	81, 91, 96	syl2anc 595	. . . . . 6 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → (𝑉‘𝑙) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑙 ⊆ 𝑗})
98	89, 97	eleqtrrd 2872	. . . . 5 ⊢ ((((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) ∧ 𝑝 ∈ (𝑉‘(𝐾‘∪ 𝑇))) ∧ 𝑙 ∈ 𝑇) → 𝑝 ∈ (𝑉‘𝑙))
99	98	ralrimiva 3163	. . . 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 2767	1 ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) = (𝑉‘(𝐾‘∪ 𝑇)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  {crab 3423  Vcvv 3463   ⊆ wss 3913  ∅c0 4294  ∪ cuni 4876  ∩ ciin 4961   ↦ cmpt 5196  ‘cfv 6537  Basecbs 17268  Ringcrg 20314  LIdealclidl 21307  RSpancrsp 21308  PrmIdealcprmidl 21430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306  df-7 12307  df-8 12308  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-mulr 17323  df-sca 17325  df-vsca 17326  df-ip 17327  df-0g 17493  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-grp 19002  df-minusg 19003  df-sbg 19004  df-subg 19188  df-mgp 20216  df-ur 20263  df-ring 20316  df-subrg 20654  df-lmod 20960  df-lss 21030  df-lsp 21070  df-sra 21271  df-rgmod 21272  df-lidl 21309  df-rsp 21310  df-prmidl 21431

This theorem is referenced by:  zarclsint  34206  zarcmplem  34215