zarclsun

Description: The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024)

		Ref	Expression
	Hypothesis	zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
	Assertion	zarclsun	$⊢ (R \in CRing \land X \in ran V \land Y \in ran V) \to X \cup Y \in ran V$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
2		simpllr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \land Y = \{j \in PrmIdeal (R) \| k \subseteq j\}) \to X = \{j \in PrmIdeal (R) \| l \subseteq j\}$
3		simpr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \land Y = \{j \in PrmIdeal (R) \| k \subseteq j\}) \to Y = \{j \in PrmIdeal (R) \| k \subseteq j\}$
4	2 3	uneq12d	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \land Y = \{j \in PrmIdeal (R) \| k \subseteq j\}) \to X \cup Y = \{j \in PrmIdeal (R) \| l \subseteq j\} \cup \{j \in PrmIdeal (R) \| k \subseteq j\}$
5		unrab	$⊢ \{j \in PrmIdeal (R) \| l \subseteq j\} \cup \{j \in PrmIdeal (R) \| k \subseteq j\} = \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\}$
6		eqid	$⊢ IDLsrg (R) = IDLsrg (R)$
7		eqid	$⊢ LIdeal (R) = LIdeal (R)$
8		eqid	$⊢ \cdot_{IDLsrg (R)} = \cdot_{IDLsrg (R)}$
9		simpll	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to R \in CRing$
10	9	crngringd	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to R \in Ring$
11		simplr	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to l \in LIdeal (R)$
12		simpr	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to k \in LIdeal (R)$
13	6 7 8 10 11 12	idlsrgmulrcl	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to l \cdot_{IDLsrg (R)} k \in LIdeal (R)$
14		sseq1	$⊢ i = l \cdot_{IDLsrg (R)} k \to (i \subseteq j \leftrightarrow l \cdot_{IDLsrg (R)} k \subseteq j)$
15	14	rabbidv	$⊢ i = l \cdot_{IDLsrg (R)} k \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| l \cdot_{IDLsrg (R)} k \subseteq j\}$
16	15	eqeq2d	$⊢ i = l \cdot_{IDLsrg (R)} k \to (\{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} = \{j \in PrmIdeal (R) \| l \cdot_{IDLsrg (R)} k \subseteq j\})$
17	16	adantl	$⊢ (((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land i = l \cdot_{IDLsrg (R)} k) \to (\{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} = \{j \in PrmIdeal (R) \| l \cdot_{IDLsrg (R)} k \subseteq j\})$
18		eqid	$⊢ \cdot_{R} = \cdot_{R}$
19	9	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \subseteq j) \to R \in CRing$
20	11	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \subseteq j) \to l \in LIdeal (R)$
21	12	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \subseteq j) \to k \in LIdeal (R)$
22	6 7 8 18 19 20 21	idlsrgmulrss1	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \subseteq j) \to l \cdot_{IDLsrg (R)} k \subseteq l$
23		simpr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \subseteq j) \to l \subseteq j$
24	22 23	sstrd	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \subseteq j) \to l \cdot_{IDLsrg (R)} k \subseteq j$
25	10	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land k \subseteq j) \to R \in Ring$
26	11	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land k \subseteq j) \to l \in LIdeal (R)$
27	12	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land k \subseteq j) \to k \in LIdeal (R)$
28	6 7 8 18 25 26 27	idlsrgmulrss2	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land k \subseteq j) \to l \cdot_{IDLsrg (R)} k \subseteq k$
29		simpr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land k \subseteq j) \to k \subseteq j$
30	28 29	sstrd	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land k \subseteq j) \to l \cdot_{IDLsrg (R)} k \subseteq j$
31	24 30	jaodan	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land (l \subseteq j \lor k \subseteq j)) \to l \cdot_{IDLsrg (R)} k \subseteq j$
32		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
33	10	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to R \in Ring$
34		simplr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to j \in PrmIdeal (R)$
35	11	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l \in LIdeal (R)$
36	12	ad2antrr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to k \in LIdeal (R)$
37		eqid	$⊢ {Base}_{R} = {Base}_{R}$
38		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
39	37 7	lidlss	$⊢ l \in LIdeal (R) \to l \subseteq {Base}_{R}$
40	35 39	syl	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l \subseteq {Base}_{R}$
41	37 7	lidlss	$⊢ k \in LIdeal (R) \to k \subseteq {Base}_{R}$
42	36 41	syl	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to k \subseteq {Base}_{R}$
43	37 38 32 33 40 42	ringlsmss	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l LSSum ({mulGrp}_{R}) k \subseteq {Base}_{R}$
44		eqid	$⊢ RSpan (R) = RSpan (R)$
45	44 37	rspssid	$⊢ (R \in Ring \land l LSSum ({mulGrp}_{R}) k \subseteq {Base}_{R}) \to l LSSum ({mulGrp}_{R}) k \subseteq RSpan (R) (l LSSum ({mulGrp}_{R}) k)$
46	33 43 45	syl2anc	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l LSSum ({mulGrp}_{R}) k \subseteq RSpan (R) (l LSSum ({mulGrp}_{R}) k)$
47	6 7 8 38 32 33 35 36	idlsrgmulrval	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l \cdot_{IDLsrg (R)} k = RSpan (R) (l LSSum ({mulGrp}_{R}) k)$
48	46 47	sseqtrrd	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l LSSum ({mulGrp}_{R}) k \subseteq l \cdot_{IDLsrg (R)} k$
49		simpr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l \cdot_{IDLsrg (R)} k \subseteq j$
50	48 49	sstrd	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to l LSSum ({mulGrp}_{R}) k \subseteq j$
51	32 33 34 35 36 50	idlmulssprm	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \land l \cdot_{IDLsrg (R)} k \subseteq j) \to (l \subseteq j \lor k \subseteq j)$
52	31 51	impbida	$⊢ (((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \land j \in PrmIdeal (R)) \to ((l \subseteq j \lor k \subseteq j) \leftrightarrow l \cdot_{IDLsrg (R)} k \subseteq j)$
53	52	rabbidva	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} = \{j \in PrmIdeal (R) \| l \cdot_{IDLsrg (R)} k \subseteq j\}$
54	13 17 53	rspcedvd	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to \exists i \in LIdeal (R) \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} = \{j \in PrmIdeal (R) \| i \subseteq j\}$
55		fvex	$⊢ PrmIdeal (R) \in V$
56	55	rabex	$⊢ \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} \in V$
57	56	a1i	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} \in V$
58	1 54 57	elrnmptd	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to \{j \in PrmIdeal (R) \| (l \subseteq j \lor k \subseteq j)\} \in ran V$
59	5 58	eqeltrid	$⊢ ((R \in CRing \land l \in LIdeal (R)) \land k \in LIdeal (R)) \to \{j \in PrmIdeal (R) \| l \subseteq j\} \cup \{j \in PrmIdeal (R) \| k \subseteq j\} \in ran V$
60	59	adantlr	$⊢ (((R \in CRing \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \to \{j \in PrmIdeal (R) \| l \subseteq j\} \cup \{j \in PrmIdeal (R) \| k \subseteq j\} \in ran V$
61	60	adantr	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \land Y = \{j \in PrmIdeal (R) \| k \subseteq j\}) \to \{j \in PrmIdeal (R) \| l \subseteq j\} \cup \{j \in PrmIdeal (R) \| k \subseteq j\} \in ran V$
62	4 61	eqeltrd	$⊢ ((((R \in CRing \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \land Y = \{j \in PrmIdeal (R) \| k \subseteq j\}) \to X \cup Y \in ran V$
63	62	adantl4r	$⊢ (((((R \in CRing \land Y \in ran V) \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \land k \in LIdeal (R)) \land Y = \{j \in PrmIdeal (R) \| k \subseteq j\}) \to X \cup Y \in ran V$
64	55	rabex	$⊢ \{j \in PrmIdeal (R) \| i \subseteq j\} \in V$
65	1 64	elrnmpti	$⊢ Y \in ran V \leftrightarrow \exists i \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| i \subseteq j\}$
66		sseq1	$⊢ i = k \to (i \subseteq j \leftrightarrow k \subseteq j)$
67	66	rabbidv	$⊢ i = k \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| k \subseteq j\}$
68	67	eqeq2d	$⊢ i = k \to (Y = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow Y = \{j \in PrmIdeal (R) \| k \subseteq j\})$
69	68	cbvrexvw	$⊢ \exists i \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow \exists k \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| k \subseteq j\}$
70		biid	$⊢ \exists k \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| k \subseteq j\} \leftrightarrow \exists k \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| k \subseteq j\}$
71	65 69 70	3bitri	$⊢ Y \in ran V \leftrightarrow \exists k \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| k \subseteq j\}$
72	71	biimpi	$⊢ Y \in ran V \to \exists k \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| k \subseteq j\}$
73	72	ad3antlr	$⊢ (((R \in CRing \land Y \in ran V) \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \to \exists k \in LIdeal (R) Y = \{j \in PrmIdeal (R) \| k \subseteq j\}$
74	63 73	r19.29a	$⊢ (((R \in CRing \land Y \in ran V) \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \to X \cup Y \in ran V$
75	74	adantl3r	$⊢ ((((R \in CRing \land X \in ran V) \land Y \in ran V) \land l \in LIdeal (R)) \land X = \{j \in PrmIdeal (R) \| l \subseteq j\}) \to X \cup Y \in ran V$
76	1 64	elrnmpti	$⊢ X \in ran V \leftrightarrow \exists i \in LIdeal (R) X = \{j \in PrmIdeal (R) \| i \subseteq j\}$
77		sseq1	$⊢ i = l \to (i \subseteq j \leftrightarrow l \subseteq j)$
78	77	rabbidv	$⊢ i = l \to \{j \in PrmIdeal (R) \| i \subseteq j\} = \{j \in PrmIdeal (R) \| l \subseteq j\}$
79	78	eqeq2d	$⊢ i = l \to (X = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow X = \{j \in PrmIdeal (R) \| l \subseteq j\})$
80	79	cbvrexvw	$⊢ \exists i \in LIdeal (R) X = \{j \in PrmIdeal (R) \| i \subseteq j\} \leftrightarrow \exists l \in LIdeal (R) X = \{j \in PrmIdeal (R) \| l \subseteq j\}$
81		biid	$⊢ \exists l \in LIdeal (R) X = \{j \in PrmIdeal (R) \| l \subseteq j\} \leftrightarrow \exists l \in LIdeal (R) X = \{j \in PrmIdeal (R) \| l \subseteq j\}$
82	76 80 81	3bitri	$⊢ X \in ran V \leftrightarrow \exists l \in LIdeal (R) X = \{j \in PrmIdeal (R) \| l \subseteq j\}$
83	82	biimpi	$⊢ X \in ran V \to \exists l \in LIdeal (R) X = \{j \in PrmIdeal (R) \| l \subseteq j\}$
84	83	ad2antlr	$⊢ ((R \in CRing \land X \in ran V) \land Y \in ran V) \to \exists l \in LIdeal (R) X = \{j \in PrmIdeal (R) \| l \subseteq j\}$
85	75 84	r19.29a	$⊢ ((R \in CRing \land X \in ran V) \land Y \in ran V) \to X \cup Y \in ran V$
86	85	3impa	$⊢ (R \in CRing \land X \in ran V \land Y \in ran V) \to X \cup Y \in ran V$

Metamath Proof Explorer

Theorem zarclsun

Proof