elrspunidl

Description: Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024)

	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	biimpi	$⊢ j \in ⋃ S \to \exists i \in S j \in i$
20	19	adantl	$⊢ (φ \land j \in ⋃ S) \to \exists i \in S j \in i$
21	20	ralrimiva	$⊢ φ \to \forall j \in ⋃ S \exists i \in S j \in i$
22		eleq2	$⊢ i = f (j) \to (j \in i \leftrightarrow j \in f (j))$
23	22	ac6sg	$⊢ ⋃ S \in V \to (\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)))$
24	17 21 23	sylc	$⊢ φ \to \exists f (f : ⋃ S ⟶ S \land \forall j \in ⋃ S j \in f (j))$
25	24	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))$
26		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 φ$
27	26	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 φ$
28		ringcmn	$⊢ R \in Ring \to R \in CMnd$
29	27 5 28	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$
30		vex	$⊢ f \in V$
31		cnvexg	$⊢ f \in V \to f^{-1} \in V$
32		imaexg	$⊢ f^{-1} \in V \to f^{-1} [\{i\}] \in V$
33	30 31 32	mp2b	$⊢ f^{-1} [\{i\}] \in V$
34	33	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$
35	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$
36		elmapi	$⊢ b \in (B^{⋃ S}) \to b : ⋃ S ⟶ B$
37	36	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$
38		cnvimass	$⊢ f^{-1} [\{i\}] \subseteq dom f$
39		fdm	$⊢ f : ⋃ S ⟶ S \to dom f = ⋃ S$
40	38 39	sseqtrid	$⊢ f : ⋃ S ⟶ S \to f^{-1} [\{i\}] \subseteq ⋃ S$
41	40	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$
42	41	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$
43	37 42	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$
44	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$
45	44 42	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$
46	2 4	ringcl	$⊢ (R \in Ring \land b (l) \in B \land l \in B) \to b (l) \underset{˙}{\cdot} l \in B$
47	35 43 45 46	syl3anc	$⊢ (((((((φ \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$
48		fveq2	$⊢ j = l \to b (j) = b (l)$
49		id	$⊢ j = l \to j = l$
50	48 49	oveq12d	$⊢ j = l \to b (j) \underset{˙}{\cdot} j = b (l) \underset{˙}{\cdot} l$
51	50	cbvmptv	$⊢ (j \in f^{-1} [\{i\}] ⟼ b (j) \underset{˙}{\cdot} j) = (l \in f^{-1} [\{i\}] ⟼ b (l) \underset{˙}{\cdot} l)$
52	47 51	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$
53	34	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$
54	52	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)$
55		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)$
56		nfv	$⊢ Ⅎ j ((φ \land b \in (B^{⋃ S})) \land {finSupp}_{\underset{˙}{0}} (b))$
57		nfcv	$⊢ \underline{Ⅎ} j R$
58		nfcv	$⊢ \underline{Ⅎ} j Σ_{𝑔}$
59		nfmpt1	$⊢ \underline{Ⅎ} j (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
60	57 58 59	nfov	$⊢ \underline{Ⅎ} j (\underset{j \in ⋃ S}{\sum_{R}}, (b (j) \underset{˙}{\cdot} j))$
61	60	nfeq2	$⊢ Ⅎ j X = \underset{j \in ⋃ S}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)$
62	56 61	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))$
63		nfv	$⊢ Ⅎ j f : ⋃ S ⟶ S$
64	62 63	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)$
65		nfra1	$⊢ Ⅎ j \forall j \in ⋃ S j \in f (j)$
66	64 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)) \land f : ⋃ S ⟶ S) \land \forall j \in ⋃ S j \in f (j))$
67		nfv	$⊢ Ⅎ j i \in 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) \land \forall j \in ⋃ S j \in f (j)) \land i \in S)$
69		nfcv	$⊢ \underline{Ⅎ} j f^{-1} [\{i\}]$
70		nfcv	$⊢ \underline{Ⅎ} j {supp}_{\underset{˙}{0}} (b)$
71	36	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$
72	71	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$
73	26 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$
74	73	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$
75	3	fvexi	$⊢ \underset{˙}{0} \in V$
76	75	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$
77	41	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)$
78	77	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))$
79	72 74 76 78	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}$
80	79	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$
81	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$
82	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$
83	78	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$
84	82 83	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$
85	2 4 3	ringlz	$⊢ (R \in Ring \land j \in B) \to \underset{˙}{0} \underset{˙}{\cdot} j = \underset{˙}{0}$
86	81 84 85	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}$
87	80 86	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}$
88	68 69 70 87 34	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}$
89		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))$
90	53 54 55 88 89	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))$
91	2 3 29 34 52 90	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$
92	91	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$
93	2	fvexi	$⊢ B \in V$
94	93	a1i	$⊢ φ \to B \in V$
95	94 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)$
96	95	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})$
97	26 92 96	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})$
98		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))))$
99		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))$
100	99	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)))$
101		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)$
102	101	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)$
103	102	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)$
104	98 100 103	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))$
105	104	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 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))$
106	26 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$
107	106	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$
108	75	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$
109		funmpt	$⊢ Fun (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))$
110	109	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))$
111		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$
112	111	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$
113		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)$
114	113	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$
115		imafi	$⊢ (Fun f \land b supp \underset{˙}{0} \in Fin) \to f [b supp \underset{˙}{0}] \in Fin$
116	112 114 115	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$
117		nfv	$⊢ Ⅎ j i \in (S ∖ f [b supp \underset{˙}{0}])$
118	66 117	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}]))$
119		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$
120	119	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$
121		snssi	$⊢ i \in (S ∖ f [b supp \underset{˙}{0}]) \to \{i\} \subseteq S ∖ f [b supp \underset{˙}{0}]$
122	121	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}]$
123		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}]]$
124	120 122 123	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}]]$
125		difpreima	$⊢ Fun f \to f^{-1} [S ∖ f [b supp \underset{˙}{0}]] = f^{-1} [S] ∖ f^{-1} [f [b supp \underset{˙}{0}]]$
126	120 125	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}]]$
127	124 126	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}]]$
128		suppssdm	$⊢ b supp \underset{˙}{0} \subseteq dom b$
129	36	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$
130	128 129	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$
131	119	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$
132	130 131	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$
133		sseqin2	$⊢ b supp \underset{˙}{0} \subseteq dom f \leftrightarrow dom f \cap {supp}_{\underset{˙}{0}} (b) = b supp \underset{˙}{0}$
134	133	biimpi	$⊢ b supp \underset{˙}{0} \subseteq dom f \to dom f \cap {supp}_{\underset{˙}{0}} (b) = b supp \underset{˙}{0}$
135		dminss	$⊢ dom f \cap {supp}_{\underset{˙}{0}} (b) \subseteq f^{-1} [f [b supp \underset{˙}{0}]]$
136	134 135	eqsstrrdi	$⊢ b supp \underset{˙}{0} \subseteq dom f \to b supp \underset{˙}{0} \subseteq f^{-1} [f [b supp \underset{˙}{0}]]$
137	132 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 b supp \underset{˙}{0} \subseteq f^{-1} [f [b supp \underset{˙}{0}]]$
138	137	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)$
139	127 138	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)$
140		fimacnv	$⊢ f : ⋃ S ⟶ S \to f^{-1} [S] = ⋃ S$
141	119 140	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$
142	141	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)$
143	139 142	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)$
144	143	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))$
145		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}$
146	73	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$
147	75	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$
148	129 145 146 147	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}$
149	144 148	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}$
150	149	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$
151	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$
152	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$
153	40	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$
154	153	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$
155	152 154	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$
156	151 155 85	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}$
157	150 156	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}$
158	118 157	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})$
159	158	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}$
160	5 28	syl	$⊢ φ \to R \in CMnd$
161	160	cmnmndd	$⊢ φ \to R \in Mnd$
162	161	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$
163	3	gsumz	$⊢ (R \in Mnd \land f^{-1} [\{i\}] \in V) \to \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
164	162 33 163	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}$
165	159 164	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}$
166	165 106	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}]$
167	116 166	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$
168		isfsupp	$⊢ ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j))) \leftrightarrow (Fun (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) supp \underset{˙}{0} \in Fin))$
169	168	biimpar	$⊢ (((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \in V \land \underset{˙}{0} \in V) \land (Fun (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) \land (i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)) supp \underset{˙}{0} \in Fin)) \to {finSupp}_{\underset{˙}{0}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)))$
170	107 108 110 167 169	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}} ((i \in S ⟼ \underset{j \in f^{-1} [\{i\}]}{\sum_{R}} (b (j) \underset{˙}{\cdot} j)))$
171		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)$
172	26 160	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$
173	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$
174	36	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$
175	174	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$
176	26 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$
177	176	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$
178	2 4	ringcl	$⊢ (R \in Ring \land b (j) \in B \land j \in B) \to b (j) \underset{˙}{\cdot} j \in B$
179	173 175 177 178	syl3anc	$⊢ ((((((φ \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$
180		eqid	$⊢ (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j) = (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
181	66 179 180	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$
182	73	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$
183		funmpt	$⊢ Fun (j \in ⋃ S ⟼ b (j) \underset{˙}{\cdot} j)$
184	183	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)$
185		nfcv	$⊢ \underline{Ⅎ} j ⋃ S$
186	174	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$
187	186	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$
188	73	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$
189	75	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$
190		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))$
191	187 188 189 190	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}$
192	191	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$
193	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$
194	176	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$
195	190	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$
196	194 195	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$
197	193 196 85	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}$
198	192 197	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}$
199	66 185 70 198 73	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}$
200		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))$
201	182 184 113 199 200	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))$
202		sndisj	$⊢ \underset{i \in S}{Disj} \{i\}$
203		disjpreima	$⊢ (Fun f \land \underset{i \in S}{Disj} \{i\}) \to \underset{i \in S}{Disj} f^{-1} [\{i\}]$
204	112 202 203	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\}]$
205		iunid	$⊢ ⋃_{i \in S} \{i\} = S$
206	205	imaeq2i	$⊢ f^{-1} [⋃_{i \in S} \{i\}] = f^{-1} [S]$
207		iunpreima	$⊢ Fun f \to f^{-1} [⋃_{i \in S} \{i\}] = ⋃_{i \in S} f^{-1} [\{i\}]$
208	112 207	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\}]$
209	140	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$
210	206 208 209	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$
211	2 3 172 73 106 181 201 204 210	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\}]}))$
212	41	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)$
213	212	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)$
214	213	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))$
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)) \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))$
216	171 211 215	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))$
217		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))$
218		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$
219	218	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\}$
220	219	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\}]$
221	220	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)$
222	221	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)$
223		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$
224		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$
225	217 222 223 224	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)$
226	160	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$
227	30	cnvex	$⊢ f^{-1} \in V$
228	227	imaex	$⊢ f^{-1} [\{k\}] \in V$
229	228	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$
230	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$
231	26 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)$
232	231	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)$
233	8	lidlsubg	$⊢ (R \in Ring \land k \in LIdeal (R)) \to k \in SubGrp (R)$
234		subgsubm	$⊢ k \in SubGrp (R) \to k \in SubMnd (R)$
235	233 234	syl	$⊢ (R \in Ring \land k \in LIdeal (R)) \to k \in SubMnd (R)$
236	230 232 235	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)$
237	230	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$
238	232	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)$
239	36	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$
240		cnvimass	$⊢ f^{-1} [\{k\}] \subseteq dom f$
241	240 39	sseqtrid	$⊢ f : ⋃ S ⟶ S \to f^{-1} [\{k\}] \subseteq ⋃ S$
242	241	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$
243	242	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$
244	239 243	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$
245		fveq2	$⊢ j = l \to f (j) = f (l)$
246	49 245	eleq12d	$⊢ j = l \to (j \in f (j) \leftrightarrow l \in f (l))$
247		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)$
248	246 247 243	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)$
249		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$
250	249	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$
251		elpreima	$⊢ f Fn ⋃ S \to (l \in f^{-1} [\{k\}] \leftrightarrow (l \in ⋃ S \land f (l) \in \{k\}))$
252	251	biimpa	$⊢ (f Fn ⋃ S \land l \in f^{-1} [\{k\}]) \to (l \in ⋃ S \land f (l) \in \{k\})$
253		elsni	$⊢ f (l) \in \{k\} \to f (l) = k$
254	252 253	simpl2im	$⊢ (f Fn ⋃ S \land l \in f^{-1} [\{k\}]) \to f (l) = k$
255	250 254	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$
256	248 255	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$
257	8 2 4	lidlmcl	$⊢ ((R \in Ring \land k \in LIdeal (R)) \land (b (l) \in B \land l \in k)) \to b (l) \underset{˙}{\cdot} l \in k$
258	237 238 244 256 257	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) \land l \in f^{-1} [\{k\}]) \to b (l) \underset{˙}{\cdot} l \in k$
259	50	cbvmptv	$⊢ (j \in f^{-1} [\{k\}] ⟼ b (j) \underset{˙}{\cdot} j) = (l \in f^{-1} [\{k\}] ⟼ b (l) \underset{˙}{\cdot} l)$
260	258 259	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$
261	229	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$
262	260	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)$
263		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)$
264		nfv	$⊢ Ⅎ j k \in S$
265	66 264	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)$
266		nfcv	$⊢ \underline{Ⅎ} j f^{-1} [\{k\}]$
267	36	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$
268	267	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$
269	73	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$
270	75	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$
271	242	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)$
272	271	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))$
273	268 269 270 272	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}$
274	273	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$
275	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$
276	272	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$
277	275 276	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$
278	230 277 85	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}$
279	274 278	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}$
280	265 266 70 279 229	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}$
281		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))$
282	261 262 263 280 281	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))$
283	3 226 229 236 260 282	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$
284	225 283	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$
285	284	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$
286	170 216 285	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)$
287	97 105 286	rspcedvd	$⊢ (((((φ \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)$
288	287	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)$
289	25 288	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)$
290	289	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)$
291	290	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)$
292	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$
293	292	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$
294		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
295	294	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
296		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
297	296 2	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ B$
298	293 295 297	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$
299		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})$
300	75	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$
301		ssv	$⊢ ran a \subseteq V$
302		ssdif	$⊢ ran a \subseteq V \to ran a ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
303	301 302	ax-mp	$⊢ ran a ∖ \{\underset{˙}{0}\} \subseteq V ∖ \{\underset{˙}{0}\}$
304	303	sseli	$⊢ m \in (ran a ∖ \{\underset{˙}{0}\}) \to m \in (V ∖ \{\underset{˙}{0}\})$
305	304	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}\})$
306		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)$
307	299 300 305 306	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$
308		hashcl	$⊢ a^{-1} [\{m\}] \in Fin \to \|a^{-1} [\{m\}]\| \in ℕ_{0}$
309	307 308	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}$
310	309	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 ℤ$
311	298 310	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$
312		eqid	$⊢ (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) = (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|))$
313	311 312	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$
314	2 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
315		fconst6g	$⊢ \underset{˙}{0} \in B \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) : ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) ⟶ B$
316	292 314 315	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$
317		disjdif	$⊢ (ran a ∖ \{\underset{˙}{0}\}) \cap (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = \emptyset$
318	317	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$
319	313 316 318	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$
320		simplll	$⊢ ((((φ \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 (φ \land a \in (B^{S}))$
321	94 16	elmapd	$⊢ φ \to (a \in (B^{S}) \leftrightarrow a : S ⟶ B)$
322	321	biimpa	$⊢ (φ \land a \in (B^{S})) \to a : S ⟶ B$
323	320 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) \to a : S ⟶ B$
324	323	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$
325		elssuni	$⊢ k \in S \to k \subseteq ⋃ S$
326	325	adantl	$⊢ ((((φ \land a \in (B^{S})) \land {finSupp}_{\underset{˙}{0}} (a)) \land X = \sum_{R} a) \land k \in S) \to k \subseteq ⋃ S$
327	326	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)$
328	327	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)$
329	328	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$
330		fnfvrnss	$⊢ (a Fn S \land \forall k \in S a (k) \in ⋃ S) \to ran a \subseteq ⋃ S$
331	324 329 330	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$
332	331	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$
333		undif	$⊢ ran a ∖ \{\underset{˙}{0}\} \subseteq ⋃ S \leftrightarrow (ran a ∖ \{\underset{˙}{0}\}) \cup (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) = ⋃ S$
334	332 333	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$
335	334	feq2d	$⊢ ((((φ \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 \leftrightarrow ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) : ⋃ S ⟶ B)$
336	319 335	mpbid	$⊢ ((((φ \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$
337	93	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$
338	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$
339	337 338	elmapd	$⊢ ((((φ \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}) \leftrightarrow ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) : ⋃ S ⟶ B)$
340	336 339	mpbird	$⊢ ((((φ \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})$
341		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}\}))))$
342		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)$
343	342	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$
344	343	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)$
345	344	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)$
346	345	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))$
347	341 346	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)))$
348	347	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 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)))$
349	319	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}\}))$
350	340	elexd	$⊢ ((((φ \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 V$
351	75	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$
352	323	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$
353	320	simprd	$⊢ ((((φ \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})$
354		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)$
355		fsupprnfi	$⊢ ((Fun a \land a \in (B^{S})) \land (\underset{˙}{0} \in V \land {finSupp}_{\underset{˙}{0}} (a))) \to ran a \in Fin$
356		diffi	$⊢ ran a \in Fin \to ran a ∖ \{\underset{˙}{0}\} \in Fin$
357	355 356	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$
358	352 353 351 354 357	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$
359	313 358 351	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\}]\|)))$
360	13	ssdifssd	$⊢ φ \to ⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}) \subseteq B$
361	360	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$
362	337 361	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$
363	362 351	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}\}))$
364	359 363	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$
365		funisfsupp	$⊢ (Fun ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) \land (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}))) \leftrightarrow ((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)$
366	365	biimpar	$⊢ ((Fun ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) \land (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) \in V \land \underset{˙}{0} \in V) \land ((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) \to {finSupp}_{\underset{˙}{0}} (((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})))$
367	349 350 351 364 366	syl31anc	$⊢ ((((φ \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}\})))$
368		fvex	$⊢ ℤRHom (R) (\|a^{-1} [\{m\}]\|) \in V$
369	368 312	fnmpti	$⊢ (m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) Fn (ran a ∖ \{\underset{˙}{0}\})$
370	369	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}\})$
371		fnconstg	$⊢ \underset{˙}{0} \in V \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) Fn (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))$
372	75 371	ax-mp	$⊢ ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) Fn (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\}))$
373	372	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}\}))$
374	317	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$
375		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}\})$
376	370 373 374 375	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)$
377		sneq	$⊢ m = j \to \{m\} = \{j\}$
378	377	imaeq2d	$⊢ m = j \to a^{-1} [\{m\}] = a^{-1} [\{j\}]$
379	378	fveq2d	$⊢ m = j \to \|a^{-1} [\{m\}]\| = \|a^{-1} [\{j\}]\|$
380	379	fveq2d	$⊢ m = j \to ℤRHom (R) (\|a^{-1} [\{m\}]\|) = ℤRHom (R) (\|a^{-1} [\{j\}]\|)$
381		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$
382	312 380 375 381	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\}]\|)$
383	376 382	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\}]\|)$
384	383	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$
385	384	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)$
386	385	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)$
387	292 28	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) \to R \in CMnd$
388	317	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$
389		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)$
390	369 372 389	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)$
391	388 390	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)$
392	75	fvconst2	$⊢ j \in (⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \to ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\}) (j) = \underset{˙}{0}$
393	392	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}$
394	391 393	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}$
395	394	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$
396	361	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$
397	292 396 85	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}$
398	395 397	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}$
399	292	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$
400	336	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$
401	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$
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 ⋃ S) \to j \in B$
403	2 4	ringcl	$⊢ (R \in Ring \land ((m \in (ran a ∖ \{\underset{˙}{0}\}) ⟼ ℤRHom (R) (\|a^{-1} [\{m\}]\|)) \cup ((⋃ S ∖ (ran a ∖ \{\underset{˙}{0}\})) \times \{\underset{˙}{0}\})) (j) \in B \land j \in B) \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$
404	399 400 402 403	syl3anc	$⊢ (((((φ \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$
405	2 3 387 338 398 358 404 332	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)$
406		eqid	$⊢ \cdot_{R} = \cdot_{R}$
407	2 3 406 387 323 354	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)$
408		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$
409	292	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$
410	353	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})$
411	75	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$
412	303 375	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}\})$
413	354	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 {finSupp}_{\underset{˙}{0}} (a)$
414	410 411 412 413	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$
415		hashcl	$⊢ a^{-1} [\{j\}] \in Fin \to \|a^{-1} [\{j\}]\| \in ℕ_{0}$
416	414 415	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}$
417	416	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 ℤ$
418	332 401	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$
419	418	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$
420		eqid	$⊢ 1_{R} = 1_{R}$
421	294 406 420	zrhmulg	$⊢ (R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \to ℤRHom (R) (\|a^{-1} [\{j\}]\|) = \|a^{-1} [\{j\}]\| \cdot_{R} 1_{R}$
422	421	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}$
423	422	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$
424		simpll	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to R \in Ring$
425		simplr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to \|a^{-1} [\{j\}]\| \in ℤ$
426	2 420	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
427	426	ad2antrr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to 1_{R} \in B$
428		simpr	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to j \in B$
429	2 406 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)$
430	424 425 427 428 429	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)$
431	2 4 420	ringlidm	$⊢ (R \in Ring \land j \in B) \to 1_{R} \underset{˙}{\cdot} j = j$
432	424 431	sylancom	$⊢ ((R \in Ring \land \|a^{-1} [\{j\}]\| \in ℤ) \land j \in B) \to 1_{R} \underset{˙}{\cdot} j = j$
433	432	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$
434	423 430 433	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$
435	409 417 419 434	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$
436	435	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)$
437	436	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)$
438	407 408 437	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)$
439	386 405 438	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)$
440	367 439	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))$
441	340 348 440	rspcedvd	$⊢ ((((φ \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))$
442	441	exp41	$⊢ (φ \land a \in (B^{S})) \to ({finSupp}_{\underset{˙}{0}} (a) \to (X = \sum_{R} a \to (\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)))))$
443	442	3imp2	$⊢ ((φ \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))$
444	443	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))$
445	291 444	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))$
446	14 445	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