elrspunidl

Description: Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypotheses	elrspunidl.n	$⊢ N = RSpan (R)$
	elrspunidl.b	$⊢ B = {Base}_{R}$
	elrspunidl.1	$⊢ \underset{˙}{0} = 0_{R}$
	elrspunidl.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	elrspunidl.r	$⊢ φ \to R \in Ring$
	elrspunidl.i	$⊢ φ \to S \subseteq LIdeal (R)$
Assertion	elrspunidl	$⊢ φ \to (X \in N (⋃ S) \leftrightarrow \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k))$

Proof

Step	Hyp	Ref	Expression
1		elrspunidl.n	$⊢ N = RSpan (R)$
2		elrspunidl.b	$⊢ B = {Base}_{R}$
3		elrspunidl.1	$⊢ \underset{˙}{0} = 0_{R}$
4		elrspunidl.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		elrspunidl.r	$⊢ φ \to R \in Ring$
6		elrspunidl.i	$⊢ φ \to S \subseteq LIdeal (R)$
7	6	sselda	$⊢ (φ \land i \in S) \to i \in LIdeal (R)$
8		eqid	$⊢ LIdeal (R) = LIdeal (R)$
9	2 8	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq B$
10	7 9	syl	$⊢ (φ \land i \in S) \to i \subseteq B$
11	10	ralrimiva	$⊢ φ \to \forall i \in S i \subseteq B$
12		unissb	$⊢ ⋃ S \subseteq B \leftrightarrow \forall i \in S i \subseteq B$
13	11 12	sylibr	$⊢ φ \to ⋃ S \subseteq B$
14	1 2 3 4 5 13	elrsp	$⊢ φ \to (X \in N (⋃ S) \leftrightarrow \exists b \in (B^{⋃ S}) ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)))$
15		fvexd	$⊢ φ \to LIdeal (R) \in V$
16	15 6	ssexd	$⊢ φ \to S \in V$
17	16	uniexd	$⊢ φ \to ⋃ S \in V$
18		eluni2	$⊢ j \in ⋃ S \leftrightarrow \exists i \in S j \in i$
19	18	bilani	$⊢ (φ \land j \in ⋃ S) \to \exists i \in S j \in i$
20	19	ralrimiva	$⊢ φ \to \forall j \in ⋃ S \exists i \in S j \in i$
21		eleq2	$⊢ i = f (j) \to (j \in i \leftrightarrow j \in f (j))$
22	21	ac6	$⊢ (⋃ S \in V \land S \in V \land \forall j \in ⋃ S \exists i \in S j \in i) \to \exists f (f : ⋃ S ⟶ S \land \forall j \in ⋃ S j \in f (j))$
23	17 16 20 22	syl3anc	$⊢ φ \to \exists f (f : ⋃ S ⟶ S \land \forall j \in ⋃ S j \in f (j))$
24	23	ad3antrrr	$⊢ (((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to \exists f (f : ⋃ S ⟶ S \land \forall j \in ⋃ S j \in f (j))$
25		breq1	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to ({finSupp}_{\underset{˙}{0}} (a) \leftrightarrow {finSupp}_{\underset{˙}{0}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))))$
26		oveq2	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to \sum_{R} a = \underset{i \in S}{\sum_{R}} (\underset{j \in f^{-1} [\{i\}]}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j))$
27	26	eqeq2d	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to (X = \sum_{R} a \leftrightarrow X = \underset{i \in S}{\sum_{R}} (\underset{j \in f^{-1} [\{i\}]}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j)))$
28		fveq1	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to a (k) = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k)$
29	28	eleq1d	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to (a (k) \in k \leftrightarrow (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) \in k)$
30	29	ralbidv	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to (\forall k \in S a (k) \in k \leftrightarrow \forall k \in S (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) \in k)$
31	25 27 30	3anbi123d	$⊢ a = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to (({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))) \land X = \underset{i \in S}{\sum_{R}} (\underset{j \in f^{-1} [\{i\}]}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j)) \land \forall k \in S (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) \in k))$
32		simp-5l	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to φ$
33	32	adantr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to φ$
34		ringcmn	$⊢ R \in Ring \to R \in CMnd$
35	33 5 34	3syl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to R \in CMnd$
36		vex	$⊢ f \in V$
37	36	cnvex	$⊢ f^{-1} \in V$
38	37	imaex	$⊢ f^{-1} [\{i\}] \in V$
39	38	a1i	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to f^{-1} [\{i\}] \in V$
40	5	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to R \in Ring$
41		elmapi	$⊢ b \in (B^{⋃ S}) \to b : ⋃ S ⟶ B$
42	41	ad7antlr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to b : ⋃ S ⟶ B$
43		cnvimass	$⊢ f^{-1} [\{i\}] \subseteq dom f$
44		fdm	$⊢ f : ⋃ S ⟶ S \to dom f = ⋃ S$
45	43 44	sseqtrid	$⊢ f : ⋃ S ⟶ S \to f^{-1} [\{i\}] \subseteq ⋃ S$
46	45	ad3antlr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to f^{-1} [\{i\}] \subseteq ⋃ S$
47	46	sselda	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to l \in ⋃ S$
48	42 47	ffvelcdmd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to b (l) \in B$
49	13	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to ⋃ S \subseteq B$
50	49 47	sseldd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to l \in B$
51	2 4 40 48 50	ringcld	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land l \in f^{-1} [\{i\}]) \to b (l) \underset{˙}{\cdot} l \in B$
52		fveq2	$⊢ j = l \to b (j) = b (l)$
53		id	$⊢ j = l \to j = l$
54	52 53	oveq12d	$⊢ j = l \to b (j) \underset{˙}{\cdot} j = b (l) \underset{˙}{\cdot} l$
55	54	cbvmptv	$⊢ (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) = (l \in f^{-1} [\{i\}] ⟼ b (l) \underset{˙}{\cdot} l)$
56	51 55	fmptd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) : f^{-1} [\{i\}] ⟶ B$
57	39	mptexd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) \in V$
58	56	ffund	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to Fun (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j)$
59		simp-5r	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to {finSupp}_{\underset{˙}{0}} (b)$
60		nfv	$⊢ Ⅎ j ((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b))$
61		nfcv	$⊢ \underline{Ⅎ} j R$
62		nfcv	$⊢ \underline{Ⅎ} j Σ_{𝑔}$
63		nfmpt1	$⊢ \underline{Ⅎ} j (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
64	61 62 63	nfov	$⊢ \underline{Ⅎ} j (\underset{j \in ⋃ S}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j))$
65	64	nfeq2	$⊢ Ⅎ j X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)$
66	60 65	nfan	$⊢ Ⅎ j (((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
67		nfv	$⊢ Ⅎ j f : ⋃ S ⟶ S$
68	66 67	nfan	$⊢ Ⅎ j ((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S)$
69		nfra1	$⊢ Ⅎ j \forall j \in ⋃ S j \in f (j)$
70	68 69	nfan	$⊢ Ⅎ j (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j))$
71		nfv	$⊢ Ⅎ j i \in S$
72	70 71	nfan	$⊢ Ⅎ j ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S)$
73		nfcv	$⊢ \underline{Ⅎ} j f^{-1} [\{i\}]$
74		nfcv	$⊢ \underline{Ⅎ} j {supp}_{\underset{˙}{0}} (b)$
75	41	ad7antlr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b : ⋃ S ⟶ B$
76	75	ffnd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b Fn ⋃ S$
77	32 17	syl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to ⋃ S \in V$
78	77	ad2antrr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to ⋃ S \in V$
79	3	fvexi	$⊢ \underset{˙}{0} \in V$
80	79	a1i	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to \underset{˙}{0} \in V$
81	46	ssdifd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b) \subseteq ⋃ S ∖ {supp}_{\underset{˙}{0}} (b)$
82	81	sselda	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))$
83	76 78 80 82	fvdifsupp	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) = \underset{˙}{0}$
84	83	oveq1d	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0} \underset{˙}{\cdot} j$
85	5	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to R \in Ring$
86	13	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to ⋃ S \subseteq B$
87	82	eldifad	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in ⋃ S$
88	86 87	sseldd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in B$
89	2 4 3	ringlz	$⊢ (R \in Ring \land j \in B) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
90	85 88 89	syl2anc	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
91	84 90	eqtrd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \land j \in (f^{-1} [\{i\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0}$
92	72 73 74 91 39	suppss2f	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) supp \underset{˙}{0} \subseteq b supp \underset{˙}{0}$
93		fsuppsssupp	$⊢ (((j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) \in V \land Fun (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j)) \land ({finSupp}_{\underset{˙}{0}} (b) \land (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) supp \underset{˙}{0} \subseteq b supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j))$
94	57 58 59 92 93	syl22anc	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to {finSupp}_{\underset{˙}{0}} ((j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j))$
95	2 3 35 39 56 94	gsumcl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) \in B$
96	95	fmpttd	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) : S ⟶ B$
97	2	fvexi	$⊢ B \in V$
98	97	a1i	$⊢ φ \to B \in V$
99	98 16	elmapd	$⊢ φ \to ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \in (B^{S}) \leftrightarrow (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) : S ⟶ B)$
100	99	biimpar	$⊢ (φ \land (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) : S ⟶ B) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \in (B^{S})$
101	32 96 100	syl2anc	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \in (B^{S})$
102	32 16	syl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to S \in V$
103	102	mptexd	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \in V$
104	79	a1i	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to \underset{˙}{0} \in V$
105		funmpt	$⊢ Fun (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
106	105	a1i	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to Fun (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
107		simplr	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to f : ⋃ S ⟶ S$
108	107	ffund	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to Fun f$
109		simp-4r	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to {finSupp}_{\underset{˙}{0}} (b)$
110	109	fsuppimpd	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to b supp \underset{˙}{0} \in Fin$
111		imafi	$⊢ (Fun f \land b supp \underset{˙}{0} \in Fin) \to f [b supp \underset{˙}{0}] \in Fin$
112	108 110 111	syl2anc	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to f [b supp \underset{˙}{0}] \in Fin$
113		nfv	$⊢ Ⅎ j i \in (S ∖ f [b supp \underset{˙}{0}])$
114	70 113	nfan	$⊢ Ⅎ j ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}]))$
115		simpllr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f : ⋃ S ⟶ S$
116	115	ffund	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to Fun f$
117		snssi	$⊢ i \in (S ∖ f [b supp \underset{˙}{0}]) \to \{i\} \subseteq S ∖ f [b supp \underset{˙}{0}]$
118	117	adantl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to \{i\} \subseteq S ∖ f [b supp \underset{˙}{0}]$
119		sspreima	$⊢ (Fun f \land \{i\} \subseteq S ∖ f [b supp \underset{˙}{0}]) \to f^{-1} [\{i\}] \subseteq f^{-1} [S ∖ f [b supp \underset{˙}{0}]]$
120	116 118 119	syl2anc	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [\{i\}] \subseteq f^{-1} [S ∖ f [b supp \underset{˙}{0}]]$
121		difpreima	$⊢ Fun f \to f^{-1} [S ∖ f [b supp \underset{˙}{0}]] = f^{-1} [S] ∖ f^{-1} [f [b supp \underset{˙}{0}]]$
122	116 121	syl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [S ∖ f [b supp \underset{˙}{0}]] = f^{-1} [S] ∖ f^{-1} [f [b supp \underset{˙}{0}]]$
123	120 122	sseqtrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [\{i\}] \subseteq f^{-1} [S] ∖ f^{-1} [f [b supp \underset{˙}{0}]]$
124		suppssdm	$⊢ b supp \underset{˙}{0} \subseteq dom b$
125	41	ad6antlr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to b : ⋃ S ⟶ B$
126	124 125	fssdm	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to b supp \underset{˙}{0} \subseteq ⋃ S$
127	115	fdmd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to dom f = ⋃ S$
128	126 127	sseqtrrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to b supp \underset{˙}{0} \subseteq dom f$
129		sseqin2	$⊢ b supp \underset{˙}{0} \subseteq dom f \leftrightarrow dom f \cap {supp}_{\underset{˙}{0}} (b) = b supp \underset{˙}{0}$
130	129	biimpi	$⊢ b supp \underset{˙}{0} \subseteq dom f \to dom f \cap {supp}_{\underset{˙}{0}} (b) = b supp \underset{˙}{0}$
131		dminss	$⊢ dom f \cap {supp}_{\underset{˙}{0}} (b) \subseteq f^{-1} [f [b supp \underset{˙}{0}]]$
132	130 131	eqsstrrdi	$⊢ b supp \underset{˙}{0} \subseteq dom f \to b supp \underset{˙}{0} \subseteq f^{-1} [f [b supp \underset{˙}{0}]]$
133	128 132	syl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to b supp \underset{˙}{0} \subseteq f^{-1} [f [b supp \underset{˙}{0}]]$
134	133	sscond	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [S] ∖ f^{-1} [f [b supp \underset{˙}{0}]] \subseteq f^{-1} [S] ∖ {supp}_{\underset{˙}{0}} (b)$
135	123 134	sstrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [\{i\}] \subseteq f^{-1} [S] ∖ {supp}_{\underset{˙}{0}} (b)$
136		fimacnv	$⊢ f : ⋃ S ⟶ S \to f^{-1} [S] = ⋃ S$
137	115 136	syl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [S] = ⋃ S$
138	137	difeq1d	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [S] ∖ {supp}_{\underset{˙}{0}} (b) = ⋃ S ∖ {supp}_{\underset{˙}{0}} (b)$
139	135 138	sseqtrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [\{i\}] \subseteq ⋃ S ∖ {supp}_{\underset{˙}{0}} (b)$
140	139	sselda	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))$
141		ssidd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to b supp \underset{˙}{0} \subseteq b supp \underset{˙}{0}$
142	77	adantr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to ⋃ S \in V$
143	79	a1i	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to \underset{˙}{0} \in V$
144	125 141 142 143	suppssr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) = \underset{˙}{0}$
145	140 144	syldan	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to b (j) = \underset{˙}{0}$
146	145	oveq1d	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0} \underset{˙}{\cdot} j$
147	5	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to R \in Ring$
148	13	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to ⋃ S \subseteq B$
149	45	ad3antlr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to f^{-1} [\{i\}] \subseteq ⋃ S$
150	149	sselda	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to j \in ⋃ S$
151	148 150	sseldd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to j \in B$
152	147 151 89	syl2anc	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
153	146 152	eqtrd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \land j \in f^{-1} [\{i\}]) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0}$
154	114 153	mpteq2da	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) = (j \in f^{-1} [\{i\}] ⟼ \underset{˙}{0})$
155	154	oveq2d	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) = \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} \underset{˙}{0}$
156	5	ringcmnd	$⊢ φ \to R \in CMnd$
157	156	cmnmndd	$⊢ φ \to R \in Mnd$
158	157	ad6antr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to R \in Mnd$
159	3	gsumz	$⊢ (R \in Mnd \land f^{-1} [\{i\}] \in V) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
160	158 38 159	sylancl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
161	155 160	eqtrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in (S ∖ f [b supp \underset{˙}{0}])) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) = \underset{˙}{0}$
162	161 102	suppss2	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) supp \underset{˙}{0} \subseteq f [b supp \underset{˙}{0}]$
163	112 162	ssfid	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) supp \underset{˙}{0} \in Fin$
164	103 104 106 163	isfsuppd	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to {finSupp}_{\underset{˙}{0}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)))$
165		simpllr	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)$
166	32 156	syl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to R \in CMnd$
167	5	ad6antr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in ⋃ S) \to R \in Ring$
168	41	ad5antlr	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to b : ⋃ S ⟶ B$
169	168	ffvelcdmda	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in ⋃ S) \to b (j) \in B$
170	32 13	syl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to ⋃ S \subseteq B$
171	170	sselda	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in ⋃ S) \to j \in B$
172	2 4 167 169 171	ringcld	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in ⋃ S) \to b (j) \underset{˙}{\cdot} j \in B$
173		eqid	$⊢ (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) = (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
174	70 172 173	fmptdf	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) : ⋃ S ⟶ B$
175	77	mptexd	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) \in V$
176		funmpt	$⊢ Fun (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
177	176	a1i	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to Fun (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
178		nfcv	$⊢ \underline{Ⅎ} j ⋃ S$
179	168	adantr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to b : ⋃ S ⟶ B$
180	179	ffnd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to b Fn ⋃ S$
181	77	adantr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to ⋃ S \in V$
182	79	a1i	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to \underset{˙}{0} \in V$
183		simpr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))$
184	180 181 182 183	fvdifsupp	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) = \underset{˙}{0}$
185	184	oveq1d	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0} \underset{˙}{\cdot} j$
186	5	ad6antr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to R \in Ring$
187	170	adantr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to ⋃ S \subseteq B$
188	183	eldifad	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in ⋃ S$
189	187 188	sseldd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in B$
190	186 189 89	syl2anc	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
191	185 190	eqtrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0}$
192	70 178 74 191 77	suppss2f	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) supp \underset{˙}{0} \subseteq b supp \underset{˙}{0}$
193		fsuppsssupp	$⊢ (((j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) \in V \land Fun (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)) \land ({finSupp}_{\underset{˙}{0}} (b) \land (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) supp \underset{˙}{0} \subseteq b supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j))$
194	175 177 109 192 193	syl22anc	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to {finSupp}_{\underset{˙}{0}} ((j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j))$
195		sndisj	$⊢ \underset{i \in S}{Disj} \{i\}$
196		disjpreima	$⊢ (Fun f \land \underset{i \in S}{Disj} \{i\}) \to \underset{i \in S}{Disj} f^{-1} [\{i\}]$
197	108 195 196	sylancl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to \underset{i \in S}{Disj} f^{-1} [\{i\}]$
198		iunid	$⊢ ⋃_{i \in S} \{i\} = S$
199	198	imaeq2i	$⊢ f^{-1} [⋃_{i \in S} \{i\}] = f^{-1} [S]$
200		iunpreima	$⊢ Fun f \to f^{-1} [⋃_{i \in S} \{i\}] = ⋃_{i \in S} f^{-1} [\{i\}]$
201	108 200	syl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to f^{-1} [⋃_{i \in S} \{i\}] = ⋃_{i \in S} f^{-1} [\{i\}]$
202	136	ad2antlr	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to f^{-1} [S] = ⋃ S$
203	199 201 202	3eqtr3a	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to ⋃_{i \in S} f^{-1} [\{i\}] = ⋃ S$
204	2 3 166 77 102 174 194 197 203	gsumpart	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) = \underset{i \in S}{\sum_{R}} (\sum_{R}, ({(j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) ↾}_{f^{-1} [\{i\}]}))$
205	46	resmptd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to {(j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) ↾}_{f^{-1} [\{i\}]} = (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j)$
206	205	oveq2d	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land i \in S) \to \sum_{R} ({(j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) ↾}_{f^{-1} [\{i\}]}) = \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)$
207	206	mpteq2dva	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to (i \in S ⟼ \sum_{R} ({(j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) ↾}_{f^{-1} [\{i\}]})) = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
208	207	oveq2d	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to \underset{i \in S}{\sum_{R}} (\sum_{R}, ({(j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) ↾}_{f^{-1} [\{i\}]})) = \underset{i \in S}{\sum_{R}} (\underset{j \in f^{-1} [\{i\}]}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j))$
209	165 204 208	3eqtrd	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to X = \underset{i \in S}{\sum_{R}} (\underset{j \in f^{-1} [\{i\}]}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j))$
210		eqid	$⊢ (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) = (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
211		simpr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land i = k) \to i = k$
212	211	sneqd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land i = k) \to \{i\} = \{k\}$
213	212	imaeq2d	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land i = k) \to f^{-1} [\{i\}] = f^{-1} [\{k\}]$
214	213	mpteq1d	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land i = k) \to (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) = (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j)$
215	214	oveq2d	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land i = k) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) = \underset{j \in f^{-1} [\{k\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)$
216		simpr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to k \in S$
217		ovexd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to \underset{j \in f^{-1} [\{k\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) \in V$
218	210 215 216 217	fvmptd2	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) = \underset{j \in f^{-1} [\{k\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)$
219	156	ad6antr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to R \in CMnd$
220	37	imaex	$⊢ f^{-1} [\{k\}] \in V$
221	220	a1i	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to f^{-1} [\{k\}] \in V$
222	5	ad6antr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to R \in Ring$
223	32 6	syl	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to S \subseteq LIdeal (R)$
224	223	sselda	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to k \in LIdeal (R)$
225	8	lidlsubg	$⊢ (R \in Ring \land k \in LIdeal (R)) \to k \in SubGrp (R)$
226		subgsubm	$⊢ k \in SubGrp (R) \to k \in SubMnd (R)$
227	225 226	syl	$⊢ (R \in Ring \land k \in LIdeal (R)) \to k \in SubMnd (R)$
228	222 224 227	syl2anc	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to k \in SubMnd (R)$
229	222	adantr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to R \in Ring$
230	224	adantr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to k \in LIdeal (R)$
231	41	ad7antlr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to b : ⋃ S ⟶ B$
232		cnvimass	$⊢ f^{-1} [\{k\}] \subseteq dom f$
233	232 44	sseqtrid	$⊢ f : ⋃ S ⟶ S \to f^{-1} [\{k\}] \subseteq ⋃ S$
234	233	ad3antlr	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to f^{-1} [\{k\}] \subseteq ⋃ S$
235	234	sselda	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to l \in ⋃ S$
236	231 235	ffvelcdmd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to b (l) \in B$
237		fveq2	$⊢ j = l \to f (j) = f (l)$
238	53 237	eleq12d	$⊢ j = l \to (j \in f (j) \leftrightarrow l \in f (l))$
239		simpllr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to \forall j \in ⋃ S j \in f (j)$
240	238 239 235	rspcdva	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to l \in f (l)$
241		simp-4r	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to f : ⋃ S ⟶ S$
242	241	ffnd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to f Fn ⋃ S$
243		elpreima	$⊢ f Fn ⋃ S \to (l \in f^{-1} [\{k\}] \leftrightarrow (l \in ⋃ S \land f (l) \in \{k\}))$
244	243	biimpa	$⊢ (f Fn ⋃ S \land l \in f^{-1} [\{k\}]) \to (l \in ⋃ S \land f (l) \in \{k\})$
245		elsni	$⊢ f (l) \in \{k\} \to f (l) = k$
246	244 245	simpl2im	$⊢ (f Fn ⋃ S \land l \in f^{-1} [\{k\}]) \to f (l) = k$
247	242 246	sylancom	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to f (l) = k$
248	240 247	eleqtrd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to l \in k$
249	8 2 4 229 230 236 248	lidlmcld	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land l \in f^{-1} [\{k\}]) \to b (l) \underset{˙}{\cdot} l \in k$
250	54	cbvmptv	$⊢ (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) = (l \in f^{-1} [\{k\}] ⟼ b (l) \underset{˙}{\cdot} l)$
251	249 250	fmptd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) : f^{-1} [\{k\}] ⟶ k$
252	221	mptexd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) \in V$
253	251	ffund	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to Fun (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j)$
254		simp-5r	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to {finSupp}_{\underset{˙}{0}} (b)$
255		nfv	$⊢ Ⅎ j k \in S$
256	70 255	nfan	$⊢ Ⅎ j ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S)$
257		nfcv	$⊢ \underline{Ⅎ} j f^{-1} [\{k\}]$
258	41	ad7antlr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b : ⋃ S ⟶ B$
259	258	ffnd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b Fn ⋃ S$
260	77	ad2antrr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to ⋃ S \in V$
261	79	a1i	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to \underset{˙}{0} \in V$
262	234	ssdifd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b) \subseteq ⋃ S ∖ {supp}_{\underset{˙}{0}} (b)$
263	262	sselda	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in (⋃ S ∖ {supp}_{\underset{˙}{0}} (b))$
264	259 260 261 263	fvdifsupp	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) = \underset{˙}{0}$
265	264	oveq1d	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0} \underset{˙}{\cdot} j$
266	13	ad7antr	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to ⋃ S \subseteq B$
267	263	eldifad	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in ⋃ S$
268	266 267	sseldd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to j \in B$
269	222 268 89	syl2an2r	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
270	265 269	eqtrd	$⊢ (((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \land j \in (f^{-1} [\{k\}] ∖ {supp}_{\underset{˙}{0}} (b))) \to b (j) \underset{˙}{\cdot} j = \underset{˙}{0}$
271	256 257 74 270 221	suppss2f	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) supp \underset{˙}{0} \subseteq b supp \underset{˙}{0}$
272		fsuppsssupp	$⊢ (((j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) \in V \land Fun (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j)) \land ({finSupp}_{\underset{˙}{0}} (b) \land (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) supp \underset{˙}{0} \subseteq b supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j))$
273	252 253 254 271 272	syl22anc	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to {finSupp}_{\underset{˙}{0}} ((j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j))$
274	3 219 221 228 251 273	gsumsubmcl	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to \underset{j \in f^{-1} [\{k\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) \in k$
275	218 274	eqeltrd	$⊢ ((((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \land k \in S) \to (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) \in k$
276	275	ralrimiva	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to \forall k \in S (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) \in k$
277	164 209 276	3jca	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to ({finSupp}_{\underset{˙}{0}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))) \land X = \underset{i \in S}{\sum_{R}} (\underset{j \in f^{-1} [\{i\}]}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j)) \land \forall k \in S (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) (k) \in k)$
278	31 101 277	rspcedvdw	$⊢ (((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j)) \to \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)$
279	278	anasss	$⊢ ((((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land (f : ⋃ S ⟶ S \land \forall j \in ⋃ S j \in f (j))) \to \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)$
280	24 279	exlimddv	$⊢ (((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b)) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \to \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)$
281	280	anasss	$⊢ ((φ \land b \in (B^{⋃ S})) \land ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))) \to \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)$
282	281	r19.29an	$⊢ (φ \land \exists b \in (B^{⋃ S}) ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))) \to \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)$
283		breq1	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to ({finSupp}_{\underset{˙}{0}} (b) \leftrightarrow {finSupp}_{\underset{˙}{0}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}))))$
284		fveq1	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to b (j) = ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j)$
285	284	oveq1d	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to b (j) \underset{˙}{\cdot} j = ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j$
286	285	mpteq2dv	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) = (j \in ⋃ S ⟼ ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j)$
287	286	oveq2d	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) = \underset{j \in ⋃ S}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j)$
288	287	eqeq2d	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to (X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j) \leftrightarrow X = \underset{j \in ⋃ S}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j))$
289	283 288	anbi12d	$⊢ b = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \to (({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}))) \land X = \underset{j \in ⋃ S}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j)))$
290	97	a1i	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to B \in V$
291	17	ad4antr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ⋃ S \in V$
292	98 16	elmapd	$⊢ φ \to (a \in (B^{S}) \leftrightarrow a : S ⟶ B)$
293	292	biimpa	$⊢ (φ \land a \in (B^{S})) \to a : S ⟶ B$
294	293	ad3antrrr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to a : S ⟶ B$
295	294	ffnd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to a Fn S$
296		elssuni	$⊢ k \in S \to k \subseteq ⋃ S$
297	296	adantl	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land k \in S) \to k \subseteq ⋃ S$
298	297	sseld	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land k \in S) \to (a (k) \in k \to a (k) \in ⋃ S)$
299	298	ralimdva	$⊢ (((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \to (\forall k \in S a (k) \in k \to \forall k \in S a (k) \in ⋃ S)$
300	299	imp	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \forall k \in S a (k) \in ⋃ S$
301		fnfvrnss	$⊢ (a Fn S \land \forall k \in S a (k) \in ⋃ S) \to ran a \subseteq ⋃ S$
302	295 300 301	syl2anc	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ran a \subseteq ⋃ S$
303	302	ssdifssd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ran a ∖ \{\underset{˙}{0}\} \subseteq ⋃ S$
304		undif	$⊢ ran a ∖ \{\underset{˙}{0}\} \subseteq ⋃ S \leftrightarrow (ran a ∖ \{\underset{˙}{0}\}) \cup (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = ⋃ S$
305	303 304	sylib	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to (ran a ∖ \{\underset{˙}{0}\}) \cup (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = ⋃ S$
306	5	ad4antr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to R \in Ring$
307	306	adantr	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to R \in Ring$
308		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
309	308	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
310		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
311	310 2	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ B$
312	307 309 311	3syl	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to ℤRHom (R) : ℤ ⟶ B$
313		simp-5r	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to a \in (B^{S})$
314	79	a1i	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to \underset{˙}{0} \in V$
315		ssv	$⊢ ran a \subseteq V$
316		ssdif	$⊢ ran a \subseteq V \to ran a ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
317	315 316	ax-mp	$⊢ ran a ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
318	317	sseli	$⊢ m \in (ran a ∖ \{\underset{˙}{0}\}) \to m \in (V ∖ \{\underset{˙}{0}\})$
319	318	adantl	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to m \in (V ∖ \{\underset{˙}{0}\})$
320		simp-4r	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to {finSupp}_{\underset{˙}{0}} (a)$
321	313 314 319 320	fsuppinisegfi	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to a^{-1} [\{m\}] \in Fin$
322		hashcl	$⊢ a^{-1} [\{m\}] \in Fin \to \|a^{-1} [\{m\}]\| \in ℕ_{0}$
323	321 322	syl	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to \|a^{-1} [\{m\}]\| \in ℕ_{0}$
324	323	nn0zd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to \|a^{-1} [\{m\}]\| \in ℤ$
325	312 324	ffvelcdmd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land m \in (ran a ∖ \{\underset{˙}{0}\})) \to ℤRHom (R) (\|a^{-1} [\{m\}]\|) \in B$
326		eqid	$⊢ (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|))$
327	325 326	fmptd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) : ran a ∖ \{\underset{˙}{0}\} ⟶ B$
328	2 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
329		fconst6g	$⊢ \underset{˙}{0} \in B \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) : ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) ⟶ B$
330	306 328 329	3syl	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) : ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) ⟶ B$
331		disjdif	$⊢ (ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset$
332	331	a1i	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to (ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset$
333	327 330 332	fun2d	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) : (ran a ∖ \{\underset{˙}{0}\}) \cup (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) ⟶ B$
334	305 333	feq2dd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) : ⋃ S ⟶ B$
335	290 291 334	elmapdd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \in (B^{⋃ S})$
336	79	a1i	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \underset{˙}{0} \in V$
337	333	ffund	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to Fun ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}))$
338	294	ffund	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to Fun a$
339		simp-4r	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to a \in (B^{S})$
340		simpllr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to {finSupp}_{\underset{˙}{0}} (a)$
341		fsupprnfi	$⊢ ((Fun a \land a \in (B^{S})) \land (\underset{˙}{0} \in V \land {finSupp}_{\underset{˙}{0}} (a))) \to ran a \in Fin$
342		diffi	$⊢ ran a \in Fin \to ran a ∖ \{\underset{˙}{0}\} \in Fin$
343	341 342	syl	$⊢ ((Fun a \land a \in (B^{S})) \land (\underset{˙}{0} \in V \land {finSupp}_{\underset{˙}{0}} (a))) \to ran a ∖ \{\underset{˙}{0}\} \in Fin$
344	338 339 336 340 343	syl22anc	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ran a ∖ \{\underset{˙}{0}\} \in Fin$
345	327 344 336	fdmfifsupp	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to {finSupp}_{\underset{˙}{0}} ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)))$
346	13	ssdifssd	$⊢ φ \to ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) \subseteq B$
347	346	ad4antr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) \subseteq B$
348	290 347	ssexd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) \in V$
349	348 336	fczfsuppd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to {finSupp}_{\underset{˙}{0}} (((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}))$
350	345 349	fsuppun	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) supp \underset{˙}{0} \in Fin$
351	335 336 337 350	isfsuppd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to {finSupp}_{\underset{˙}{0}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})))$
352		fvex	$⊢ ℤRHom (R) (\|a^{-1} [\{m\}]\|) \in V$
353	352 326	fnmpti	$⊢ (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) Fn (ran a ∖ \{\underset{˙}{0}\})$
354	353	a1i	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) Fn (ran a ∖ \{\underset{˙}{0}\})$
355		fnconstg	$⊢ \underset{˙}{0} \in V \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) Fn (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))$
356	79 355	ax-mp	$⊢ ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) Fn (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))$
357	356	a1i	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) Fn (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))$
358	331	a1i	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to (ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset$
359		simpr	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to j \in (ran a ∖ \{\underset{˙}{0}\})$
360	354 357 358 359	fvun1d	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) (j)$
361		sneq	$⊢ m = j \to \{m\} = \{j\}$
362	361	imaeq2d	$⊢ m = j \to a^{-1} [\{m\}] = a^{-1} [\{j\}]$
363	362	fveq2d	$⊢ m = j \to \|a^{-1} [\{m\}]\| = \|a^{-1} [\{j\}]\|$
364	363	fveq2d	$⊢ m = j \to ℤRHom (R) (\|a^{-1} [\{m\}]\|) = ℤRHom (R) (\|a^{-1} [\{j\}]\|)$
365		fvexd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) \in V$
366	326 364 359 365	fvmptd3	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) (j) = ℤRHom (R) (\|a^{-1} [\{j\}]\|)$
367	360 366	eqtrd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) = ℤRHom (R) (\|a^{-1} [\{j\}]\|)$
368	367	oveq1d	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j = ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j$
369	368	mpteq2dva	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to (j \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j) = (j \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j)$
370	369	oveq2d	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j) = \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j)$
371	306	ringcmnd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to R \in CMnd$
372	331	a1i	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to (ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset$
373		fvun2	$⊢ ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) Fn (ran a ∖ \{\underset{˙}{0}\}) \land ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) Fn (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \land ((ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})))) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) = ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) (j)$
374	353 356 373	mp3an12	$⊢ ((ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) = ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) (j)$
375	372 374	sylancom	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) = ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) (j)$
376	79	fvconst2	$⊢ j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) (j) = \underset{˙}{0}$
377	376	adantl	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) (j) = \underset{˙}{0}$
378	375 377	eqtrd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) = \underset{˙}{0}$
379	378	oveq1d	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j = \underset{˙}{0} \underset{˙}{\cdot} j$
380	347	sselda	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to j \in B$
381	306 380 89	syl2an2r	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
382	379 381	eqtrd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j = \underset{˙}{0}$
383	306	adantr	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in ⋃ S) \to R \in Ring$
384	334	ffvelcdmda	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in ⋃ S) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \in B$
385	13	ad4antr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ⋃ S \subseteq B$
386	385	sselda	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in ⋃ S) \to j \in B$
387	2 4 383 384 386	ringcld	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in ⋃ S) \to ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j \in B$
388	2 3 371 291 382 344 387 303	gsummptres2	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \underset{j \in ⋃ S}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j) = \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j)$
389		eqid	$⊢ \cdot_{R} = \cdot_{R}$
390	2 3 389 371 294 340	gsumhashmul	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \sum_{R} a = \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (\|a^{-1} [\{j\}]\| \cdot_{R} j)$
391		simplr	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to X = \sum_{R} a$
392	306	adantr	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to R \in Ring$
393	339	adantr	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to a \in (B^{S})$
394	79	a1i	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to \underset{˙}{0} \in V$
395	317 359	sselid	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to j \in (V ∖ \{\underset{˙}{0}\})$
396		simp-4r	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to {finSupp}_{\underset{˙}{0}} (a)$
397	393 394 395 396	fsuppinisegfi	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to a^{-1} [\{j\}] \in Fin$
398		hashcl	$⊢ a^{-1} [\{j\}] \in Fin \to \|a^{-1} [\{j\}]\| \in ℕ_{0}$
399	397 398	syl	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to \|a^{-1} [\{j\}]\| \in ℕ_{0}$
400	399	nn0zd	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to \|a^{-1} [\{j\}]\| \in ℤ$
401	303 385	sstrd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ran a ∖ \{\underset{˙}{0}\} \subseteq B$
402	401	sselda	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to j \in B$
403		eqid	$⊢ 1_{R} = 1_{R}$
404	308 389 403	zrhmulg	$⊢ (R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) = \|a^{-1} [\{j\}]\| \cdot_{R} 1_{R}$
405	404	adantr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) = \|a^{-1} [\{j\}]\| \cdot_{R} 1_{R}$
406	405	oveq1d	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j = (\|a^{-1} [\{j\}]\| \cdot_{R} 1_{R}) \underset{˙}{\cdot} j$
407		simpll	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to R \in Ring$
408		simplr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to \|a^{-1} [\{j\}]\| \in ℤ$
409	2 403	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
410	409	ad2antrr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to 1_{R} \in B$
411		simpr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to j \in B$
412	2 389 4	mulgass2	$⊢ (R \in Ring \land (\|a^{-1} [\{j\}]\| \in ℤ \land 1_{R} \in B \land j \in B)) \to (\|a^{-1} [\{j\}]\| \cdot_{R} 1_{R}) \underset{˙}{\cdot} j = \|a^{-1} [\{j\}]\| \cdot_{R} (1_{R} \underset{˙}{\cdot} j)$
413	407 408 410 411 412	syl13anc	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to (\|a^{-1} [\{j\}]\| \cdot_{R} 1_{R}) \underset{˙}{\cdot} j = \|a^{-1} [\{j\}]\| \cdot_{R} (1_{R} \underset{˙}{\cdot} j)$
414	2 4 403	ringlidm	$⊢ (R \in Ring \land j \in B) \to 1_{R} \underset{˙}{\cdot} j = j$
415	407 414	sylancom	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to 1_{R} \underset{˙}{\cdot} j = j$
416	415	oveq2d	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to \|a^{-1} [\{j\}]\| \cdot_{R} (1_{R} \underset{˙}{\cdot} j) = \|a^{-1} [\{j\}]\| \cdot_{R} j$
417	406 413 416	3eqtrd	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j = \|a^{-1} [\{j\}]\| \cdot_{R} j$
418	392 400 402 417	syl21anc	$⊢ (((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \land j \in (ran a ∖ \{\underset{˙}{0}\})) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j = \|a^{-1} [\{j\}]\| \cdot_{R} j$
419	418	mpteq2dva	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to (j \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j) = (j \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ \|a^{-1} [\{j\}]\| \cdot_{R} j)$
420	419	oveq2d	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j) = \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (\|a^{-1} [\{j\}]\| \cdot_{R} j)$
421	390 391 420	3eqtr4d	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to X = \underset{j \in ran a ∖ \{\underset{˙}{0}\}}{\sum_{R}} (ℤRHom (R) (\|a^{-1} [\{j\}]\|) \underset{˙}{\cdot} j)$
422	370 388 421	3eqtr4rd	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to X = \underset{j \in ⋃ S}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j)$
423	351 422	jca	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to ({finSupp}_{\underset{˙}{0}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}))) \land X = \underset{j \in ⋃ S}{\sum_{R}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \underset{˙}{\cdot} j))$
424	289 335 423	rspcedvdw	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land \forall k \in S a (k) \in k) \to \exists b \in (B^{⋃ S}) ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
425	424	3anasss	$⊢ ((φ \land a \in (B^{S})) \land ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)) \to \exists b \in (B^{⋃ S}) ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
426	425	r19.29an	$⊢ (φ \land \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k)) \to \exists b \in (B^{⋃ S}) ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
427	282 426	impbida	$⊢ φ \to (\exists b \in (B^{⋃ S}) ({finSupp}_{\underset{˙}{0}} (b) \land X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \leftrightarrow \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k))$
428	14 427	bitrd	$⊢ φ \to (X \in N (⋃ S) \leftrightarrow \exists a \in (B^{S}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{R} a \land \forall k \in S a (k) \in k))$

Metamath Proof Explorer

Theorem elrspunidl

Proof