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