zarclsiin

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)

	Ref	Expression
Hypotheses	zarclsx.1	No typesetting found for \|- V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) with typecode \|-
	zarclsiin.1	$⊢ K = RSpan (R)$
Assertion	zarclsiin	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋂_{l \in T} V (l) = V (K (⋃ T))$

Proof

Step	Hyp	Ref	Expression
1		zarclsx.1	Could not format V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) : No typesetting found for \|- V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) with typecode \|-
2		zarclsiin.1	$⊢ K = RSpan (R)$
3		sseq2	$⊢ j = p \to (K (⋃ T) \subseteq j \leftrightarrow K (⋃ T) \subseteq p)$
4		simpl3	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to T \neq \emptyset$
5	1	a1i	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
6		sseq1	$⊢ i = l \to (i \subseteq j \leftrightarrow l \subseteq j)$
7	6	rabbidv	Could not format ( i = l -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( i = l -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
8	7	adantl	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) /\ i = l ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) /\ i = l ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
9		simp2	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to T \subseteq LIdeal (R)$
10	9	sselda	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in T) \to l \in LIdeal (R)$
11		fvex	Could not format ( PrmIdeal ` R ) e. _V : No typesetting found for \|- ( PrmIdeal ` R ) e. _V with typecode \|-
12	11	rabex	Could not format { j e. ( PrmIdeal ` R ) \| l C_ j } e. _V : No typesetting found for \|- { j e. ( PrmIdeal ` R ) \| l C_ j } e. _V with typecode \|-
13	12	a1i	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> { j e. ( PrmIdeal ` R ) \| l C_ j } e. _V ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> { j e. ( PrmIdeal ` R ) \| l C_ j } e. _V ) with typecode \|-
14	5 8 10 13	fvmptd	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
15		ssrab2	Could not format { j e. ( PrmIdeal ` R ) \| l C_ j } C_ ( PrmIdeal ` R ) : No typesetting found for \|- { j e. ( PrmIdeal ` R ) \| l C_ j } C_ ( PrmIdeal ` R ) with typecode \|-
16	15	a1i	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> { j e. ( PrmIdeal ` R ) \| l C_ j } C_ ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> { j e. ( PrmIdeal ` R ) \| l C_ j } C_ ( PrmIdeal ` R ) ) with typecode \|-
17	14 16	eqsstrd	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( V ` l ) C_ ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( V ` l ) C_ ( PrmIdeal ` R ) ) with typecode \|-
18	17	sseld	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( p e. ( V ` l ) -> p e. ( PrmIdeal ` R ) ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. T ) -> ( p e. ( V ` l ) -> p e. ( PrmIdeal ` R ) ) ) with typecode \|-
19	18	ralimdva	Could not format ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( A. l e. T p e. ( V ` l ) -> A. l e. T p e. ( PrmIdeal ` R ) ) ) : No typesetting found for \|- ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( A. l e. T p e. ( V ` l ) -> A. l e. T p e. ( PrmIdeal ` R ) ) ) with typecode \|-
20		eliin	$⊢ p \in V \to (p \in ⋂_{l \in T} V (l) \leftrightarrow \forall l \in T p \in V (l))$
21	20	elv	$⊢ p \in ⋂_{l \in T} V (l) \leftrightarrow \forall l \in T p \in V (l)$
22	21	biimpi	$⊢ p \in ⋂_{l \in T} V (l) \to \forall l \in T p \in V (l)$
23	19 22	impel	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> A. l e. T p e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> A. l e. T p e. ( PrmIdeal ` R ) ) with typecode \|-
24		rspn0	Could not format ( T =/= (/) -> ( A. l e. T p e. ( PrmIdeal ` R ) -> p e. ( PrmIdeal ` R ) ) ) : No typesetting found for \|- ( T =/= (/) -> ( A. l e. T p e. ( PrmIdeal ` R ) -> p e. ( PrmIdeal ` R ) ) ) with typecode \|-
25	24	imp	Could not format ( ( T =/= (/) /\ A. l e. T p e. ( PrmIdeal ` R ) ) -> p e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( T =/= (/) /\ A. l e. T p e. ( PrmIdeal ` R ) ) -> p e. ( PrmIdeal ` R ) ) with typecode \|-
26	4 23 25	syl2anc	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> p e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> p e. ( PrmIdeal ` R ) ) with typecode \|-
27		simp1	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to R \in Ring$
28	27	adantr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to R \in Ring$
29		prmidlidl	Could not format ( ( R e. Ring /\ p e. ( PrmIdeal ` R ) ) -> p e. ( LIdeal ` R ) ) : No typesetting found for \|- ( ( R e. Ring /\ p e. ( PrmIdeal ` R ) ) -> p e. ( LIdeal ` R ) ) with typecode \|-
30	28 26 29	syl2anc	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to p \in LIdeal (R)$
31		nfv	$⊢ Ⅎ l (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset)$
32		nfcv	$⊢ \underline{Ⅎ} l p$
33		nfii1	$⊢ \underline{Ⅎ} l ⋂_{l \in T} V (l)$
34	32 33	nfel	$⊢ Ⅎ l p \in ⋂_{l \in T} V (l)$
35	31 34	nfan	$⊢ Ⅎ l ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l))$
36	22	a1i	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to (p \in ⋂_{l \in T} V (l) \to \forall l \in T p \in V (l))$
37	36	imp	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to \forall l \in T p \in V (l)$
38	37	adantr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to \forall l \in T p \in V (l)$
39		simpr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to l \in T$
40		rspa	$⊢ (\forall l \in T p \in V (l) \land l \in T) \to p \in V (l)$
41	38 39 40	syl2anc	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to p \in V (l)$
42	14	adantlr	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
43	41 42	eleqtrd	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) /\ l e. T ) -> p e. { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) /\ l e. T ) -> p e. { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
44		sseq2	$⊢ j = p \to (l \subseteq j \leftrightarrow l \subseteq p)$
45	44	elrab	Could not format ( p e. { j e. ( PrmIdeal ` R ) \| l C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) ) : No typesetting found for \|- ( p e. { j e. ( PrmIdeal ` R ) \| l C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) ) with typecode \|-
46	43 45	sylib	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) /\ l e. T ) -> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) /\ l e. T ) -> ( p e. ( PrmIdeal ` R ) /\ l C_ p ) ) with typecode \|-
47	46	simprd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \land l \in T) \to l \subseteq p$
48	47	ex	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to (l \in T \to l \subseteq p)$
49	35 48	ralrimi	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to \forall l \in T l \subseteq p$
50		unissb	$⊢ ⋃ T \subseteq p \leftrightarrow \forall l \in T l \subseteq p$
51	49 50	sylibr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to ⋃ T \subseteq p$
52		eqid	$⊢ LIdeal (R) = LIdeal (R)$
53	2 52	rspssp	$⊢ (R \in Ring \land p \in LIdeal (R) \land ⋃ T \subseteq p) \to K (⋃ T) \subseteq p$
54	28 30 51 53	syl3anc	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to K (⋃ T) \subseteq p$
55	3 26 54	elrabd	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) with typecode \|-
56	1	a1i	Could not format ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
57		sseq1	$⊢ i = K (⋃ T) \to (i \subseteq j \leftrightarrow K (⋃ T) \subseteq j)$
58	57	rabbidv	Could not format ( i = ( K ` U. T ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) : No typesetting found for \|- ( i = ( K ` U. T ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) with typecode \|-
59	58	adantl	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i = ( K ` U. T ) ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ i = ( K ` U. T ) ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) with typecode \|-
60	9	sselda	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i \in T) \to i \in LIdeal (R)$
61		eqid	$⊢ {Base}_{R} = {Base}_{R}$
62	61 52	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq {Base}_{R}$
63	60 62	syl	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land i \in T) \to i \subseteq {Base}_{R}$
64	63	ralrimiva	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to \forall i \in T i \subseteq {Base}_{R}$
65		unissb	$⊢ ⋃ T \subseteq {Base}_{R} \leftrightarrow \forall i \in T i \subseteq {Base}_{R}$
66	64 65	sylibr	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋃ T \subseteq {Base}_{R}$
67	2 61 52	rspcl	$⊢ (R \in Ring \land ⋃ T \subseteq {Base}_{R}) \to K (⋃ T) \in LIdeal (R)$
68	27 66 67	syl2anc	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to K (⋃ T) \in LIdeal (R)$
69	11	rabex	Could not format { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } e. _V : No typesetting found for \|- { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } e. _V with typecode \|-
70	69	a1i	Could not format ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } e. _V ) : No typesetting found for \|- ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } e. _V ) with typecode \|-
71	56 59 68 70	fvmptd	Could not format ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( V ` ( K ` U. T ) ) = { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) : No typesetting found for \|- ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( V ` ( K ` U. T ) ) = { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) with typecode \|-
72	71	eleq2d	Could not format ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( p e. ( V ` ( K ` U. T ) ) <-> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) ) : No typesetting found for \|- ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) -> ( p e. ( V ` ( K ` U. T ) ) <-> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) ) with typecode \|-
73	72	adantr	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> ( p e. ( V ` ( K ` U. T ) ) <-> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. \|^\|_ l e. T ( V ` l ) ) -> ( p e. ( V ` ( K ` U. T ) ) <-> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) ) with typecode \|-
74	55 73	mpbird	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in ⋂_{l \in T} V (l)) \to p \in V (K (⋃ T))$
75	72	biimpa	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } ) with typecode \|-
76	3	elrab	Could not format ( p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) ) : No typesetting found for \|- ( p e. { j e. ( PrmIdeal ` R ) \| ( K ` U. T ) C_ j } <-> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) ) with typecode \|-
77	75 76	sylib	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> ( p e. ( PrmIdeal ` R ) /\ ( K ` U. T ) C_ p ) ) with typecode \|-
78	77	simpld	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) -> p e. ( PrmIdeal ` R ) ) with typecode \|-
79	78	adantr	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. ( PrmIdeal ` R ) ) with typecode \|-
80		elssuni	$⊢ l \in T \to l \subseteq ⋃ T$
81	80	adantl	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \subseteq ⋃ T$
82		simpll	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset)$
83	2 61	rspssid	$⊢ (R \in Ring \land ⋃ T \subseteq {Base}_{R}) \to ⋃ T \subseteq K (⋃ T)$
84	27 66 83	syl2anc	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋃ T \subseteq K (⋃ T)$
85	82 84	syl	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to ⋃ T \subseteq K (⋃ T)$
86	81 85	sstrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \subseteq K (⋃ T)$
87	77	simprd	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to K (⋃ T) \subseteq p$
88	87	adantr	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to K (⋃ T) \subseteq p$
89	86 88	sstrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \subseteq p$
90	44 79 89	elrabd	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> p e. { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
91	9	adantr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to T \subseteq LIdeal (R)$
92	91	sselda	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to l \in LIdeal (R)$
93	1	a1i	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> V = ( i e. ( LIdeal ` R ) \|-> { j e. ( PrmIdeal ` R ) \| i C_ j } ) ) with typecode \|-
94	7	adantl	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) /\ i = l ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) /\ i = l ) -> { j e. ( PrmIdeal ` R ) \| i C_ j } = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
95		simpr	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land l \in LIdeal (R)) \to l \in LIdeal (R)$
96	12	a1i	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) \| l C_ j } e. _V ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> { j e. ( PrmIdeal ` R ) \| l C_ j } e. _V ) with typecode \|-
97	93 94 95 96	fvmptd	Could not format ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ l e. ( LIdeal ` R ) ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
98	82 92 97	syl2anc	Could not format ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ T C_ ( LIdeal ` R ) /\ T =/= (/) ) /\ p e. ( V ` ( K ` U. T ) ) ) /\ l e. T ) -> ( V ` l ) = { j e. ( PrmIdeal ` R ) \| l C_ j } ) with typecode \|-
99	90 98	eleqtrrd	$⊢ (((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \land l \in T) \to p \in V (l)$
100	99	ralrimiva	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to \forall l \in T p \in V (l)$
101	21	a1i	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to (p \in ⋂_{l \in T} V (l) \leftrightarrow \forall l \in T p \in V (l))$
102	100 101	mpbird	$⊢ ((R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \land p \in V (K (⋃ T))) \to p \in ⋂_{l \in T} V (l)$
103	74 102	impbida	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to (p \in ⋂_{l \in T} V (l) \leftrightarrow p \in V (K (⋃ T)))$
104	103	eqrdv	$⊢ (R \in Ring \land T \subseteq LIdeal (R) \land T \neq \emptyset) \to ⋂_{l \in T} V (l) = V (K (⋃ T))$

Metamath Proof Explorer

Theorem zarclsiin

Proof