elrspunsn

Description: Membership to the span of an ideal R and a single element X . (Contributed by Thierry Arnoux, 9-Mar-2025)

	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$
	elrspunsn.p	$⊢ \underset{˙}{+} = +_{R}$
	elrspunsn.i	$⊢ φ \to I \in LIdeal (R)$
	elrspunsn.x	$⊢ φ \to X \in (B ∖ I)$
Assertion	elrspunsn	$⊢ φ \to (A \in N (I \cup \{X\}) \leftrightarrow \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i)$

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		elrspunsn.p	$⊢ \underset{˙}{+} = +_{R}$
7		elrspunsn.i	$⊢ φ \to I \in LIdeal (R)$
8		elrspunsn.x	$⊢ φ \to X \in (B ∖ I)$
9		eqid	$⊢ LIdeal (R) = LIdeal (R)$
10	2 9	lidlss	$⊢ I \in LIdeal (R) \to I \subseteq B$
11	7 10	syl	$⊢ φ \to I \subseteq B$
12	8	eldifad	$⊢ φ \to X \in B$
13	12	snssd	$⊢ φ \to \{X\} \subseteq B$
14	11 13	unssd	$⊢ φ \to I \cup \{X\} \subseteq B$
15	1 2 3 4 5 14	elrsp	$⊢ φ \to (A \in N (I \cup \{X\}) \leftrightarrow \exists a \in (B^{(I \cup \{X\})}) ({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)))$
16		oveq1	$⊢ r = a (X) \to r \underset{˙}{\cdot} X = a (X) \underset{˙}{\cdot} X$
17	16	oveq1d	$⊢ r = a (X) \to (r \underset{˙}{\cdot} X) \underset{˙}{+} i = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} i$
18	17	eqeq2d	$⊢ r = a (X) \to (A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i \leftrightarrow A = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} i)$
19		oveq2	$⊢ i = \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \to (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} i = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
20	19	eqeq2d	$⊢ i = \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \to (A = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} i \leftrightarrow A = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)))$
21		elmapi	$⊢ a \in (B^{(I \cup \{X\})}) \to a : I \cup \{X\} ⟶ B$
22	21	ad3antlr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to a : I \cup \{X\} ⟶ B$
23	12	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to X \in B$
24		snidg	$⊢ X \in B \to X \in \{X\}$
25		elun2	$⊢ X \in \{X\} \to X \in (I \cup \{X\})$
26	23 24 25	3syl	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to X \in (I \cup \{X\})$
27	22 26	ffvelcdmd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to a (X) \in B$
28	2	fvexi	$⊢ B \in V$
29	28	a1i	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to B \in V$
30	7	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to I \in LIdeal (R)$
31		ssun1	$⊢ I \subseteq I \cup \{X\}$
32	31	a1i	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to I \subseteq I \cup \{X\}$
33	22 32	fssresd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to ({a ↾}_{I}) : I ⟶ B$
34	29 30 33	elmapdd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to {a ↾}_{I} \in (B^{I})$
35		breq1	$⊢ b = {a ↾}_{I} \to ({finSupp}_{\underset{˙}{0}} (b) \leftrightarrow {finSupp}_{\underset{˙}{0}} (({a ↾}_{I})))$
36		fveq1	$⊢ b = {a ↾}_{I} \to b (y) = ({a ↾}_{I}) (y)$
37	36	oveq1d	$⊢ b = {a ↾}_{I} \to b (y) \underset{˙}{\cdot} y = ({a ↾}_{I}) (y) \underset{˙}{\cdot} y$
38	37	mpteq2dv	$⊢ b = {a ↾}_{I} \to (y \in I ⟼ b (y) \underset{˙}{\cdot} y) = (y \in I ⟼ ({a ↾}_{I}) (y) \underset{˙}{\cdot} y)$
39	38	oveq2d	$⊢ b = {a ↾}_{I} \to \underset{y \in I}{\sum_{R}} (b (y) \underset{˙}{\cdot} y) = \underset{y \in I}{\sum_{R}} (({a ↾}_{I}) (y) \underset{˙}{\cdot} y)$
40	39	eqeq2d	$⊢ b = {a ↾}_{I} \to (\underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (b (y) \underset{˙}{\cdot} y) \leftrightarrow \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (({a ↾}_{I}) (y) \underset{˙}{\cdot} y))$
41	35 40	anbi12d	$⊢ b = {a ↾}_{I} \to (({finSupp}_{\underset{˙}{0}} (b) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (b (y) \underset{˙}{\cdot} y)) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (({a ↾}_{I})) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (({a ↾}_{I}) (y) \underset{˙}{\cdot} y)))$
42	41	adantl	$⊢ ((((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \land b = {a ↾}_{I}) \to (({finSupp}_{\underset{˙}{0}} (b) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (b (y) \underset{˙}{\cdot} y)) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (({a ↾}_{I})) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (({a ↾}_{I}) (y) \underset{˙}{\cdot} y)))$
43		simplr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to {finSupp}_{\underset{˙}{0}} (a)$
44	5	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to R \in Ring$
45	2 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
46	44 45	syl	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \underset{˙}{0} \in B$
47	43 46	fsuppres	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to {finSupp}_{\underset{˙}{0}} (({a ↾}_{I}))$
48		fveq2	$⊢ x = y \to a (x) = a (y)$
49		id	$⊢ x = y \to x = y$
50	48 49	oveq12d	$⊢ x = y \to a (x) \underset{˙}{\cdot} x = a (y) \underset{˙}{\cdot} y$
51	50	cbvmptv	$⊢ (x \in I ⟼ a (x) \underset{˙}{\cdot} x) = (y \in I ⟼ a (y) \underset{˙}{\cdot} y)$
52		simpr	$⊢ ((((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \land y \in I) \to y \in I$
53	52	fvresd	$⊢ ((((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \land y \in I) \to ({a ↾}_{I}) (y) = a (y)$
54	53	oveq1d	$⊢ ((((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \land y \in I) \to ({a ↾}_{I}) (y) \underset{˙}{\cdot} y = a (y) \underset{˙}{\cdot} y$
55	54	mpteq2dva	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to (y \in I ⟼ ({a ↾}_{I}) (y) \underset{˙}{\cdot} y) = (y \in I ⟼ a (y) \underset{˙}{\cdot} y)$
56	51 55	eqtr4id	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to (x \in I ⟼ a (x) \underset{˙}{\cdot} x) = (y \in I ⟼ ({a ↾}_{I}) (y) \underset{˙}{\cdot} y)$
57	56	oveq2d	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (({a ↾}_{I}) (y) \underset{˙}{\cdot} y)$
58	47 57	jca	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to ({finSupp}_{\underset{˙}{0}} (({a ↾}_{I})) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (({a ↾}_{I}) (y) \underset{˙}{\cdot} y))$
59	34 42 58	rspcedvd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \exists b \in (B^{I}) ({finSupp}_{\underset{˙}{0}} (b) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (b (y) \underset{˙}{\cdot} y))$
60	11	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to I \subseteq B$
61	1 2 3 4 44 60	elrsp	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to (\underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \in N (I) \leftrightarrow \exists b \in (B^{I}) ({finSupp}_{\underset{˙}{0}} (b) \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{y \in I}{\sum_{R}} (b (y) \underset{˙}{\cdot} y)))$
62	59 61	mpbird	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \in N (I)$
63	1 9	rspidlid	$⊢ (R \in Ring \land I \in LIdeal (R)) \to N (I) = I$
64	5 7 63	syl2anc	$⊢ φ \to N (I) = I$
65	64	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to N (I) = I$
66	62 65	eleqtrd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \in I$
67		simpr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)$
68	5	ringcmnd	$⊢ φ \to R \in CMnd$
69	68	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to R \in CMnd$
70	7	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to I \in LIdeal (R)$
71		snex	$⊢ \{X\} \in V$
72	71	a1i	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \{X\} \in V$
73	70 72	unexd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to I \cup \{X\} \in V$
74	5	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to R \in Ring$
75	21	ad3antlr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to a : I \cup \{X\} ⟶ B$
76		simpr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to x \in (I \cup \{X\})$
77	75 76	ffvelcdmd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to a (x) \in B$
78	14	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to I \cup \{X\} \subseteq B$
79	78 76	sseldd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to x \in B$
80	2 4 74 77 79	ringcld	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I \cup \{X\})) \to a (x) \underset{˙}{\cdot} x \in B$
81	73	mptexd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x) \in V$
82	5 45	syl	$⊢ φ \to \underset{˙}{0} \in B$
83	82	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \underset{˙}{0} \in B$
84		funmpt	$⊢ Fun (x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x)$
85	84	a1i	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to Fun (x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x)$
86		simpr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to {finSupp}_{\underset{˙}{0}} (a)$
87	86	fsuppimpd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to a supp \underset{˙}{0} \in Fin$
88	21	ad3antlr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to a : I \cup \{X\} ⟶ B$
89	88	ffnd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to a Fn (I \cup \{X\})$
90	73	adantr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to I \cup \{X\} \in V$
91	5	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to R \in Ring$
92	91 45	syl	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to \underset{˙}{0} \in B$
93		simpr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))$
94	89 90 92 93	fvdifsupp	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to a (x) = \underset{˙}{0}$
95	94	oveq1d	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to a (x) \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} x$
96	14	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to I \cup \{X\} \subseteq B$
97	93	eldifad	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in (I \cup \{X\})$
98	96 97	sseldd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in B$
99	2 4 3	ringlz	$⊢ (R \in Ring \land x \in B) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
100	91 98 99	syl2anc	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
101	95 100	eqtrd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))) \to a (x) \underset{˙}{\cdot} x = \underset{˙}{0}$
102	101 73	suppss2	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x) supp \underset{˙}{0} \subseteq a supp \underset{˙}{0}$
103	87 102	ssfid	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x) supp \underset{˙}{0} \in Fin$
104	81 83 85 103	isfsuppd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to {finSupp}_{\underset{˙}{0}} ((x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x))$
105	8	eldifbd	$⊢ φ \to \neg X \in I$
106	105	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \neg X \in I$
107		disjsn	$⊢ I \cap \{X\} = \emptyset \leftrightarrow \neg X \in I$
108	106 107	sylibr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to I \cap \{X\} = \emptyset$
109		eqidd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to I \cup \{X\} = I \cup \{X\}$
110	2 3 6 69 73 80 104 108 109	gsumsplit2	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (\underset{x \in \{X\}}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
111	69	cmnmndd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to R \in Mnd$
112	12	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to X \in B$
113	5	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to R \in Ring$
114	21	ad2antlr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to a : I \cup \{X\} ⟶ B$
115		ssun2	$⊢ \{X\} \subseteq I \cup \{X\}$
116	12 24	syl	$⊢ φ \to X \in \{X\}$
117	116	ad2antrr	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to X \in \{X\}$
118	115 117	sselid	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to X \in (I \cup \{X\})$
119	114 118	ffvelcdmd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to a (X) \in B$
120	2 4 113 119 112	ringcld	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to a (X) \underset{˙}{\cdot} X \in B$
121		simpr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x = X) \to x = X$
122	121	fveq2d	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x = X) \to a (x) = a (X)$
123	122 121	oveq12d	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x = X) \to a (x) \underset{˙}{\cdot} x = a (X) \underset{˙}{\cdot} X$
124	2 111 112 120 123	gsumsnd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \underset{x \in \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = a (X) \underset{˙}{\cdot} X$
125	124	oveq2d	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (\underset{x \in \{X\}}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)) = (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (a (X) \underset{˙}{\cdot} X)$
126	5	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to R \in Ring$
127	21	ad3antlr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to a : I \cup \{X\} ⟶ B$
128		simpr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to x \in I$
129	31 128	sselid	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to x \in (I \cup \{X\})$
130	127 129	ffvelcdmd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to a (x) \in B$
131	11	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to I \subseteq B$
132	131 128	sseldd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to x \in B$
133	2 4 126 130 132	ringcld	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in I) \to a (x) \underset{˙}{\cdot} x \in B$
134	133	fmpttd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (x \in I ⟼ a (x) \underset{˙}{\cdot} x) : I ⟶ B$
135	31	a1i	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to I \subseteq I \cup \{X\}$
136	135	ssdifd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to I ∖ {supp}_{\underset{˙}{0}} (a) \subseteq (I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a)$
137	136	sselda	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} (a))$
138	137 94	syldan	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to a (x) = \underset{˙}{0}$
139	138	oveq1d	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to a (x) \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} x$
140	5	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to R \in Ring$
141	11	ad3antrrr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to I \subseteq B$
142		simpr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in (I ∖ {supp}_{\underset{˙}{0}} (a))$
143	142	eldifad	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in I$
144	141 143	sseldd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to x \in B$
145	140 144 99	syl2anc	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
146	139 145	eqtrd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (a))) \to a (x) \underset{˙}{\cdot} x = \underset{˙}{0}$
147	146 70	suppss2	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (x \in I ⟼ a (x) \underset{˙}{\cdot} x) supp \underset{˙}{0} \subseteq a supp \underset{˙}{0}$
148	87 147	ssfid	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (x \in I ⟼ a (x) \underset{˙}{\cdot} x) supp \underset{˙}{0} \in Fin$
149	2 3 69 70 134 148	gsumcl2	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \in B$
150	2 6	cmncom	$⊢ (R \in CMnd \land \underset{x \in I}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \in B \land a (X) \underset{˙}{\cdot} X \in B) \to (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (a (X) \underset{˙}{\cdot} X) = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
151	69 149 120 150	syl3anc	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (a (X) \underset{˙}{\cdot} X) = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
152	110 125 151	3eqtrd	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \to \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
153	152	adantr	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
154	67 153	eqtrd	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to A = (a (X) \underset{˙}{\cdot} X) \underset{˙}{+} (\underset{x \in I}{\sum_{R}}, (a (x) \underset{˙}{\cdot} x))$
155	18 20 27 66 154	2rspcedvdw	$⊢ (((φ \land a \in (B^{(I \cup \{X\})})) \land {finSupp}_{\underset{˙}{0}} (a)) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \to \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i$
156	155	anasss	$⊢ ((φ \land a \in (B^{(I \cup \{X\})})) \land ({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x))) \to \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i$
157	156	r19.29an	$⊢ (φ \land \exists a \in (B^{(I \cup \{X\})}) ({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x))) \to \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i$
158	28	a1i	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to B \in V$
159	7	ad3antrrr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to I \in LIdeal (R)$
160	71	a1i	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \{X\} \in V$
161	159 160	unexd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to I \cup \{X\} \in V$
162		simp-4r	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in (I \cup \{X\})) \to r \in B$
163		eqid	$⊢ 1_{R} = 1_{R}$
164	2 163	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
165	5 164	syl	$⊢ φ \to 1_{R} \in B$
166	165	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in (I \cup \{X\})) \to 1_{R} \in B$
167	162 166	ifcld	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in (I \cup \{X\})) \to if (y = X, r, 1_{R}) \in B$
168	82	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in (I \cup \{X\})) \to \underset{˙}{0} \in B$
169	167 168	ifcld	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in (I \cup \{X\})) \to if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}) \in B$
170	169	fmpttd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) : I \cup \{X\} ⟶ B$
171	158 161 170	elmapdd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \in (B^{(I \cup \{X\})})$
172		breq1	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to ({finSupp}_{\underset{˙}{0}} (a) \leftrightarrow {finSupp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))$
173		fveq1	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to a (x) = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x)$
174	173	oveq1d	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to a (x) \underset{˙}{\cdot} x = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x$
175	174	mpteq2dv	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to (x \in (I \cup \{X\}) ⟼ a (x) \underset{˙}{\cdot} x) = (x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
176	175	oveq2d	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) = \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
177	176	eqeq2d	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to (A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x) \leftrightarrow A = \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x))$
178	172 177	anbi12d	$⊢ a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) \to (({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)))$
179	178	adantl	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land a = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))) \to (({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \leftrightarrow ({finSupp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)))$
180		eqid	$⊢ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))$
181		prfi	$⊢ \{X, i\} \in Fin$
182	181	a1i	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \{X, i\} \in Fin$
183		simp-4r	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in \{X, i\}) \to r \in B$
184	165	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in \{X, i\}) \to 1_{R} \in B$
185	183 184	ifcld	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land y \in \{X, i\}) \to if (y = X, r, 1_{R}) \in B$
186	82	ad3antrrr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \underset{˙}{0} \in B$
187	180 161 182 185 186	mptiffisupp	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to {finSupp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})))$
188	68	ad3antrrr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to R \in CMnd$
189	159 10	syl	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to I \subseteq B$
190		simplr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to i \in I$
191	189 190	sseldd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to i \in B$
192	5	ad3antrrr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to R \in Ring$
193		simpllr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to r \in B$
194	12	ad3antrrr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to X \in B$
195	2 4 192 193 194	ringcld	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to r \underset{˙}{\cdot} X \in B$
196	2 6	cmncom	$⊢ (R \in CMnd \land i \in B \land r \underset{˙}{\cdot} X \in B) \to i \underset{˙}{+} (r \underset{˙}{\cdot} X) = (r \underset{˙}{\cdot} X) \underset{˙}{+} i$
197	188 191 195 196	syl3anc	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to i \underset{˙}{+} (r \underset{˙}{\cdot} X) = (r \underset{˙}{\cdot} X) \underset{˙}{+} i$
198	188	cmnmndd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to R \in Mnd$
199		eqid	$⊢ (x \in I ⟼ if (x = i, i, \underset{˙}{0})) = (x \in I ⟼ if (x = i, i, \underset{˙}{0}))$
200	191 2	eleqtrdi	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to i \in {Base}_{R}$
201	3 198 159 190 199 200	gsummptif1n0	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \underset{x \in I}{\sum_{R}} if (x = i, i, \underset{˙}{0}) = i$
202		fveq2	$⊢ x = i \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (i)$
203		id	$⊢ x = i \to x = i$
204	202 203	oveq12d	$⊢ x = i \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (i) \underset{˙}{\cdot} i$
205	204	adantl	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (i) \underset{˙}{\cdot} i$
206		simpr	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to y = i$
207		prid2g	$⊢ i \in I \to i \in \{X, i\}$
208	207	ad5antlr	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to i \in \{X, i\}$
209	206 208	eqeltrd	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to y \in \{X, i\}$
210	209	iftrued	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}) = if (y = X, r, 1_{R})$
211	190	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to i \in I$
212	211	adantr	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to i \in I$
213	206 212	eqeltrd	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to y \in I$
214	105	ad3antrrr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \neg X \in I$
215	214	ad3antrrr	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to \neg X \in I$
216		nelneq	$⊢ (y \in I \land \neg X \in I) \to \neg y = X$
217	213 215 216	syl2anc	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to \neg y = X$
218	217	iffalsed	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to if (y = X, r, 1_{R}) = 1_{R}$
219	210 218	eqtrd	$⊢ ((((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \land y = i) \to if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}) = 1_{R}$
220	31 211	sselid	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to i \in (I \cup \{X\})$
221	192	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to R \in Ring$
222	221 164	syl	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to 1_{R} \in B$
223	180 219 220 222	fvmptd2	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (i) = 1_{R}$
224	223	oveq1d	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (i) \underset{˙}{\cdot} i = 1_{R} \underset{˙}{\cdot} i$
225	191	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to i \in B$
226	2 4 163 221 225	ringlidmd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to 1_{R} \underset{˙}{\cdot} i = i$
227	205 224 226	3eqtrrd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land x = i) \to i = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x$
228		eleq1w	$⊢ y = x \to (y \in \{X, i\} \leftrightarrow x \in \{X, i\})$
229		eqeq1	$⊢ y = x \to (y = X \leftrightarrow x = X)$
230	229	ifbid	$⊢ y = x \to if (y = X, r, 1_{R}) = if (x = X, r, 1_{R})$
231	228 230	ifbieq1d	$⊢ y = x \to if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}) = if (x \in \{X, i\}, if (x = X, r, 1_{R}), \underset{˙}{0})$
232		simplr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to x \in I$
233	31 232	sselid	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to x \in (I \cup \{X\})$
234	193	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to r \in B$
235	165	ad5antr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to 1_{R} \in B$
236	234 235	ifcld	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to if (x = X, r, 1_{R}) \in B$
237	186	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to \underset{˙}{0} \in B$
238	236 237	ifcld	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to if (x \in \{X, i\}, if (x = X, r, 1_{R}), \underset{˙}{0}) \in B$
239	180 231 233 238	fvmptd3	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) = if (x \in \{X, i\}, if (x = X, r, 1_{R}), \underset{˙}{0})$
240	214	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to \neg X \in I$
241		nelne2	$⊢ (x \in I \land \neg X \in I) \to x \neq X$
242	232 240 241	syl2anc	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to x \neq X$
243		neqne	$⊢ \neg x = i \to x \neq i$
244	243	adantl	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to x \neq i$
245	242 244	nelprd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to \neg x \in \{X, i\}$
246	245	iffalsed	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to if (x \in \{X, i\}, if (x = X, r, 1_{R}), \underset{˙}{0}) = \underset{˙}{0}$
247	239 246	eqtrd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) = \underset{˙}{0}$
248	247	oveq1d	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} x$
249	192	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to R \in Ring$
250	189	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to I \subseteq B$
251	250 232	sseldd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to x \in B$
252	249 251 99	syl2anc	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
253	248 252	eqtr2d	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \land \neg x = i) \to \underset{˙}{0} = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x$
254	227 253	ifeqda	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in I) \to if (x = i, i, \underset{˙}{0}) = (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x$
255	254	mpteq2dva	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (x \in I ⟼ if (x = i, i, \underset{˙}{0})) = (x \in I ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
256	255	oveq2d	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \underset{x \in I}{\sum_{R}} if (x = i, i, \underset{˙}{0}) = \underset{x \in I}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
257	201 256	eqtr3d	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to i = \underset{x \in I}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
258		simpr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to y = x$
259		simplr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to x = X$
260	194	ad2antrr	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to X \in B$
261		prid1g	$⊢ X \in B \to X \in \{X, i\}$
262	260 261	syl	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to X \in \{X, i\}$
263	259 262	eqeltrd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to x \in \{X, i\}$
264	258 263	eqeltrd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to y \in \{X, i\}$
265	264	iftrued	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}) = if (y = X, r, 1_{R})$
266	258 259	eqtrd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to y = X$
267	266	iftrued	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to if (y = X, r, 1_{R}) = r$
268	265 267	eqtrd	$⊢ (((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \land y = x) \to if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}) = r$
269		simpr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to x = X$
270	116	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to X \in \{X\}$
271	270 25	syl	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to X \in (I \cup \{X\})$
272	269 271	eqeltrd	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to x \in (I \cup \{X\})$
273	193	adantr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to r \in B$
274	180 268 272 273	fvmptd2	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) = r$
275	274 269	oveq12d	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x = X) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x = r \underset{˙}{\cdot} X$
276	2 198 194 195 275	gsumsnd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \underset{x \in \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x) = r \underset{˙}{\cdot} X$
277	276	eqcomd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to r \underset{˙}{\cdot} X = \underset{x \in \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
278	257 277	oveq12d	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to i \underset{˙}{+} (r \underset{˙}{\cdot} X) = (\underset{x \in I}{\sum_{R}}, ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (\underset{x \in \{X\}}{\sum_{R}}, ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x))$
279	197 278	eqtr3d	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (r \underset{˙}{\cdot} X) \underset{˙}{+} i = (\underset{x \in I}{\sum_{R}}, ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (\underset{x \in \{X\}}{\sum_{R}}, ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x))$
280		simpr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i$
281	5	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in (I \cup \{X\})) \to R \in Ring$
282	170	ffvelcdmda	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in (I \cup \{X\})) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \in B$
283	14	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in (I \cup \{X\})) \to I \cup \{X\} \subseteq B$
284		simpr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in (I \cup \{X\})) \to x \in (I \cup \{X\})$
285	283 284	sseldd	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in (I \cup \{X\})) \to x \in B$
286	2 4 281 282 285	ringcld	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in (I \cup \{X\})) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x \in B$
287	161	mptexd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x) \in V$
288		funmpt	$⊢ Fun (x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
289	288	a1i	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to Fun (x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
290	187	fsuppimpd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) supp \underset{˙}{0} \in Fin$
291		nfv	$⊢ Ⅎ y (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i)$
292	291 169 180	fnmptd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) Fn (I \cup \{X\})$
293	292	adantr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) Fn (I \cup \{X\})$
294	161	adantr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to I \cup \{X\} \in V$
295	186	adantr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to \underset{˙}{0} \in B$
296		simpr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))$
297	293 294 295 296	fvdifsupp	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) = \underset{˙}{0}$
298	297	oveq1d	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x = \underset{˙}{0} \underset{˙}{\cdot} x$
299	5	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to R \in Ring$
300	14	ad4antr	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to I \cup \{X\} \subseteq B$
301	296	eldifad	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to x \in (I \cup \{X\})$
302	300 301	sseldd	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to x \in B$
303	299 302 99	syl2anc	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to \underset{˙}{0} \underset{˙}{\cdot} x = \underset{˙}{0}$
304	298 303	eqtrd	$⊢ ((((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \land x \in ((I \cup \{X\}) ∖ {supp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))))) \to (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x = \underset{˙}{0}$
305	304 161	suppss2	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x) supp \underset{˙}{0} \subseteq (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) supp \underset{˙}{0}$
306	290 305	ssfid	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to (x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x) supp \underset{˙}{0} \in Fin$
307	287 186 289 306	isfsuppd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to {finSupp}_{\underset{˙}{0}} ((x \in (I \cup \{X\}) ⟼ (y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x))$
308	214 107	sylibr	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to I \cap \{X\} = \emptyset$
309		eqidd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to I \cup \{X\} = I \cup \{X\}$
310	2 3 6 188 161 286 307 308 309	gsumsplit2	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x) = (\underset{x \in I}{\sum_{R}}, ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)) \underset{˙}{+} (\underset{x \in \{X\}}{\sum_{R}}, ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x))$
311	279 280 310	3eqtr4d	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to A = \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x)$
312	187 311	jca	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to ({finSupp}_{\underset{˙}{0}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0}))) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} ((y \in (I \cup \{X\}) ⟼ if (y \in \{X, i\}, if (y = X, r, 1_{R}), \underset{˙}{0})) (x) \underset{˙}{\cdot} x))$
313	171 179 312	rspcedvd	$⊢ (((φ \land r \in B) \land i \in I) \land A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \exists a \in (B^{(I \cup \{X\})}) ({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x))$
314	313	r19.29ffa	$⊢ (φ \land \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i) \to \exists a \in (B^{(I \cup \{X\})}) ({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x))$
315	157 314	impbida	$⊢ φ \to (\exists a \in (B^{(I \cup \{X\})}) ({finSupp}_{\underset{˙}{0}} (a) \land A = \underset{x \in I \cup \{X\}}{\sum_{R}} (a (x) \underset{˙}{\cdot} x)) \leftrightarrow \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i)$
316	15 315	bitrd	$⊢ φ \to (A \in N (I \cup \{X\}) \leftrightarrow \exists r \in B \exists i \in I A = (r \underset{˙}{\cdot} X) \underset{˙}{+} i)$

Metamath Proof Explorer

Theorem elrspunsn

Proof