Theorem elrspunidl 34024

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

Hypotheses

Ref	Expression
elrspunidl.n	⊢ 𝑁 = (RSpan‘𝑅)
elrspunidl.b	⊢ 𝐵 = (Base‘𝑅)
elrspunidl.1	⊢ 0 = (0g‘𝑅)
elrspunidl.x	⊢ · = (.r‘𝑅)
elrspunidl.r	⊢ (𝜑 → 𝑅 ∈ Ring)
elrspunidl.i	⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅))

Assertion

Ref	Expression
elrspunidl	⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)))

Distinct variable groups:   0 ,𝑎,𝑘   · ,𝑎,𝑘   𝐵,𝑎,𝑘   𝑅,𝑎,𝑘   𝑆,𝑎,𝑘   𝑋,𝑎,𝑘   𝜑,𝑎,𝑘

Allowed substitution hints:   𝑁(𝑘, 𝑎)

Proof of Theorem elrspunidl

Dummy variables 𝑏 𝑓 𝑖 𝑗 𝑙 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elrspunidl.n	. . 3 ⊢ 𝑁 = (RSpan‘𝑅)
2		elrspunidl.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		elrspunidl.1	. . 3 ⊢ 0 = (0g‘𝑅)
4		elrspunidl.x	. . 3 ⊢ · = (.r‘𝑅)
5		elrspunidl.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
6		elrspunidl.i	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅))
7	6	sselda 3908	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8		eqid 2760	. . . . . . 7 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
9	2, 8	lidlss 21495	. . . . . 6 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
10	7, 9	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝑖 ⊆ 𝐵)
11	10	ralrimiva 3154	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑆 𝑖 ⊆ 𝐵)
12		unissb 4900	. . . 4 ⊢ (∪ 𝑆 ⊆ 𝐵 ↔ ∀𝑖 ∈ 𝑆 𝑖 ⊆ 𝐵)
13	11, 12	sylibr 237	. . 3 ⊢ (𝜑 → ∪ 𝑆 ⊆ 𝐵)
14	1, 2, 3, 4, 5, 13	elrsp 33973	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑏 ∈ (𝐵 ↑m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))))
15		fvexd 6900	. . . . . . . . . 10 ⊢ (𝜑 → (LIdeal‘𝑅) ∈ V)
16	15, 6	ssexd 5285	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
17	16	uniexd 7759	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
18		eluni2 4870	. . . . . . . . . 10 ⊢ (𝑗 ∈ ∪ 𝑆 ↔ ∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖)
19	18	bilani 510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑆) → ∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖)
20	19	ralrimiva 3154	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ ∪ 𝑆∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖)
21		eleq2 2849	. . . . . . . . 9 ⊢ (𝑖 = (𝑓‘𝑗) → (𝑗 ∈ 𝑖 ↔ 𝑗 ∈ (𝑓‘𝑗)))
22	21	ac6 10561	. . . . . . . 8 ⊢ ((∪ 𝑆 ∈ V ∧ 𝑆 ∈ V ∧ ∀𝑗 ∈ ∪ 𝑆∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖) → ∃𝑓(𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)))
23	17, 16, 20, 22	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)))
24	23	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) → ∃𝑓(𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)))
25		breq1 5105	. . . . . . . . 9 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) finSupp 0 ))
26		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))))
27	26	eqeq2d 2771	. . . . . . . . 9 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σg 𝑎) ↔ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))))))
28		fveq1 6884	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑎‘𝑘) = ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘))
29	28	eleq1d 2845	. . . . . . . . . 10 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → ((𝑎‘𝑘) ∈ 𝑘 ↔ ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
30	29	ralbidv 3185	. . . . . . . . 9 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
31	25, 27, 30	3anbi123d 1464	. . . . . . . 8 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → ((𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ↔ ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))) ∧ ∀𝑘 ∈ 𝑆 ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
32		simp-5l 797	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝜑)
33	32	adantr 486	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → 𝜑)
34		ringcmn 20516	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
35	33, 5, 34	3syl 19	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → 𝑅 ∈ CMnd)
36		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
37	36	cnvex 7937	. . . . . . . . . . . . 13 ⊢ ◡𝑓 ∈ V
38	37	imaex 7926	. . . . . . . . . . . 12 ⊢ (◡𝑓 “ {𝑖}) ∈ V
39	38	a1i 11	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (◡𝑓 “ {𝑖}) ∈ V)
40	5	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
41		elmapi 8872	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝐵 ↑m ∪ 𝑆) → 𝑏:∪ 𝑆⟶𝐵)
42	41	ad7antlr 752	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → 𝑏:∪ 𝑆⟶𝐵)
43		cnvimass 6198	. . . . . . . . . . . . . . . . 17 ⊢ (◡𝑓 “ {𝑖}) ⊆ dom 𝑓
44		fdm 6719	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:∪ 𝑆⟶𝑆 → dom 𝑓 = ∪ 𝑆)
45	43, 44	sseqtrid 3950	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:∪ 𝑆⟶𝑆 → (◡𝑓 “ {𝑖}) ⊆ ∪ 𝑆)
46	45	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (◡𝑓 “ {𝑖}) ⊆ ∪ 𝑆)
47	46	sselda 3908	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → 𝑙 ∈ ∪ 𝑆)
48	42, 47	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → (𝑏‘𝑙) ∈ 𝐵)
49	13	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → ∪ 𝑆 ⊆ 𝐵)
50	49, 47	sseldd 3909	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → 𝑙 ∈ 𝐵)
51	2, 4, 40, 48, 50	ringcld 20489	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑖})) → ((𝑏‘𝑙) · 𝑙) ∈ 𝐵)
52		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑙 → (𝑏‘𝑗) = (𝑏‘𝑙))
53		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑙 → 𝑗 = 𝑙)
54	52, 53	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑙 → ((𝑏‘𝑗) · 𝑗) = ((𝑏‘𝑙) · 𝑙))
55	54	cbvmptv 5208	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑙 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑙) · 𝑙))
56	51, 55	fmptd 7114	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)):(◡𝑓 “ {𝑖})⟶𝐵)
57	39	mptexd 7230	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V)
58	56	ffund 6714	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → Fun (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))
59		simp-5r 798	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → 𝑏 finSupp 0 )
60		nfv 1946	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 )
61		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝑅
62		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 Σg
63		nfmpt1 5203	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))
64	61, 62, 63	nfov 7450	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))
65	64	nfeq2 2939	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))
66	60, 65	nfan 1931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗(((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))
67		nfv 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑓:∪ 𝑆⟶𝑆
68	66, 67	nfan 1931	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆)
69		nfra1 3286	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)
70	68, 69	nfan 1931	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗))
71		nfv 1946	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗 𝑖 ∈ 𝑆
72	70, 71	nfan 1931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆)
73		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(◡𝑓 “ {𝑖})
74		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝑏 supp 0 )
75	41	ad7antlr 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏:∪ 𝑆⟶𝐵)
76	75	ffnd 6710	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn ∪ 𝑆)
77	32, 17	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∪ 𝑆 ∈ V)
78	77	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ∈ V)
79	3	fvexi 6899	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
80	79	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
81	46	ssdifd 4081	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ (∪ 𝑆 ∖ (𝑏 supp 0 )))
82	81	sselda 3908	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
83	76, 78, 80, 82	fvdifsupp 8191	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
84	83	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = ( 0 · 𝑗))
85	5	ad7antr 751	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
86	13	ad7antr 751	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ⊆ 𝐵)
87	82	eldifad 4051	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ∪ 𝑆)
88	86, 87	sseldd 3909	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ 𝐵)
89	2, 4, 3	ringlz 20529	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ 𝐵) → ( 0 · 𝑗) = 0 )
90	85, 88, 89	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
91	84, 90	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = 0 )
92	72, 73, 74, 91, 39	suppss2f 33279	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → ((𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
93		fsuppsssupp 9376	. . . . . . . . . . . 12 ⊢ ((((𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) finSupp 0 )
94	57, 58, 59, 92, 93	syl22anc 852	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) finSupp 0 )
95	2, 3, 35, 39, 56, 94	gsumcl 20134	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) ∈ 𝐵)
96	95	fmpttd 7115	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))):𝑆⟶𝐵)
97	2	fvexi 6899	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
98	97	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ V)
99	98, 16	elmapd 8863	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) ∈ (𝐵 ↑m 𝑆) ↔ (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))):𝑆⟶𝐵))
100	99	biimpar 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))):𝑆⟶𝐵) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) ∈ (𝐵 ↑m 𝑆))
101	32, 96, 100	syl2anc 596	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) ∈ (𝐵 ↑m 𝑆))
102	32, 16	syl 18	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑆 ∈ V)
103	102	mptexd 7230	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) ∈ V)
104	79	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 0 ∈ V)
105		funmpt 6578	. . . . . . . . . . 11 ⊢ Fun (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))
106	105	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Fun (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))))
107		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑓:∪ 𝑆⟶𝑆)
108	107	ffund 6714	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Fun 𝑓)
109		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑏 finSupp 0 )
110	109	fsuppimpd 9364	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑏 supp 0 ) ∈ Fin)
111		imafi 9310	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
112	108, 110, 111	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
113		nfv 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
114	70, 113	nfan 1931	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
115		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓:∪ 𝑆⟶𝑆)
116	115	ffund 6714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
117		snssi 4742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
118	117	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
119		sspreima 7067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ {𝑖}) ⊆ (◡𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
120	116, 118, 119	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ {𝑖}) ⊆ (◡𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
121		difpreima 7064	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝑓 → (◡𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((◡𝑓 “ 𝑆) ∖ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
122	116, 121	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((◡𝑓 “ 𝑆) ∖ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
123	120, 122	sseqtrd 3944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ {𝑖}) ⊆ ((◡𝑓 “ 𝑆) ∖ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
124		suppssdm 8197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 supp 0 ) ⊆ dom 𝑏
125	41	ad6antlr 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏:∪ 𝑆⟶𝐵)
126	124, 125	fssdm 6729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ ∪ 𝑆)
127	115	fdmd 6720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = ∪ 𝑆)
128	126, 127	sseqtrrd 3945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
129		sseqin2 4120	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
130	129	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
131		dminss 6142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))
132	130, 131	eqsstrrdi 3953	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 supp 0 ) ⊆ dom 𝑓 → (𝑏 supp 0 ) ⊆ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
133	128, 132	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
134	133	sscond 4082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((◡𝑓 “ 𝑆) ∖ (◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((◡𝑓 “ 𝑆) ∖ (𝑏 supp 0 )))
135	123, 134	sstrd 3918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ {𝑖}) ⊆ ((◡𝑓 “ 𝑆) ∖ (𝑏 supp 0 )))
136		fimacnv 6732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:∪ 𝑆⟶𝑆 → (◡𝑓 “ 𝑆) = ∪ 𝑆)
137	115, 136	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ 𝑆) = ∪ 𝑆)
138	137	difeq1d 4062	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((◡𝑓 “ 𝑆) ∖ (𝑏 supp 0 )) = (∪ 𝑆 ∖ (𝑏 supp 0 )))
139	135, 138	sseqtrd 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ {𝑖}) ⊆ (∪ 𝑆 ∖ (𝑏 supp 0 )))
140	139	sselda 3908	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
141		ssidd 3931	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑏 supp 0 ))
142	77	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ∪ 𝑆 ∈ V)
143	79	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 0 ∈ V)
144	125, 141, 142, 143	suppssr 8215	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
145	140, 144	syldan 603	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → (𝑏‘𝑗) = 0 )
146	145	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → ((𝑏‘𝑗) · 𝑗) = ( 0 · 𝑗))
147	5	ad7antr 751	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
148	13	ad7antr 751	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → ∪ 𝑆 ⊆ 𝐵)
149	45	ad3antlr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (◡𝑓 “ {𝑖}) ⊆ ∪ 𝑆)
150	149	sselda 3908	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → 𝑗 ∈ ∪ 𝑆)
151	148, 150	sseldd 3909	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → 𝑗 ∈ 𝐵)
152	147, 151, 89	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → ( 0 · 𝑗) = 0 )
153	146, 152	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (◡𝑓 “ {𝑖})) → ((𝑏‘𝑗) · 𝑗) = 0 )
154	114, 153	mpteq2da 5196	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ 0 ))
155	154	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ 0 )))
156	5	ringcmnd 20518	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ CMnd)
157	156	cmnmndd 20023	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ Mnd)
158	157	ad6antr 749	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
159	3	gsumz 19037	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Mnd ∧ (◡𝑓 “ {𝑖}) ∈ V) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ 0 )) = 0 )
160	158, 38, 159	sylancl 598	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ 0 )) = 0 )
161	155, 160	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) = 0 )
162	161, 102	suppss2 8220	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
163	112, 162	ssfid 9263	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
164	103, 104, 106, 163	isfsuppd 9361	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) finSupp 0 )
165		simpllr 788	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))
166	32, 156	syl 18	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑅 ∈ CMnd)
167	5	ad6antr 749	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → 𝑅 ∈ Ring)
168	41	ad5antlr 748	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑏:∪ 𝑆⟶𝐵)
169	168	ffvelcdmda 7084	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → (𝑏‘𝑗) ∈ 𝐵)
170	32, 13	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∪ 𝑆 ⊆ 𝐵)
171	170	sselda 3908	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → 𝑗 ∈ 𝐵)
172	2, 4, 167, 169, 171	ringcld 20489	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → ((𝑏‘𝑗) · 𝑗) ∈ 𝐵)
173		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))
174	70, 172, 173	fmptdf 7117	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)):∪ 𝑆⟶𝐵)
175	77	mptexd 7230	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V)
176		funmpt 6578	. . . . . . . . . . . . 13 ⊢ Fun (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))
177	176	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Fun (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))
178		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∪ 𝑆
179	168	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏:∪ 𝑆⟶𝐵)
180	179	ffnd 6710	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏 Fn ∪ 𝑆)
181	77	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ∈ V)
182	79	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 0 ∈ V)
183		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
184	180, 181, 182, 183	fvdifsupp 8191	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
185	184	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = ( 0 · 𝑗))
186	5	ad6antr 749	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
187	170	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ⊆ 𝐵)
188	183	eldifad 4051	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ∪ 𝑆)
189	187, 188	sseldd 3909	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ 𝐵)
190	186, 189, 89	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
191	185, 190	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = 0 )
192	70, 178, 74, 191, 77	suppss2f 33279	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
193		fsuppsssupp 9376	. . . . . . . . . . . 12 ⊢ ((((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) finSupp 0 )
194	175, 177, 109, 192, 193	syl22anc 852	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) finSupp 0 )
195		sndisj 5094	. . . . . . . . . . . 12 ⊢ Disj 𝑖 ∈ 𝑆 {𝑖}
196		disjpreima 33225	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ Disj 𝑖 ∈ 𝑆 {𝑖}) → Disj 𝑖 ∈ 𝑆 (◡𝑓 “ {𝑖}))
197	108, 195, 196	sylancl 598	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Disj 𝑖 ∈ 𝑆 (◡𝑓 “ {𝑖}))
198		iunid 5018	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ 𝑆 {𝑖} = 𝑆
199	198	imaeq2i 6049	. . . . . . . . . . . 12 ⊢ (◡𝑓 “ ∪ 𝑖 ∈ 𝑆 {𝑖}) = (◡𝑓 “ 𝑆)
200		iunpreima 7068	. . . . . . . . . . . . 13 ⊢ (Fun 𝑓 → (◡𝑓 “ ∪ 𝑖 ∈ 𝑆 {𝑖}) = ∪ 𝑖 ∈ 𝑆 (◡𝑓 “ {𝑖}))
201	108, 200	syl 18	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (◡𝑓 “ ∪ 𝑖 ∈ 𝑆 {𝑖}) = ∪ 𝑖 ∈ 𝑆 (◡𝑓 “ {𝑖}))
202	136	ad2antlr 740	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (◡𝑓 “ 𝑆) = ∪ 𝑆)
203	199, 201, 202	3eqtr3a 2819	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∪ 𝑖 ∈ 𝑆 (◡𝑓 “ {𝑖}) = ∪ 𝑆)
204	2, 3, 166, 77, 102, 174, 194, 197, 203	gsumpart 33670	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (◡𝑓 “ {𝑖}))))))
205	46	resmptd 6031	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (◡𝑓 “ {𝑖})) = (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))
206	205	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑅 Σg ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (◡𝑓 “ {𝑖}))) = (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))
207	206	mpteq2dva 5197	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σg ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (◡𝑓 “ {𝑖})))) = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))))
208	207	oveq2d 7436	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (◡𝑓 “ {𝑖}))))) = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))))
209	165, 204, 208	3eqtrd 2799	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑋 = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))))
210		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) = (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))
211		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
212	211	sneqd 4592	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
213	212	imaeq2d 6051	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → (◡𝑓 “ {𝑖}) = (◡𝑓 “ {𝑘}))
214	213	mpteq1d 5194	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)))
215	214	oveq2d 7436	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))))
216		simpr 490	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆)
217		ovexd 7455	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))) ∈ V)
218	210, 215, 216, 217	fvmptd2 7002	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) = (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))))
219	156	ad6antr 749	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑅 ∈ CMnd)
220	37	imaex 7926	. . . . . . . . . . . . 13 ⊢ (◡𝑓 “ {𝑘}) ∈ V
221	220	a1i 11	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (◡𝑓 “ {𝑘}) ∈ V)
222	5	ad6antr 749	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑅 ∈ Ring)
223	32, 6	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑆 ⊆ (LIdeal‘𝑅))
224	223	sselda 3908	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
225	8	lidlsubg 21507	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
226		subgsubm 19364	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (SubGrp‘𝑅) → 𝑘 ∈ (SubMnd‘𝑅))
227	225, 226	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubMnd‘𝑅))
228	222, 224, 227	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (SubMnd‘𝑅))
229	222	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑅 ∈ Ring)
230	224	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑘 ∈ (LIdeal‘𝑅))
231	41	ad7antlr 752	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑏:∪ 𝑆⟶𝐵)
232		cnvimass 6198	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑓 “ {𝑘}) ⊆ dom 𝑓
233	232, 44	sseqtrid 3950	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:∪ 𝑆⟶𝑆 → (◡𝑓 “ {𝑘}) ⊆ ∪ 𝑆)
234	233	ad3antlr 744	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (◡𝑓 “ {𝑘}) ⊆ ∪ 𝑆)
235	234	sselda 3908	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑙 ∈ ∪ 𝑆)
236	231, 235	ffvelcdmd 7085	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → (𝑏‘𝑙) ∈ 𝐵)
237		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑙 → (𝑓‘𝑗) = (𝑓‘𝑙))
238	53, 237	eleq12d 2854	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑙 → (𝑗 ∈ (𝑓‘𝑗) ↔ 𝑙 ∈ (𝑓‘𝑙)))
239		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗))
240	238, 239, 235	rspcdva 3577	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓‘𝑙))
241		simp-4r 796	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑓:∪ 𝑆⟶𝑆)
242	241	ffnd 6710	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑓 Fn ∪ 𝑆)
243		elpreima 7057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 Fn ∪ 𝑆 → (𝑙 ∈ (◡𝑓 “ {𝑘}) ↔ (𝑙 ∈ ∪ 𝑆 ∧ (𝑓‘𝑙) ∈ {𝑘})))
244	243	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 Fn ∪ 𝑆 ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → (𝑙 ∈ ∪ 𝑆 ∧ (𝑓‘𝑙) ∈ {𝑘}))
245		elsni 4597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓‘𝑙) ∈ {𝑘} → (𝑓‘𝑙) = 𝑘)
246	244, 245	simpl2im 513	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 Fn ∪ 𝑆 ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → (𝑓‘𝑙) = 𝑘)
247	242, 246	sylancom 600	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → (𝑓‘𝑙) = 𝑘)
248	240, 247	eleqtrd 2862	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → 𝑙 ∈ 𝑘)
249	8, 2, 4, 229, 230, 236, 248	lidlmcld 21511	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (◡𝑓 “ {𝑘})) → ((𝑏‘𝑙) · 𝑙) ∈ 𝑘)
250	54	cbvmptv 5208	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑙 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑙) · 𝑙))
251	249, 250	fmptd 7114	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)):(◡𝑓 “ {𝑘})⟶𝑘)
252	221	mptexd 7230	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V)
253	251	ffund 6714	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → Fun (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)))
254		simp-5r 798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑏 finSupp 0 )
255		nfv 1946	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗 𝑘 ∈ 𝑆
256	70, 255	nfan 1931	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆)
257		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(◡𝑓 “ {𝑘})
258	41	ad7antlr 752	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏:∪ 𝑆⟶𝐵)
259	258	ffnd 6710	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn ∪ 𝑆)
260	77	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ∈ V)
261	79	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
262	234	ssdifd 4081	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ (∪ 𝑆 ∖ (𝑏 supp 0 )))
263	262	sselda 3908	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
264	259, 260, 261, 263	fvdifsupp 8191	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
265	264	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = ( 0 · 𝑗))
266	13	ad7antr 751	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ⊆ 𝐵)
267	263	eldifad 4051	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ∪ 𝑆)
268	266, 267	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ 𝐵)
269	222, 268, 89	syl2an2r 698	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
270	265, 269	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = 0 )
271	256, 257, 74, 270, 221	suppss2f 33279	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
272		fsuppsssupp 9376	. . . . . . . . . . . . 13 ⊢ ((((𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) finSupp 0 )
273	252, 253, 254, 271, 272	syl22anc 852	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) finSupp 0 )
274	3, 219, 221, 228, 251, 273	gsumsubmcl 20138	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))) ∈ 𝑘)
275	218, 274	eqeltrd 2860	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
276	275	ralrimiva 3154	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∀𝑘 ∈ 𝑆 ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
277	164, 209, 276	3jca 1146	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))) ∧ ∀𝑘 ∈ 𝑆 ((𝑖 ∈ 𝑆 ↦ (𝑅 Σg (𝑗 ∈ (◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
278	31, 101, 277	rspcedvdw 3579	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))
279	278	anasss 472	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ (𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗))) → ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))
280	24, 279	exlimddv 1967	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) → ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))
281	280	anasss 472	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (𝐵 ↑m ∪ 𝑆)) ∧ (𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))
282	281	r19.29an 3166	. . 3 ⊢ ((𝜑 ∧ ∃𝑏 ∈ (𝐵 ↑m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))
283		breq1 5105	. . . . . . 7 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
284		fveq1 6884	. . . . . . . . . . 11 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏‘𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
285	284	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏‘𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
286	285	mpteq2dv 5198	. . . . . . . . 9 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
287	286	oveq2d 7436	. . . . . . . 8 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
288	287	eqeq2d 2771	. . . . . . 7 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))) ↔ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
289	283, 288	anbi12d 644	. . . . . 6 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ↔ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))))
290	97	a1i 11	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝐵 ∈ V)
291	17	ad4antr 745	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∪ 𝑆 ∈ V)
292	98, 16	elmapd 8863	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑎 ∈ (𝐵 ↑m 𝑆) ↔ 𝑎:𝑆⟶𝐵))
293	292	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) → 𝑎:𝑆⟶𝐵)
294	293	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑎:𝑆⟶𝐵)
295	294	ffnd 6710	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
296		elssuni 4898	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
297	296	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
298	297	sseld 3907	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘 ∈ 𝑆) → ((𝑎‘𝑘) ∈ 𝑘 → (𝑎‘𝑘) ∈ ∪ 𝑆))
299	298	ralimdva 3174	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) → (∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘 → ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ ∪ 𝑆))
300	299	imp 412	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ ∪ 𝑆)
301		fnfvrnss 7121	. . . . . . . . . . 11 ⊢ ((𝑎 Fn 𝑆 ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ ∪ 𝑆) → ran 𝑎 ⊆ ∪ 𝑆)
302	295, 300, 301	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ran 𝑎 ⊆ ∪ 𝑆)
303	302	ssdifssd 4083	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ ∪ 𝑆)
304		undif 4437	. . . . . . . . 9 ⊢ ((ran 𝑎 ∖ { 0 }) ⊆ ∪ 𝑆 ↔ ((ran 𝑎 ∖ { 0 }) ∪ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∪ 𝑆)
305	303, 304	sylib 221	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∪ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∪ 𝑆)
306	5	ad4antr 745	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑅 ∈ Ring)
307	306	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
308		eqid 2760	. . . . . . . . . . . . 13 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
309	308	zrhrhm 21822	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
310		zringbas 21764	. . . . . . . . . . . . 13 ⊢ ℤ = (Base‘ℤring)
311	310, 2	rhmf 20720	. . . . . . . . . . . 12 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
312	307, 309, 311	3syl 19	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (ℤRHom‘𝑅):ℤ⟶𝐵)
313		simp-5r 798	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵 ↑m 𝑆))
314	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
315		ssv 3932	. . . . . . . . . . . . . . . . 17 ⊢ ran 𝑎 ⊆ V
316		ssdif 4080	. . . . . . . . . . . . . . . . 17 ⊢ (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
317	315, 316	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
318	317	sseli 3904	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (ran 𝑎 ∖ { 0 }) → 𝑚 ∈ (V ∖ { 0 }))
319	318	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑚 ∈ (V ∖ { 0 }))
320		simp-4r 796	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
321	313, 314, 319, 320	fsuppinisegfi 33327	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (◡𝑎 “ {𝑚}) ∈ Fin)
322		hashcl 14503	. . . . . . . . . . . . 13 ⊢ ((◡𝑎 “ {𝑚}) ∈ Fin → (♯‘(◡𝑎 “ {𝑚})) ∈ ℕ0)
323	321, 322	syl 18	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(◡𝑎 “ {𝑚})) ∈ ℕ0)
324	323	nn0zd 12721	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(◡𝑎 “ {𝑚})) ∈ ℤ)
325	312, 324	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚}))) ∈ 𝐵)
326		eqid 2760	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚}))))
327	325, 326	fmptd 7114	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
328	2, 3	ring0cl 20501	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵)
329		fconst6g 6771	. . . . . . . . . 10 ⊢ ( 0 ∈ 𝐵 → ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):(∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
330	306, 328, 329	3syl 19	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):(∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
331		disjdif 4425	. . . . . . . . . 10 ⊢ ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
332	331	a1i 11	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
333	327, 330, 332	fun2d 6746	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
334	305, 333	feq2dd 6695	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):∪ 𝑆⟶𝐵)
335	290, 291, 334	elmapdd 8864	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵 ↑m ∪ 𝑆))
336	79	a1i 11	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 0 ∈ V)
337	333	ffund 6714	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })))
338	294	ffund 6714	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → Fun 𝑎)
339		simp-4r 796	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑎 ∈ (𝐵 ↑m 𝑆))
340		simpllr 788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑎 finSupp 0 )
341		fsupprnfi 33332	. . . . . . . . . . . 12 ⊢ (((Fun 𝑎 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
342		diffi 9193	. . . . . . . . . . . 12 ⊢ (ran 𝑎 ∈ Fin → (ran 𝑎 ∖ { 0 }) ∈ Fin)
343	341, 342	syl 18	. . . . . . . . . . 11 ⊢ (((Fun 𝑎 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
344	338, 339, 336, 340, 343	syl22anc 852	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
345	327, 344, 336	fdmfifsupp 9370	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) finSupp 0 )
346	13	ssdifssd 4083	. . . . . . . . . . . 12 ⊢ (𝜑 → (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
347	346	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
348	290, 347	ssexd 5285	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
349	348, 336	fczfsuppd 9381	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
350	345, 349	fsuppun 9382	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
351	335, 336, 337, 350	isfsuppd 9361	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
352		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚}))) ∈ V
353	352, 326	fnmpti 6682	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 })
354	353	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }))
355		fnconstg 6770	. . . . . . . . . . . . . . 15 ⊢ ( 0 ∈ V → ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })))
356	79, 355	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))
357	356	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })))
358	331	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
359		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (ran 𝑎 ∖ { 0 }))
360	354, 357, 358, 359	fvun1d 6978	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚}))))‘𝑗))
361		sneq 4590	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → {𝑚} = {𝑗})
362	361	imaeq2d 6051	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → (◡𝑎 “ {𝑚}) = (◡𝑎 “ {𝑗}))
363	362	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (♯‘(◡𝑎 “ {𝑚})) = (♯‘(◡𝑎 “ {𝑗})))
364	363	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))))
365		fvexd 6900	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) ∈ V)
366	326, 364, 359, 365	fvmptd3 7017	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))))
367	360, 366	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))))
368	367	oveq1d 7435	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗))
369	368	mpteq2dva 5197	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗)))
370	369	oveq2d 7436	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗))))
371	306	ringcmnd 20518	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑅 ∈ CMnd)
372	331	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
373		fvun2 6977	. . . . . . . . . . . . . 14 ⊢ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }) ∧ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∧ (((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅ ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = (((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
374	353, 356, 373	mp3an12 1480	. . . . . . . . . . . . 13 ⊢ ((((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅ ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = (((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
375	372, 374	sylancom 600	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = (((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
376	79	fvconst2 7210	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) → (((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
377	376	adantl 487	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
378	375, 377	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
379	378	oveq1d 7435	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
380	347	sselda 3908	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → 𝑗 ∈ 𝐵)
381	306, 380, 89	syl2an2r 698	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ( 0 · 𝑗) = 0 )
382	379, 381	eqtrd 2795	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = 0 )
383	306	adantr 486	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → 𝑅 ∈ Ring)
384	334	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
385	13	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∪ 𝑆 ⊆ 𝐵)
386	385	sselda 3908	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → 𝑗 ∈ 𝐵)
387	2, 4, 383, 384, 386	ringcld 20489	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
388	2, 3, 371, 291, 382, 344, 387, 303	gsummptres2 33660	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
389		eqid 2760	. . . . . . . . . 10 ⊢ (.g‘𝑅) = (.g‘𝑅)
390	2, 3, 389, 371, 294, 340	gsumhashmul 33674	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)𝑗))))
391		simplr 781	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg 𝑎))
392	306	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
393	339	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵 ↑m 𝑆))
394	79	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
395	317, 359	sselid 3906	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (V ∖ { 0 }))
396		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
397	393, 394, 395, 396	fsuppinisegfi 33327	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (◡𝑎 “ {𝑗}) ∈ Fin)
398		hashcl 14503	. . . . . . . . . . . . . 14 ⊢ ((◡𝑎 “ {𝑗}) ∈ Fin → (♯‘(◡𝑎 “ {𝑗})) ∈ ℕ0)
399	397, 398	syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(◡𝑎 “ {𝑗})) ∈ ℕ0)
400	399	nn0zd 12721	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ)
401	303, 385	sstrd 3918	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
402	401	sselda 3908	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ 𝐵)
403		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑅) = (1r‘𝑅)
404	308, 389, 403	zrhmulg 21820	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)(1r‘𝑅)))
405	404	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)(1r‘𝑅)))
406	405	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)(1r‘𝑅)) · 𝑗))
407		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → 𝑅 ∈ Ring)
408		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ)
409	2, 403	ringidcl 20499	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ 𝐵)
410	409	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (1r‘𝑅) ∈ 𝐵)
411		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → 𝑗 ∈ 𝐵)
412	2, 389, 4	mulgass2 20545	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ ((♯‘(◡𝑎 “ {𝑗})) ∈ ℤ ∧ (1r‘𝑅) ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)(1r‘𝑅)) · 𝑗) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)((1r‘𝑅) · 𝑗)))
413	407, 408, 410, 411, 412	syl13anc 1399	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)(1r‘𝑅)) · 𝑗) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)((1r‘𝑅) · 𝑗)))
414	2, 4, 403	ringlidm 20503	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ 𝐵) → ((1r‘𝑅) · 𝑗) = 𝑗)
415	407, 414	sylancom 600	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → ((1r‘𝑅) · 𝑗) = 𝑗)
416	415	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)((1r‘𝑅) · 𝑗)) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)𝑗))
417	406, 413, 416	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)𝑗))
418	392, 400, 402, 417	syl21anc 851	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)𝑗))
419	418	mpteq2dva 5197	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)𝑗)))
420	419	oveq2d 7436	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(◡𝑎 “ {𝑗}))(.g‘𝑅)𝑗))))
421	390, 391, 420	3eqtr4d 2805	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑗}))) · 𝑗))))
422	370, 388, 421	3eqtr4rd 2806	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
423	351, 422	jca 521	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
424	289, 335, 423	rspcedvdw 3579	. . . . 5 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵 ↑m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))))
425	424	3anasss 1380	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑m 𝑆)) ∧ (𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵 ↑m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))))
426	425	r19.29an 3166	. . 3 ⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵 ↑m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))))
427	282, 426	impbida 813	. 2 ⊢ (𝜑 → (∃𝑏 ∈ (𝐵 ↑m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)))
428	14, 427	bitrd 282	1 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045   ∩ cin 4089   ∪ cun 4149  ∅c0 4278  {csn 4584  ∪ cuni 4866  ∪ ciun 4950  Disj wdisj 5069   class class class wbr 5102   ↦ cmpt 5185   × cxp 5648  ^◡ccnv 5649  dom cdm 5650  ran crn 5651   ↾ cres 5652   “ cima 5653  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   supp csupp 8179   ↑_m cmap 8850  Fincfn 8976   finSupp cfsupp 9356  ℕ₀cn0 12609  ℤcz 12696  ♯chash 14477  Basecbs 17392  ._rcmulr 17434  0_gc0g 17615   Σ_g cgsu 17616  Mndcmnd 18928  SubMndcsubmnd 18982  ._gcmg 19282  SubGrpcsubg 19335  CMndccmn 19999  1_rcur 20412  Ringcrg 20464   RingHom crh 20704  LIdealclidl 21489  RSpancrsp 21490  ℤ_ringczring 21757  ℤRHomczrh 21810

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-ac2 10544  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280  ax-addf 11282  ax-mulf 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-disj 5070  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8180  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-2o 8480  df-er 8720  df-map 8852  df-ixp 8929  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-fsupp 9357  df-sup 9437  df-oi 9507  df-card 10023  df-ac 10198  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-nn 12339  df-2 12408  df-3 12409  df-4 12410  df-5 12411  df-6 12412  df-7 12413  df-8 12414  df-9 12415  df-n0 12610  df-z 12697  df-dec 12818  df-uz 12969  df-fz 13643  df-fzo 13792  df-seq 14148  df-hash 14478  df-struct 17330  df-sets 17347  df-slot 17365  df-ndx 17377  df-base 17393  df-ress 17414  df-plusg 17446  df-mulr 17447  df-starv 17448  df-sca 17449  df-vsca 17450  df-ip 17451  df-tset 17452  df-ple 17453  df-ds 17455  df-unif 17456  df-hom 17457  df-cco 17458  df-0g 17617  df-gsum 17618  df-prds 17623  df-pws 17625  df-mre 17761  df-mrc 17762  df-acs 17764  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-mhm 18983  df-submnd 18984  df-grp 19152  df-minusg 19153  df-sbg 19154  df-mulg 19283  df-subg 19338  df-ghm 19433  df-cntz 19536  df-cmn 20001  df-abl 20002  df-mgp 20366  df-rng 20380  df-ur 20413  df-ring 20466  df-cring 20467  df-rhm 20707  df-nzr 20768  df-subrng 20803  df-subrg 20827  df-lmod 21142  df-lss 21212  df-lsp 21252  df-lmhm 21302  df-lbs 21355  df-sra 21453  df-rgmod 21454  df-lidl 21491  df-rsp 21492  df-cnfld 21684  df-zring 21758  df-zrh 21814  df-dsmm 22043  df-frlm 22058  df-uvc 22094

This theorem is used by:  zarcmplem  34559