elrspunidl - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elrspunidl		Structured version Visualization version GIF version

Theorem elrspunidl 34062

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

**Hypotheses**
Ref	Expression
elrspunidl.n	⊢ 𝑁 = (RSpan‘𝑅)
elrspunidl.b	⊢ 𝐵 = (Base‘𝑅)
elrspunidl.1	⊢ 0 = (0_g‘𝑅)
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 = (0_g‘𝑅)
4		elrspunidl.x	. . 3 ⊢ · = (._r‘𝑅)
5		elrspunidl.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ Ring)
6		elrspunidl.i	. . . . . . 7 ⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅))
7	6	sselda 3913	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8		eqid 2763	. . . . . . 7 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
9	2, 8	lidlss 21523	. . . . . 6 ⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵)
10	7, 9	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑆) → 𝑖 ⊆ 𝐵)
11	10	ralrimiva 3158	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ 𝑆 𝑖 ⊆ 𝐵)
12		unissb 4904	. . . 4 ⊢ (∪ 𝑆 ⊆ 𝐵 ↔ ∀𝑖 ∈ 𝑆 𝑖 ⊆ 𝐵)
13	11, 12	sylibr 237	. . 3 ⊢ (𝜑 → ∪ 𝑆 ⊆ 𝐵)
14	1, 2, 3, 4, 5, 13	elrsp 34011	. 2 ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))))
15		fvexd 6926	. . . . . . . . . 10 ⊢ (𝜑 → (LIdeal‘𝑅) ∈ V)
16	15, 6	ssexd 5291	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ V)
17	16	uniexd 7786	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑆 ∈ V)
18		eluni2 4874	. . . . . . . . . 10 ⊢ (𝑗 ∈ ∪ 𝑆 ↔ ∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖)
19	18	bilani 510	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑆) → ∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖)
20	19	ralrimiva 3158	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ ∪ 𝑆∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖)
21		eleq2 2853	. . . . . . . . 9 ⊢ (𝑖 = (𝑓‘𝑗) → (𝑗 ∈ 𝑖 ↔ 𝑗 ∈ (𝑓‘𝑗)))
22	21	ac6 10588	. . . . . . . 8 ⊢ ((∪ 𝑆 ∈ V ∧ 𝑆 ∈ V ∧ ∀𝑗 ∈ ∪ 𝑆∃𝑖 ∈ 𝑆 𝑗 ∈ 𝑖) → ∃𝑓(𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)))
23	17, 16, 20, 22	syl3anc 1399	. . . . . . 7 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)))
24	23	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) → ∃𝑓(𝑓:∪ 𝑆⟶𝑆 ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)))
25		breq1 5109	. . . . . . . . 9 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) finSupp 0 ))
26		oveq2 7454	. . . . . . . . . 10 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑅 Σ_g 𝑎) = (𝑅 Σ_g (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))))
27	26	eqeq2d 2774	. . . . . . . . 9 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σ_g 𝑎) ↔ 𝑋 = (𝑅 Σ_g (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))))))
28		fveq1 6910	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (𝑎‘𝑘) = ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘))
29	28	eleq1d 2849	. . . . . . . . . 10 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → ((𝑎‘𝑘) ∈ 𝑘 ↔ ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
30	29	ralbidv 3189	. . . . . . . . 9 ⊢ (𝑎 = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) → (∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘 ↔ ∀𝑘 ∈ 𝑆 ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
31	25, 27, 30	3anbi123d 1465	. . . . . . . 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 20544	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
35	33, 5, 34	3syl 19	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → 𝑅 ∈ CMnd)
36		vex 3458	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
37	36	cnvex 7964	. . . . . . . . . . . . 13 ⊢ ^◡𝑓 ∈ V
38	37	imaex 7953	. . . . . . . . . . . 12 ⊢ (^◡𝑓 “ {𝑖}) ∈ V
39	38	a1i 11	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (^◡𝑓 “ {𝑖}) ∈ V)
40	5	ad7antr 751	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
41		elmapi 8900	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝐵 ↑_m ∪ 𝑆) → 𝑏:∪ 𝑆⟶𝐵)
42	41	ad7antlr 752	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → 𝑏:∪ 𝑆⟶𝐵)
43		cnvimass 6212	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝑓 “ {𝑖}) ⊆ dom 𝑓
44		fdm 6744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:∪ 𝑆⟶𝑆 → dom 𝑓 = ∪ 𝑆)
45	43, 44	sseqtrid 3955	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:∪ 𝑆⟶𝑆 → (^◡𝑓 “ {𝑖}) ⊆ ∪ 𝑆)
46	45	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (^◡𝑓 “ {𝑖}) ⊆ ∪ 𝑆)
47	46	sselda 3913	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → 𝑙 ∈ ∪ 𝑆)
48	42, 47	ffvelcdmd 7112	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → (𝑏‘𝑙) ∈ 𝐵)
49	13	ad7antr 751	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → ∪ 𝑆 ⊆ 𝐵)
50	49, 47	sseldd 3914	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → 𝑙 ∈ 𝐵)
51	2, 4, 40, 48, 50	ringcld 20517	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑖})) → ((𝑏‘𝑙) · 𝑙) ∈ 𝐵)
52		fveq2 6911	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑙 → (𝑏‘𝑗) = (𝑏‘𝑙))
53		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑙 → 𝑗 = 𝑙)
54	52, 53	oveq12d 7464	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑙 → ((𝑏‘𝑗) · 𝑗) = ((𝑏‘𝑙) · 𝑙))
55	54	cbvmptv 5213	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑙 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑙) · 𝑙))
56	51, 55	fmptd 7141	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)):(^◡𝑓 “ {𝑖})⟶𝐵)
57	39	mptexd 7256	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V)
58	56	ffund 6739	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → Fun (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))
59		simp-5r 798	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → 𝑏 finSupp 0 )
60		nfv 1949	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 )
61		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝑅
62		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 Σ_g
63		nfmpt1 5208	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗(𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))
64	61, 62, 63	nfov 7476	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))
65	64	nfeq2 2943	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))
66	60, 65	nfan 1934	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗(((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))
67		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑓:∪ 𝑆⟶𝑆
68	66, 67	nfan 1934	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆)
69		nfra1 3290	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)
70	68, 69	nfan 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗))
71		nfv 1949	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗 𝑖 ∈ 𝑆
72	70, 71	nfan 1934	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆)
73		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(^◡𝑓 “ {𝑖})
74		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝑏 supp 0 )
75	41	ad7antlr 752	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏:∪ 𝑆⟶𝐵)
76	75	ffnd 6735	. . . . . . . . . . . . . . . 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 6925	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
80	79	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
81	46	ssdifd 4084	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ (∪ 𝑆 ∖ (𝑏 supp 0 )))
82	81	sselda 3913	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
83	76, 78, 80, 82	fvdifsupp 8219	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
84	83	oveq1d 7461	. . . . . . . . . . . . . 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 4054	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ∪ 𝑆)
88	86, 87	sseldd 3914	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ 𝐵)
89	2, 4, 3	ringlz 20557	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ 𝐵) → ( 0 · 𝑗) = 0 )
90	85, 88, 89	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
91	84, 90	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = 0 )
92	72, 73, 74, 91, 39	suppss2f 33307	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → ((𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
93		fsuppsssupp 9403	. . . . . . . . . . . 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 20162	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) ∈ 𝐵)
96	95	fmpttd 7142	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))):𝑆⟶𝐵)
97	2	fvexi 6925	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
98	97	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ V)
99	98, 16	elmapd 8891	. . . . . . . . . 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 7256	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) ∈ V)
104	79	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 0 ∈ V)
105		funmpt 6601	. . . . . . . . . . 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 6739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Fun 𝑓)
109		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑏 finSupp 0 )
110	109	fsuppimpd 9392	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑏 supp 0 ) ∈ Fin)
111		imafi 9338	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
112	108, 110, 111	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
113		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
114	70, 113	nfan 1934	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
115		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓:∪ 𝑆⟶𝑆)
116	115	ffund 6739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
117		snssi 4746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
118	117	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
119		sspreima 7094	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (^◡𝑓 “ {𝑖}) ⊆ (^◡𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
120	116, 118, 119	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (^◡𝑓 “ {𝑖}) ⊆ (^◡𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
121		difpreima 7091	. . . . . . . . . . . . . . . . . . . . . . 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 3949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (^◡𝑓 “ {𝑖}) ⊆ ((^◡𝑓 “ 𝑆) ∖ (^◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
124		suppssdm 8225	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 supp 0 ) ⊆ dom 𝑏
125	41	ad6antlr 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏:∪ 𝑆⟶𝐵)
126	124, 125	fssdm 6754	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ ∪ 𝑆)
127	115	fdmd 6745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = ∪ 𝑆)
128	126, 127	sseqtrrd 3950	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
129		sseqin2 4123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
130	129	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
131		dminss 6156	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (^◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))
132	130, 131	eqsstrrdi 3958	. . . . . . . . . . . . . . . . . . . . . . 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 4085	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((^◡𝑓 “ 𝑆) ∖ (^◡𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((^◡𝑓 “ 𝑆) ∖ (𝑏 supp 0 )))
135	123, 134	sstrd 3923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (^◡𝑓 “ {𝑖}) ⊆ ((^◡𝑓 “ 𝑆) ∖ (𝑏 supp 0 )))
136		fimacnv 6757	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓:∪ 𝑆⟶𝑆 → (^◡𝑓 “ 𝑆) = ∪ 𝑆)
137	115, 136	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (^◡𝑓 “ 𝑆) = ∪ 𝑆)
138	137	difeq1d 4065	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((^◡𝑓 “ 𝑆) ∖ (𝑏 supp 0 )) = (∪ 𝑆 ∖ (𝑏 supp 0 )))
139	135, 138	sseqtrd 3949	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (^◡𝑓 “ {𝑖}) ⊆ (∪ 𝑆 ∖ (𝑏 supp 0 )))
140	139	sselda 3913	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (^◡𝑓 “ {𝑖})) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
141		ssidd 3936	. . . . . . . . . . . . . . . . . . 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 8243	. . . . . . . . . . . . . . . . . 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 7461	. . . . . . . . . . . . . . . 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 3913	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (^◡𝑓 “ {𝑖})) → 𝑗 ∈ ∪ 𝑆)
151	148, 150	sseldd 3914	. . . . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (^◡𝑓 “ {𝑖})) → ((𝑏‘𝑗) · 𝑗) = 0 )
154	114, 153	mpteq2da 5201	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ 0 ))
155	154	oveq2d 7462	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ 0 )))
156	5	ringcmnd 20546	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑅 ∈ CMnd)
157	156	cmnmndd 20051	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ Mnd)
158	157	ad6antr 749	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
159	3	gsumz 19064	. . . . . . . . . . . . . 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 2798	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) = 0 )
162	161, 102	suppss2 8248	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
163	112, 162	ssfid 9291	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
164	103, 104, 106, 163	isfsuppd 9389	. . . . . . . . 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 7111	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → (𝑏‘𝑗) ∈ 𝐵)
170	32, 13	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∪ 𝑆 ⊆ 𝐵)
171	170	sselda 3913	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → 𝑗 ∈ 𝐵)
172	2, 4, 167, 169, 171	ringcld 20517	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ ∪ 𝑆) → ((𝑏‘𝑗) · 𝑗) ∈ 𝐵)
173		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))
174	70, 172, 173	fmptdf 7144	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)):∪ 𝑆⟶𝐵)
175	77	mptexd 7256	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V)
176		funmpt 6601	. . . . . . . . . . . . 13 ⊢ Fun (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))
177	176	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Fun (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))
178		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗∪ 𝑆
179	168	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏:∪ 𝑆⟶𝐵)
180	179	ffnd 6735	. . . . . . . . . . . . . . . 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 8219	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
185	184	oveq1d 7461	. . . . . . . . . . . . . 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 4054	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ∪ 𝑆)
189	187, 188	sseldd 3914	. . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = 0 )
192	70, 178, 74, 191, 77	suppss2f 33307	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
193		fsuppsssupp 9403	. . . . . . . . . . . 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 5098	. . . . . . . . . . . 12 ⊢ Disj 𝑖 ∈ 𝑆 {𝑖}
196		disjpreima 33253	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ Disj 𝑖 ∈ 𝑆 {𝑖}) → Disj 𝑖 ∈ 𝑆 (^◡𝑓 “ {𝑖}))
197	108, 195, 196	sylancl 598	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → Disj 𝑖 ∈ 𝑆 (^◡𝑓 “ {𝑖}))
198		iunid 5022	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ 𝑆 {𝑖} = 𝑆
199	198	imaeq2i 6063	. . . . . . . . . . . 12 ⊢ (^◡𝑓 “ ∪ 𝑖 ∈ 𝑆 {𝑖}) = (^◡𝑓 “ 𝑆)
200		iunpreima 7095	. . . . . . . . . . . . 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 2822	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → ∪ 𝑖 ∈ 𝑆 (^◡𝑓 “ {𝑖}) = ∪ 𝑆)
204	2, 3, 166, 77, 102, 174, 194, 197, 203	gsumpart 33700	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σ_g (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (^◡𝑓 “ {𝑖}))))))
205	46	resmptd 6045	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (^◡𝑓 “ {𝑖})) = (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))
206	205	oveq2d 7462	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑖 ∈ 𝑆) → (𝑅 Σ_g ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (^◡𝑓 “ {𝑖}))) = (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))
207	206	mpteq2dva 5202	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (^◡𝑓 “ {𝑖})))) = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))))
208	207	oveq2d 7462	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → (𝑅 Σ_g (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g ((𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) ↾ (^◡𝑓 “ {𝑖}))))) = (𝑅 Σ_g (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))))
209	165, 204, 208	3eqtrd 2802	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) → 𝑋 = (𝑅 Σ_g (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))))
210		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)))) = (𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))
211		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
212	211	sneqd 4596	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
213	212	imaeq2d 6065	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → (^◡𝑓 “ {𝑖}) = (^◡𝑓 “ {𝑘}))
214	213	mpteq1d 5199	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)))
215	214	oveq2d 7462	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))))
216		simpr 490	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ 𝑆)
217		ovexd 7481	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))) ∈ V)
218	210, 215, 216, 217	fvmptd2 7028	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) = (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))))
219	156	ad6antr 749	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑅 ∈ CMnd)
220	37	imaex 7953	. . . . . . . . . . . . 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 3913	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
225	8	lidlsubg 21535	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
226		subgsubm 19391	. . . . . . . . . . . . . 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 6212	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑓 “ {𝑘}) ⊆ dom 𝑓
233	232, 44	sseqtrid 3955	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:∪ 𝑆⟶𝑆 → (^◡𝑓 “ {𝑘}) ⊆ ∪ 𝑆)
234	233	ad3antlr 744	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (^◡𝑓 “ {𝑘}) ⊆ ∪ 𝑆)
235	234	sselda 3913	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → 𝑙 ∈ ∪ 𝑆)
236	231, 235	ffvelcdmd 7112	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → (𝑏‘𝑙) ∈ 𝐵)
237		fveq2 6911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑙 → (𝑓‘𝑗) = (𝑓‘𝑙))
238	53, 237	eleq12d 2858	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑙 → (𝑗 ∈ (𝑓‘𝑗) ↔ 𝑙 ∈ (𝑓‘𝑙)))
239		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗))
240	238, 239, 235	rspcdva 3581	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓‘𝑙))
241		simp-4r 796	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → 𝑓:∪ 𝑆⟶𝑆)
242	241	ffnd 6735	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → 𝑓 Fn ∪ 𝑆)
243		elpreima 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 Fn ∪ 𝑆 → (𝑙 ∈ (^◡𝑓 “ {𝑘}) ↔ (𝑙 ∈ ∪ 𝑆 ∧ (𝑓‘𝑙) ∈ {𝑘})))
244	243	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 Fn ∪ 𝑆 ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → (𝑙 ∈ ∪ 𝑆 ∧ (𝑓‘𝑙) ∈ {𝑘}))
245		elsni 4601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓‘𝑙) ∈ {𝑘} → (𝑓‘𝑙) = 𝑘)
246	244, 245	simpl2im 513	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 Fn ∪ 𝑆 ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → (𝑓‘𝑙) = 𝑘)
247	242, 246	sylancom 600	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → (𝑓‘𝑙) = 𝑘)
248	240, 247	eleqtrd 2866	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → 𝑙 ∈ 𝑘)
249	8, 2, 4, 229, 230, 236, 248	lidlmcld 21539	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑙 ∈ (^◡𝑓 “ {𝑘})) → ((𝑏‘𝑙) · 𝑙) ∈ 𝑘)
250	54	cbvmptv 5213	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑙 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑙) · 𝑙))
251	249, 250	fmptd 7141	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)):(^◡𝑓 “ {𝑘})⟶𝑘)
252	221	mptexd 7256	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) ∈ V)
253	251	ffund 6739	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → Fun (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)))
254		simp-5r 798	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → 𝑏 finSupp 0 )
255		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗 𝑘 ∈ 𝑆
256	70, 255	nfan 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆)
257		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(^◡𝑓 “ {𝑘})
258	41	ad7antlr 752	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏:∪ 𝑆⟶𝐵)
259	258	ffnd 6735	. . . . . . . . . . . . . . . . 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 4084	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ (∪ 𝑆 ∖ (𝑏 supp 0 )))
263	262	sselda 3913	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ (∪ 𝑆 ∖ (𝑏 supp 0 )))
264	259, 260, 261, 263	fvdifsupp 8219	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏‘𝑗) = 0 )
265	264	oveq1d 7461	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = ( 0 · 𝑗))
266	13	ad7antr 751	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ∪ 𝑆 ⊆ 𝐵)
267	263	eldifad 4054	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ∪ 𝑆)
268	266, 267	sseldd 3914	. . . . . . . . . . . . . . . 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 2798	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) ∧ 𝑗 ∈ ((^◡𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏‘𝑗) · 𝑗) = 0 )
271	256, 257, 74, 270, 221	suppss2f 33307	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
272		fsuppsssupp 9403	. . . . . . . . . . . . 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 20166	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑘}) ↦ ((𝑏‘𝑗) · 𝑗))) ∈ 𝑘)
275	218, 274	eqeltrd 2864	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))) ∧ 𝑓:∪ 𝑆⟶𝑆) ∧ ∀𝑗 ∈ ∪ 𝑆𝑗 ∈ (𝑓‘𝑗)) ∧ 𝑘 ∈ 𝑆) → ((𝑖 ∈ 𝑆 ↦ (𝑅 Σ_g (𝑗 ∈ (^◡𝑓 “ {𝑖}) ↦ ((𝑏‘𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
276	275	ralrimiva 3158	. . . . . . . . 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 3583	. . . . . . 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 1970	. . . . 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 3170	. . 3 ⊢ ((𝜑 ∧ ∃𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵 ↑_m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σ_g 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))
283		breq1 5109	. . . . . . 7 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
284		fveq1 6910	. . . . . . . . . . 11 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏‘𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
285	284	oveq1d 7461	. . . . . . . . . 10 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏‘𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
286	285	mpteq2dv 5203	. . . . . . . . 9 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)) = (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
287	286	oveq2d 7462	. . . . . . . 8 ⊢ (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗))) = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
288	287	eqeq2d 2774	. . . . . . 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 8891	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑎 ∈ (𝐵 ↑_m 𝑆) ↔ 𝑎:𝑆⟶𝐵))
293	292	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) → 𝑎:𝑆⟶𝐵)
294	293	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑎:𝑆⟶𝐵)
295	294	ffnd 6735	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
296		elssuni 4902	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ 𝑆 → 𝑘 ⊆ ∪ 𝑆)
297	296	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ 𝑘 ∈ 𝑆) → 𝑘 ⊆ ∪ 𝑆)
298	297	sseld 3912	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ 𝑘 ∈ 𝑆) → ((𝑎‘𝑘) ∈ 𝑘 → (𝑎‘𝑘) ∈ ∪ 𝑆))
299	298	ralimdva 3178	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) → (∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘 → ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ ∪ 𝑆))
300	299	imp 412	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ ∪ 𝑆)
301		fnfvrnss 7148	. . . . . . . . . . 11 ⊢ ((𝑎 Fn 𝑆 ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ ∪ 𝑆) → ran 𝑎 ⊆ ∪ 𝑆)
302	295, 300, 301	syl2anc 596	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ran 𝑎 ⊆ ∪ 𝑆)
303	302	ssdifssd 4086	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ ∪ 𝑆)
304		undif 4441	. . . . . . . . 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 2763	. . . . . . . . . . . . 13 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
309	308	zrhrhm 21850	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤ_ring RingHom 𝑅))
310		zringbas 21792	. . . . . . . . . . . . 13 ⊢ ℤ = (Base‘ℤ_ring)
311	310, 2	rhmf 20748	. . . . . . . . . . . 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 3937	. . . . . . . . . . . . . . . . 17 ⊢ ran 𝑎 ⊆ V
316		ssdif 4083	. . . . . . . . . . . . . . . . 17 ⊢ (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
317	315, 316	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
318	317	sseli 3909	. . . . . . . . . . . . . . 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 33354	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (^◡𝑎 “ {𝑚}) ∈ Fin)
322		hashcl 14530	. . . . . . . . . . . . 13 ⊢ ((^◡𝑎 “ {𝑚}) ∈ Fin → (♯‘(^◡𝑎 “ {𝑚})) ∈ ℕ₀)
323	321, 322	syl 18	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(^◡𝑎 “ {𝑚})) ∈ ℕ₀)
324	323	nn0zd 12748	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(^◡𝑎 “ {𝑚})) ∈ ℤ)
325	312, 324	ffvelcdmd 7112	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚}))) ∈ 𝐵)
326		eqid 2763	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚}))))
327	325, 326	fmptd 7141	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
328	2, 3	ring0cl 20529	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵)
329		fconst6g 6796	. . . . . . . . . 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 4429	. . . . . . . . . 10 ⊢ ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
332	331	a1i 11	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
333	327, 330, 332	fun2d 6771	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
334	305, 333	feq2dd 6720	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):∪ 𝑆⟶𝐵)
335	290, 291, 334	elmapdd 8892	. . . . . 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 6739	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })))
338	294	ffund 6739	. . . . . . . . . . 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 33359	. . . . . . . . . . . 12 ⊢ (((Fun 𝑎 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
342		diffi 9221	. . . . . . . . . . . 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 9397	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) finSupp 0 )
346	13	ssdifssd 4086	. . . . . . . . . . . 12 ⊢ (𝜑 → (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
347	346	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
348	290, 347	ssexd 5291	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
349	348, 336	fczfsuppd 9408	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
350	345, 349	fsuppun 9409	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
351	335, 336, 337, 350	isfsuppd 9389	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
352		fvex 6924	. . . . . . . . . . . . . . 15 ⊢ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚}))) ∈ V
353	352, 326	fnmpti 6707	. . . . . . . . . . . . . 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 6795	. . . . . . . . . . . . . . 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 7004	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚}))))‘𝑗))
361		sneq 4594	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑗 → {𝑚} = {𝑗})
362	361	imaeq2d 6065	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑗 → (^◡𝑎 “ {𝑚}) = (^◡𝑎 “ {𝑗}))
363	362	fveq2d 6915	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑗 → (♯‘(^◡𝑎 “ {𝑚})) = (♯‘(^◡𝑎 “ {𝑗})))
364	363	fveq2d 6915	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))))
365		fvexd 6926	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) ∈ V)
366	326, 364, 359, 365	fvmptd3 7043	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))))
367	360, 366	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))))
368	367	oveq1d 7461	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗))
369	368	mpteq2dva 5202	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗)))
370	369	oveq2d 7462	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σ_g (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σ_g (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗))))
371	306	ringcmnd 20546	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑅 ∈ CMnd)
372	331	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((ran 𝑎 ∖ { 0 }) ∩ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
373		fvun2 7003	. . . . . . . . . . . . . 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 1481	. . . . . . . . . . . . 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 7236	. . . . . . . . . . . . 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 2798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
379	378	oveq1d 7461	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
380	347	sselda 3913	. . . . . . . . . . 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 2798	. . . . . . . . 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 7111	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
385	13	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∪ 𝑆 ⊆ 𝐵)
386	385	sselda 3913	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → 𝑗 ∈ 𝐵)
387	2, 4, 383, 384, 386	ringcld 20517	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ∪ 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
388	2, 3, 371, 291, 382, 344, 387, 303	gsummptres2 33690	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σ_g (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑚})))) ∪ ((∪ 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
389		eqid 2763	. . . . . . . . . 10 ⊢ (._g‘𝑅) = (._g‘𝑅)
390	2, 3, 389, 371, 294, 340	gsumhashmul 33704	. . . . . . . . 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 3911	. . . . . . . . . . . . . . 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 33354	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (^◡𝑎 “ {𝑗}) ∈ Fin)
398		hashcl 14530	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑎 “ {𝑗}) ∈ Fin → (♯‘(^◡𝑎 “ {𝑗})) ∈ ℕ₀)
399	397, 398	syl 18	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(^◡𝑎 “ {𝑗})) ∈ ℕ₀)
400	399	nn0zd 12748	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ)
401	303, 385	sstrd 3923	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
402	401	sselda 3913	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ 𝐵)
403		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
404	308, 389, 403	zrhmulg 21848	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)(1_r‘𝑅)))
405	404	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → ((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)(1_r‘𝑅)))
406	405	oveq1d 7461	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)(1_r‘𝑅)) · 𝑗))
407		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → 𝑅 ∈ Ring)
408		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ)
409	2, 403	ringidcl 20527	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ Ring → (1_r‘𝑅) ∈ 𝐵)
410	409	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (1_r‘𝑅) ∈ 𝐵)
411		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → 𝑗 ∈ 𝐵)
412	2, 389, 4	mulgass2 20573	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Ring ∧ ((♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ ∧ (1_r‘𝑅) ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)(1_r‘𝑅)) · 𝑗) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)((1_r‘𝑅) · 𝑗)))
413	407, 408, 410, 411, 412	syl13anc 1400	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)(1_r‘𝑅)) · 𝑗) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)((1_r‘𝑅) · 𝑗)))
414	2, 4, 403	ringlidm 20531	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ 𝐵) → ((1_r‘𝑅) · 𝑗) = 𝑗)
415	407, 414	sylancom 600	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → ((1_r‘𝑅) · 𝑗) = 𝑗)
416	415	oveq2d 7462	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)((1_r‘𝑅) · 𝑗)) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)𝑗))
417	406, 413, 416	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ (♯‘(^◡𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗 ∈ 𝐵) → (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)𝑗))
418	392, 400, 402, 417	syl21anc 851	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)𝑗))
419	418	mpteq2dva 5202	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)𝑗)))
420	419	oveq2d 7462	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → (𝑅 Σ_g (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σ_g (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(^◡𝑎 “ {𝑗}))(._g‘𝑅)𝑗))))
421	390, 391, 420	3eqtr4d 2808	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σ_g (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(^◡𝑎 “ {𝑗}))) · 𝑗))))
422	370, 388, 421	3eqtr4rd 2809	. . . . . . 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 3583	. . . . 5 ⊢ (((((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σ_g 𝑎)) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))))
425	424	3anasss 1381	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝐵 ↑_m 𝑆)) ∧ (𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σ_g 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵 ↑_m ∪ 𝑆)(𝑏 finSupp 0 ∧ 𝑋 = (𝑅 Σ_g (𝑗 ∈ ∪ 𝑆 ↦ ((𝑏‘𝑗) · 𝑗)))))
426	425	r19.29an 3170	. . 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 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∪ cun 4152 ∅c0 4281 {csn 4588 ∪ cuni 4870 ∪ ciun 4954 Disj wdisj 5073 class class class wbr 5106 ↦ cmpt 5190 × cxp 5654 ^◡ccnv 5655 dom cdm 5656 ran crn 5657 ↾ cres 5658 “ cima 5659 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7446 supp csupp 8207 ↑_m cmap 8878 Fincfn 9004 finSupp cfsupp 9384 ℕ₀cn0 12636 ℤcz 12723 ♯chash 14504 Basecbs 17419 ._rcmulr 17461 0_gc0g 17642 Σ_g cgsu 17643 Mndcmnd 18955 SubMndcsubmnd 19009 ._gcmg 19309 SubGrpcsubg 19362 CMndccmn 20027 1_rcur 20440 Ringcrg 20492 RingHom crh 20732 LIdealclidl 21517 RSpancrsp 21518 ℤ_ringczring 21785 ℤRHomczrh 21838

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-ac2 10571 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-addf 11309 ax-mulf 11310

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-disj 5074 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-of 7720 df-om 7905 df-1st 8028 df-2nd 8029 df-supp 8208 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-er 8748 df-map 8880 df-ixp 8957 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-fsupp 9385 df-sup 9464 df-oi 9534 df-card 10050 df-ac 10225 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-7 12440 df-8 12441 df-9 12442 df-n0 12637 df-z 12724 df-dec 12845 df-uz 12996 df-fz 13670 df-fzo 13819 df-seq 14175 df-hash 14505 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-starv 17475 df-sca 17476 df-vsca 17477 df-ip 17478 df-tset 17479 df-ple 17480 df-ds 17482 df-unif 17483 df-hom 17484 df-cco 17485 df-0g 17644 df-gsum 17645 df-prds 17650 df-pws 17652 df-mre 17788 df-mrc 17789 df-acs 17791 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-mhm 19010 df-submnd 19011 df-grp 19179 df-minusg 19180 df-sbg 19181 df-mulg 19310 df-subg 19365 df-ghm 19460 df-cntz 19564 df-cmn 20029 df-abl 20030 df-mgp 20394 df-rng 20408 df-ur 20441 df-ring 20494 df-cring 20495 df-rhm 20735 df-nzr 20796 df-subrng 20831 df-subrg 20855 df-lmod 21170 df-lss 21240 df-lsp 21280 df-lmhm 21330 df-lbs 21383 df-sra 21481 df-rgmod 21482 df-lidl 21519 df-rsp 21520 df-cnfld 21712 df-zring 21786 df-zrh 21842 df-dsmm 22071 df-frlm 22086 df-uvc 22122

This theorem is used by: zarcmplem 34596

W3C validator