zarcmplem

	Ref	Expression
Hypotheses	zartop.1	$⊢ S = Spec (R)$
	zartop.2	$⊢ J = TopOpen (S)$
	zarcmplem.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
Assertion	zarcmplem	$⊢ R \in CRing \to J \in Comp$

Proof

Step	Hyp	Ref	Expression
1		zartop.1	$⊢ S = Spec (R)$
2		zartop.2	$⊢ J = TopOpen (S)$
3		zarcmplem.1	$⊢ V = (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\})$
4		crngring	$⊢ R \in CRing \to R \in Ring$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	1 2 5	zar0ring	$⊢ (R \in Ring \land \|{Base}_{R}\| = 1) \to J = \{\emptyset\}$
7	4 6	sylan	$⊢ (R \in CRing \land \|{Base}_{R}\| = 1) \to J = \{\emptyset\}$
8		0cmp	$⊢ \{\emptyset\} \in Comp$
9	7 8	eqeltrdi	$⊢ (R \in CRing \land \|{Base}_{R}\| = 1) \to J \in Comp$
10	1 2	zartop	$⊢ R \in CRing \to J \in Top$
11		fvex	$⊢ LIdeal (R) \in V$
12	11	mptex	$⊢ (i \in LIdeal (R) ⟼ \{j \in PrmIdeal (R) \| i \subseteq j\}) \in V$
13	3 12	eqeltri	$⊢ V \in V$
14		imaexg	$⊢ V \in V \to V [a supp 0_{R}] \in V$
15	13 14	mp1i	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [a supp 0_{R}] \in V$
16		suppssdm	$⊢ a supp 0_{R} \subseteq dom a$
17		imass2	$⊢ a supp 0_{R} \subseteq dom a \to V [a supp 0_{R}] \subseteq V [dom a]$
18	16 17	mp1i	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [a supp 0_{R}] \subseteq V [dom a]$
19	3	funmpt2	$⊢ Fun V$
20		ssidd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to dom a \subseteq dom a$
21		simpllr	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to a \in ({Base}_{R}^{V^{-1} [x]})$
22		fvexd	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to {Base}_{R} \in V$
23	13	cnvex	$⊢ V^{-1} \in V$
24	23	imaex	$⊢ V^{-1} [x] \in V$
25	24	a1i	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to V^{-1} [x] \in V$
26	22 25	elmapd	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to (a \in ({Base}_{R}^{V^{-1} [x]}) \leftrightarrow a : V^{-1} [x] ⟶ {Base}_{R})$
27	21 26	mpbid	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to a : V^{-1} [x] ⟶ {Base}_{R}$
28	27	fdmd	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to dom a = V^{-1} [x]$
29	28	adantr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to dom a = V^{-1} [x]$
30	20 29	sseqtrd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to dom a \subseteq V^{-1} [x]$
31		funimass2	$⊢ (Fun V \land dom a \subseteq V^{-1} [x]) \to V [dom a] \subseteq x$
32	19 30 31	sylancr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [dom a] \subseteq x$
33	18 32	sstrd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [a supp 0_{R}] \subseteq x$
34	15 33	elpwd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [a supp 0_{R}] \in 𝒫 x$
35		simpllr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to {finSupp}_{0_{R}} (a)$
36	35	fsuppimpd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a supp 0_{R} \in Fin$
37		imafi	$⊢ (Fun V \land a supp 0_{R} \in Fin) \to V [a supp 0_{R}] \in Fin$
38	19 36 37	sylancr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [a supp 0_{R}] \in Fin$
39	34 38	elind	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V [a supp 0_{R}] \in (𝒫 x \cap Fin)$
40		inteq	$⊢ y = V [a supp 0_{R}] \to ⋂ y = ⋂ V [a supp 0_{R}]$
41	40	eqeq2d	$⊢ y = V [a supp 0_{R}] \to (\emptyset = ⋂ y \leftrightarrow \emptyset = ⋂ V [a supp 0_{R}])$
42	41	adantl	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land y = V [a supp 0_{R}]) \to (\emptyset = ⋂ y \leftrightarrow \emptyset = ⋂ V [a supp 0_{R}])$
43	16 29	sseqtrid	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a supp 0_{R} \subseteq V^{-1} [x]$
44		cnvimass	$⊢ V^{-1} [x] \subseteq dom V$
45	43 44	sstrdi	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a supp 0_{R} \subseteq dom V$
46		intimafv	$⊢ (Fun V \land a supp 0_{R} \subseteq dom V) \to ⋂ V [a supp 0_{R}] = ⋂_{l \in a supp 0_{R}} V (l)$
47	19 45 46	sylancr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to ⋂ V [a supp 0_{R}] = ⋂_{l \in a supp 0_{R}} V (l)$
48		simplll	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to R \in CRing$
49	48	crngringd	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to R \in Ring$
50	49	ad4antr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to R \in Ring$
51		fvex	$⊢ PrmIdeal (R) \in V$
52	51	rabex	$⊢ \{j \in PrmIdeal (R) \| i \subseteq j\} \in V$
53	52 3	dmmpti	$⊢ dom V = LIdeal (R)$
54	45 53	sseqtrdi	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a supp 0_{R} \subseteq LIdeal (R)$
55		simp-7r	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \|{Base}_{R}\| \neq 1$
56		simpllr	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to 1_{R} = \sum_{R} a$
57		eqid	$⊢ 0_{R} = 0_{R}$
58		ringcmn	$⊢ R \in Ring \to R \in CMnd$
59	4 58	syl	$⊢ R \in CRing \to R \in CMnd$
60	59	ad8antr	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to R \in CMnd$
61	24	a1i	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to V^{-1} [x] \in V$
62	27	ad2antrr	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to a : V^{-1} [x] ⟶ {Base}_{R}$
63		simpr	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to a supp 0_{R} = \emptyset$
64		ssidd	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to \emptyset \subseteq \emptyset$
65	63 64	eqsstrd	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to a supp 0_{R} \subseteq \emptyset$
66	35	adantr	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to {finSupp}_{0_{R}} (a)$
67	5 57 60 61 62 65 66	gsumres	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to \sum_{R} ({a ↾}_{\emptyset}) = \sum_{R} a$
68		res0	$⊢ {a ↾}_{\emptyset} = \emptyset$
69	68	oveq2i	$⊢ \sum_{R} ({a ↾}_{\emptyset}) = \sum_{R} \emptyset$
70	57	gsum0	$⊢ \sum_{R} \emptyset = 0_{R}$
71	69 70	eqtri	$⊢ \sum_{R} ({a ↾}_{\emptyset}) = 0_{R}$
72	67 71	eqtr3di	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to \sum_{R} a = 0_{R}$
73	56 72	eqtr2d	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to 0_{R} = 1_{R}$
74		eqid	$⊢ 1_{R} = 1_{R}$
75	5 57 74	01eq0ring	$⊢ (R \in Ring \land 0_{R} = 1_{R}) \to {Base}_{R} = \{0_{R}\}$
76	50 73 75	syl2an2r	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to {Base}_{R} = \{0_{R}\}$
77	76	fveq2d	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to \|{Base}_{R}\| = \|\{0_{R}\}\|$
78		fvex	$⊢ 0_{R} \in V$
79		hashsng	$⊢ 0_{R} \in V \to \|\{0_{R}\}\| = 1$
80	78 79	ax-mp	$⊢ \|\{0_{R}\}\| = 1$
81	77 80	eqtrdi	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land a supp 0_{R} = \emptyset) \to \|{Base}_{R}\| = 1$
82	55 81	mteqand	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a supp 0_{R} \neq \emptyset$
83		eqid	$⊢ RSpan (R) = RSpan (R)$
84	3 83	zarclsiin	$⊢ (R \in Ring \land a supp 0_{R} \subseteq LIdeal (R) \land a supp 0_{R} \neq \emptyset) \to ⋂_{l \in a supp 0_{R}} V (l) = V (RSpan (R) (⋃ {supp}_{0_{R}} (a)))$
85	50 54 82 84	syl3anc	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to ⋂_{l \in a supp 0_{R}} V (l) = V (RSpan (R) (⋃ {supp}_{0_{R}} (a)))$
86		nfv	$⊢ Ⅎ l ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a)$
87		nfra1	$⊢ Ⅎ l \forall l \in V^{-1} [x] a (l) \in l$
88	86 87	nfan	$⊢ Ⅎ l (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l)$
89	54	sselda	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land l \in {supp}_{0_{R}} (a)) \to l \in LIdeal (R)$
90		eqid	$⊢ LIdeal (R) = LIdeal (R)$
91	5 90	lidlss	$⊢ l \in LIdeal (R) \to l \subseteq {Base}_{R}$
92	89 91	syl	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land l \in {supp}_{0_{R}} (a)) \to l \subseteq {Base}_{R}$
93	92	ex	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to (l \in {supp}_{0_{R}} (a) \to l \subseteq {Base}_{R})$
94	88 93	ralrimi	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \forall l \in {supp}_{0_{R}} (a) l \subseteq {Base}_{R}$
95		unissb	$⊢ ⋃ {supp}_{0_{R}} (a) \subseteq {Base}_{R} \leftrightarrow \forall l \in {supp}_{0_{R}} (a) l \subseteq {Base}_{R}$
96	94 95	sylibr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to ⋃ {supp}_{0_{R}} (a) \subseteq {Base}_{R}$
97	83 5 90	rspcl	$⊢ (R \in Ring \land ⋃ {supp}_{0_{R}} (a) \subseteq {Base}_{R}) \to RSpan (R) (⋃ {supp}_{0_{R}} (a)) \in LIdeal (R)$
98	50 96 97	syl2anc	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to RSpan (R) (⋃ {supp}_{0_{R}} (a)) \in LIdeal (R)$
99	5 90	lidlss	$⊢ RSpan (R) (⋃ {supp}_{0_{R}} (a)) \in LIdeal (R) \to RSpan (R) (⋃ {supp}_{0_{R}} (a)) \subseteq {Base}_{R}$
100	98 99	syl	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to RSpan (R) (⋃ {supp}_{0_{R}} (a)) \subseteq {Base}_{R}$
101	83 5 74	rsp1	$⊢ R \in Ring \to RSpan (R) (\{1_{R}\}) = {Base}_{R}$
102	50 101	syl	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to RSpan (R) (\{1_{R}\}) = {Base}_{R}$
103	27	adantr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a : V^{-1} [x] ⟶ {Base}_{R}$
104	103 43	fssresd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to ({a ↾}_{{supp}_{0_{R}} (a)}) : a supp 0_{R} ⟶ {Base}_{R}$
105		fvex	$⊢ {Base}_{R} \in V$
106		ovex	$⊢ a supp 0_{R} \in V$
107	105 106	elmap	$⊢ {a ↾}_{{supp}_{0_{R}} (a)} \in ({Base}_{R}^{{supp}_{0_{R}} (a)}) \leftrightarrow ({a ↾}_{{supp}_{0_{R}} (a)}) : a supp 0_{R} ⟶ {Base}_{R}$
108	104 107	sylibr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to {a ↾}_{{supp}_{0_{R}} (a)} \in ({Base}_{R}^{{supp}_{0_{R}} (a)})$
109		breq1	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to ({finSupp}_{0_{R}} (b) \leftrightarrow {finSupp}_{0_{R}} (({a ↾}_{{supp}_{0_{R}} (a)})))$
110		oveq2	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to \sum_{R} b = \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)})$
111	110	eqeq2d	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to (1_{R} = \sum_{R} b \leftrightarrow 1_{R} = \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)}))$
112		fveq1	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to b (k) = ({a ↾}_{{supp}_{0_{R}} (a)}) (k)$
113	112	eleq1d	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to (b (k) \in k \leftrightarrow ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k)$
114	113	ralbidv	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to (\forall k \in {supp}_{0_{R}} (a) b (k) \in k \leftrightarrow \forall k \in {supp}_{0_{R}} (a) ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k)$
115	109 111 114	3anbi123d	$⊢ b = {a ↾}_{{supp}_{0_{R}} (a)} \to (({finSupp}_{0_{R}} (b) \land 1_{R} = \sum_{R} b \land \forall k \in {supp}_{0_{R}} (a) b (k) \in k) \leftrightarrow ({finSupp}_{0_{R}} (({a ↾}_{{supp}_{0_{R}} (a)})) \land 1_{R} = \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)}) \land \forall k \in {supp}_{0_{R}} (a) ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k))$
116	115	adantl	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land b = {a ↾}_{{supp}_{0_{R}} (a)}) \to (({finSupp}_{0_{R}} (b) \land 1_{R} = \sum_{R} b \land \forall k \in {supp}_{0_{R}} (a) b (k) \in k) \leftrightarrow ({finSupp}_{0_{R}} (({a ↾}_{{supp}_{0_{R}} (a)})) \land 1_{R} = \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)}) \land \forall k \in {supp}_{0_{R}} (a) ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k))$
117		fvexd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to 0_{R} \in V$
118	35 117	fsuppres	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to {finSupp}_{0_{R}} (({a ↾}_{{supp}_{0_{R}} (a)}))$
119		simplr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to 1_{R} = \sum_{R} a$
120	50 58	syl	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to R \in CMnd$
121	24	a1i	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V^{-1} [x] \in V$
122		ssidd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to a supp 0_{R} \subseteq a supp 0_{R}$
123	5 57 120 121 103 122 35	gsumres	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)}) = \sum_{R} a$
124	119 123	eqtr4d	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to 1_{R} = \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)})$
125		simpr	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land k \in {supp}_{0_{R}} (a)) \to k \in {supp}_{0_{R}} (a)$
126	125	fvresd	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land k \in {supp}_{0_{R}} (a)) \to ({a ↾}_{{supp}_{0_{R}} (a)}) (k) = a (k)$
127	16 28	sseqtrid	$⊢ ((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \to a supp 0_{R} \subseteq V^{-1} [x]$
128	127	sselda	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land k \in {supp}_{0_{R}} (a)) \to k \in V^{-1} [x]$
129		fveq2	$⊢ l = k \to a (l) = a (k)$
130		id	$⊢ l = k \to l = k$
131	129 130	eleq12d	$⊢ l = k \to (a (l) \in l \leftrightarrow a (k) \in k)$
132	131	adantl	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land k \in {supp}_{0_{R}} (a)) \land l = k) \to (a (l) \in l \leftrightarrow a (k) \in k)$
133	128 132	rspcdv	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land k \in {supp}_{0_{R}} (a)) \to (\forall l \in V^{-1} [x] a (l) \in l \to a (k) \in k)$
134	133	imp	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land k \in {supp}_{0_{R}} (a)) \land \forall l \in V^{-1} [x] a (l) \in l) \to a (k) \in k$
135	134	an32s	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land k \in {supp}_{0_{R}} (a)) \to a (k) \in k$
136	126 135	eqeltrd	$⊢ ((((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \land k \in {supp}_{0_{R}} (a)) \to ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k$
137	136	ralrimiva	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \forall k \in {supp}_{0_{R}} (a) ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k$
138	118 124 137	3jca	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to ({finSupp}_{0_{R}} (({a ↾}_{{supp}_{0_{R}} (a)})) \land 1_{R} = \sum_{R} ({a ↾}_{{supp}_{0_{R}} (a)}) \land \forall k \in {supp}_{0_{R}} (a) ({a ↾}_{{supp}_{0_{R}} (a)}) (k) \in k)$
139	108 116 138	rspcedvd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \exists b \in ({Base}_{R}^{{supp}_{0_{R}} (a)}) ({finSupp}_{0_{R}} (b) \land 1_{R} = \sum_{R} b \land \forall k \in {supp}_{0_{R}} (a) b (k) \in k)$
140		eqid	$⊢ \cdot_{R} = \cdot_{R}$
141	83 5 57 140 50 54	elrspunidl	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to (1_{R} \in RSpan (R) (⋃ {supp}_{0_{R}} (a)) \leftrightarrow \exists b \in ({Base}_{R}^{{supp}_{0_{R}} (a)}) ({finSupp}_{0_{R}} (b) \land 1_{R} = \sum_{R} b \land \forall k \in {supp}_{0_{R}} (a) b (k) \in k))$
142	139 141	mpbird	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to 1_{R} \in RSpan (R) (⋃ {supp}_{0_{R}} (a))$
143	142	snssd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \{1_{R}\} \subseteq RSpan (R) (⋃ {supp}_{0_{R}} (a))$
144	83 90	rspssp	$⊢ (R \in Ring \land RSpan (R) (⋃ {supp}_{0_{R}} (a)) \in LIdeal (R) \land \{1_{R}\} \subseteq RSpan (R) (⋃ {supp}_{0_{R}} (a))) \to RSpan (R) (\{1_{R}\}) \subseteq RSpan (R) (⋃ {supp}_{0_{R}} (a))$
145	50 98 143 144	syl3anc	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to RSpan (R) (\{1_{R}\}) \subseteq RSpan (R) (⋃ {supp}_{0_{R}} (a))$
146	102 145	eqsstrrd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to {Base}_{R} \subseteq RSpan (R) (⋃ {supp}_{0_{R}} (a))$
147	100 146	eqssd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to RSpan (R) (⋃ {supp}_{0_{R}} (a)) = {Base}_{R}$
148	147	fveq2d	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V (RSpan (R) (⋃ {supp}_{0_{R}} (a))) = V ({Base}_{R})$
149	90 5	lidl1	$⊢ R \in Ring \to {Base}_{R} \in LIdeal (R)$
150	4 149	syl	$⊢ R \in CRing \to {Base}_{R} \in LIdeal (R)$
151	3 5	zarcls1	$⊢ (R \in CRing \land {Base}_{R} \in LIdeal (R)) \to (V ({Base}_{R}) = \emptyset \leftrightarrow {Base}_{R} = {Base}_{R})$
152	150 151	mpdan	$⊢ R \in CRing \to (V ({Base}_{R}) = \emptyset \leftrightarrow {Base}_{R} = {Base}_{R})$
153	5 152	mpbiri	$⊢ R \in CRing \to V ({Base}_{R}) = \emptyset$
154	153	ad7antr	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V ({Base}_{R}) = \emptyset$
155	148 154	eqtrd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to V (RSpan (R) (⋃ {supp}_{0_{R}} (a))) = \emptyset$
156	47 85 155	3eqtrrd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \emptyset = ⋂ V [a supp 0_{R}]$
157	39 42 156	rspcedvd	$⊢ (((((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land {finSupp}_{0_{R}} (a)) \land 1_{R} = \sum_{R} a) \land \forall l \in V^{-1} [x] a (l) \in l) \to \exists y \in (𝒫 x \cap Fin) \emptyset = ⋂ y$
158	157	exp41	$⊢ ((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \to ({finSupp}_{0_{R}} (a) \to (1_{R} = \sum_{R} a \to (\forall l \in V^{-1} [x] a (l) \in l \to \exists y \in (𝒫 x \cap Fin) \emptyset = ⋂ y)))$
159	158	3imp2	$⊢ (((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land a \in ({Base}_{R}^{V^{-1} [x]})) \land ({finSupp}_{0_{R}} (a) \land 1_{R} = \sum_{R} a \land \forall l \in V^{-1} [x] a (l) \in l)) \to \exists y \in (𝒫 x \cap Fin) \emptyset = ⋂ y$
160	5 74	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
161	49 160	syl	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to 1_{R} \in {Base}_{R}$
162		simplr	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to x \in 𝒫 Clsd (J)$
163		eqid	$⊢ PrmIdeal (R) = PrmIdeal (R)$
164	1 2 163 3	zartopn	$⊢ R \in CRing \to (J \in TopOn (PrmIdeal (R)) \land ran V = Clsd (J))$
165	164	simprd	$⊢ R \in CRing \to ran V = Clsd (J)$
166	48 165	syl	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to ran V = Clsd (J)$
167	166	pweqd	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to 𝒫 ran V = 𝒫 Clsd (J)$
168	162 167	eleqtrrd	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to x \in 𝒫 ran V$
169	168	elpwid	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to x \subseteq ran V$
170		intimafv	$⊢ (Fun V \land V^{-1} [x] \subseteq dom V) \to ⋂ V [V^{-1} [x]] = ⋂_{l \in V^{-1} [x]} V (l)$
171	19 44 170	mp2an	$⊢ ⋂ V [V^{-1} [x]] = ⋂_{l \in V^{-1} [x]} V (l)$
172		funimacnv	$⊢ Fun V \to V [V^{-1} [x]] = x \cap ran V$
173	19 172	ax-mp	$⊢ V [V^{-1} [x]] = x \cap ran V$
174		dfss2	$⊢ x \subseteq ran V \leftrightarrow x \cap ran V = x$
175	174	biimpi	$⊢ x \subseteq ran V \to x \cap ran V = x$
176	173 175	eqtrid	$⊢ x \subseteq ran V \to V [V^{-1} [x]] = x$
177	176	inteqd	$⊢ x \subseteq ran V \to ⋂ V [V^{-1} [x]] = ⋂ x$
178	171 177	eqtr3id	$⊢ x \subseteq ran V \to ⋂_{l \in V^{-1} [x]} V (l) = ⋂ x$
179	169 178	syl	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to ⋂_{l \in V^{-1} [x]} V (l) = ⋂ x$
180	44	a1i	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to V^{-1} [x] \subseteq dom V$
181	180 53	sseqtrdi	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to V^{-1} [x] \subseteq LIdeal (R)$
182	19	a1i	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to Fun V$
183		inteq	$⊢ x = \emptyset \to ⋂ x = ⋂ \emptyset$
184		int0	$⊢ ⋂ \emptyset = V$
185	183 184	eqtrdi	$⊢ x = \emptyset \to ⋂ x = V$
186		vn0	$⊢ V \neq \emptyset$
187		neeq1	$⊢ ⋂ x = V \to (⋂ x \neq \emptyset \leftrightarrow V \neq \emptyset)$
188	186 187	mpbiri	$⊢ ⋂ x = V \to ⋂ x \neq \emptyset$
189	185 188	syl	$⊢ x = \emptyset \to ⋂ x \neq \emptyset$
190	189	necon2i	$⊢ ⋂ x = \emptyset \to x \neq \emptyset$
191	190	adantl	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to x \neq \emptyset$
192		preiman0	$⊢ (Fun V \land x \subseteq ran V \land x \neq \emptyset) \to V^{-1} [x] \neq \emptyset$
193	182 169 191 192	syl3anc	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to V^{-1} [x] \neq \emptyset$
194	3 83	zarclsiin	$⊢ (R \in Ring \land V^{-1} [x] \subseteq LIdeal (R) \land V^{-1} [x] \neq \emptyset) \to ⋂_{l \in V^{-1} [x]} V (l) = V (RSpan (R) (⋃ V^{-1} [x]))$
195	49 181 193 194	syl3anc	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to ⋂_{l \in V^{-1} [x]} V (l) = V (RSpan (R) (⋃ V^{-1} [x]))$
196		simpr	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to ⋂ x = \emptyset$
197	179 195 196	3eqtr3d	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to V (RSpan (R) (⋃ V^{-1} [x])) = \emptyset$
198	181	sselda	$⊢ ((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land l \in V^{-1} [x]) \to l \in LIdeal (R)$
199	198 91	syl	$⊢ ((((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \land l \in V^{-1} [x]) \to l \subseteq {Base}_{R}$
200	199	ralrimiva	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to \forall l \in V^{-1} [x] l \subseteq {Base}_{R}$
201		unissb	$⊢ ⋃ V^{-1} [x] \subseteq {Base}_{R} \leftrightarrow \forall l \in V^{-1} [x] l \subseteq {Base}_{R}$
202	200 201	sylibr	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to ⋃ V^{-1} [x] \subseteq {Base}_{R}$
203	83 5 90	rspcl	$⊢ (R \in Ring \land ⋃ V^{-1} [x] \subseteq {Base}_{R}) \to RSpan (R) (⋃ V^{-1} [x]) \in LIdeal (R)$
204	49 202 203	syl2anc	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to RSpan (R) (⋃ V^{-1} [x]) \in LIdeal (R)$
205	3 5	zarcls1	$⊢ (R \in CRing \land RSpan (R) (⋃ V^{-1} [x]) \in LIdeal (R)) \to (V (RSpan (R) (⋃ V^{-1} [x])) = \emptyset \leftrightarrow RSpan (R) (⋃ V^{-1} [x]) = {Base}_{R})$
206	48 204 205	syl2anc	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to (V (RSpan (R) (⋃ V^{-1} [x])) = \emptyset \leftrightarrow RSpan (R) (⋃ V^{-1} [x]) = {Base}_{R})$
207	197 206	mpbid	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to RSpan (R) (⋃ V^{-1} [x]) = {Base}_{R}$
208	161 207	eleqtrrd	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to 1_{R} \in RSpan (R) (⋃ V^{-1} [x])$
209	83 5 57 140 49 181	elrspunidl	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to (1_{R} \in RSpan (R) (⋃ V^{-1} [x]) \leftrightarrow \exists a \in ({Base}_{R}^{V^{-1} [x]}) ({finSupp}_{0_{R}} (a) \land 1_{R} = \sum_{R} a \land \forall l \in V^{-1} [x] a (l) \in l))$
210	208 209	mpbid	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to \exists a \in ({Base}_{R}^{V^{-1} [x]}) ({finSupp}_{0_{R}} (a) \land 1_{R} = \sum_{R} a \land \forall l \in V^{-1} [x] a (l) \in l)$
211	159 210	r19.29a	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to \exists y \in (𝒫 x \cap Fin) \emptyset = ⋂ y$
212		0ex	$⊢ \emptyset \in V$
213		vex	$⊢ x \in V$
214		elfi	$⊢ (\emptyset \in V \land x \in V) \to (\emptyset \in fi (x) \leftrightarrow \exists y \in (𝒫 x \cap Fin) \emptyset = ⋂ y)$
215	212 213 214	mp2an	$⊢ \emptyset \in fi (x) \leftrightarrow \exists y \in (𝒫 x \cap Fin) \emptyset = ⋂ y$
216	211 215	sylibr	$⊢ (((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \land ⋂ x = \emptyset) \to \emptyset \in fi (x)$
217	216	ex	$⊢ ((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \to (⋂ x = \emptyset \to \emptyset \in fi (x))$
218	217	necon3bd	$⊢ ((R \in CRing \land \|{Base}_{R}\| \neq 1) \land x \in 𝒫 Clsd (J)) \to (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset)$
219	218	ralrimiva	$⊢ (R \in CRing \land \|{Base}_{R}\| \neq 1) \to \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset)$
220		cmpfi	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$
221	220	biimpar	$⊢ (J \in Top \land \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset)) \to J \in Comp$
222	10 219 221	syl2an2r	$⊢ (R \in CRing \land \|{Base}_{R}\| \neq 1) \to J \in Comp$
223	9 222	pm2.61dane	$⊢ R \in CRing \to J \in Comp$

Metamath Proof Explorer

Theorem zarcmplem

Proof