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

Theorem elrspunidl 33575
Description: Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.)
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.
StepHypRef 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‘𝑅))
76sselda 3936 . . . . . 6 ((𝜑𝑖𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8 eqid 2761 . . . . . . 7 (LIdeal‘𝑅) = (LIdeal‘𝑅)
92, 8lidlss 21262 . . . . . 6 (𝑖 ∈ (LIdeal‘𝑅) → 𝑖𝐵)
107, 9syl 17 . . . . 5 ((𝜑𝑖𝑆) → 𝑖𝐵)
1110ralrimiva 3153 . . . 4 (𝜑 → ∀𝑖𝑆 𝑖𝐵)
12 unissb 4898 . . . 4 ( 𝑆𝐵 ↔ ∀𝑖𝑆 𝑖𝐵)
1311, 12sylibr 236 . . 3 (𝜑 𝑆𝐵)
141, 2, 3, 4, 5, 13elrsp 33519 . 2 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))
15 fvexd 6878 . . . . . . . . . 10 (𝜑 → (LIdeal‘𝑅) ∈ V)
1615, 6ssexd 5279 . . . . . . . . 9 (𝜑𝑆 ∈ V)
1716uniexd 7721 . . . . . . . 8 (𝜑 𝑆 ∈ V)
18 eluni2 4868 . . . . . . . . . 10 (𝑗 𝑆 ↔ ∃𝑖𝑆 𝑗𝑖)
1918bilani 508 . . . . . . . . 9 ((𝜑𝑗 𝑆) → ∃𝑖𝑆 𝑗𝑖)
2019ralrimiva 3153 . . . . . . . 8 (𝜑 → ∀𝑗 𝑆𝑖𝑆 𝑗𝑖)
21 eleq2 2850 . . . . . . . . 9 (𝑖 = (𝑓𝑗) → (𝑗𝑖𝑗 ∈ (𝑓𝑗)))
2221ac6sg 10442 . . . . . . . 8 ( 𝑆 ∈ V → (∀𝑗 𝑆𝑖𝑆 𝑗𝑖 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))))
2317, 20, 22sylc 65 . . . . . . 7 (𝜑 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
2423ad3antrrr 740 . . . . . 6 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
25 simp-5l 794 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝜑)
2625adantr 484 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝜑)
27 ringcmn 20311 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
2826, 5, 273syl 18 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑅 ∈ CMnd)
29 vex 3457 . . . . . . . . . . . . 13 𝑓 ∈ V
30 cnvexg 7901 . . . . . . . . . . . . 13 (𝑓 ∈ V → 𝑓 ∈ V)
31 imaexg 7890 . . . . . . . . . . . . 13 (𝑓 ∈ V → (𝑓 “ {𝑖}) ∈ V)
3229, 30, 31mp2b 10 . . . . . . . . . . . 12 (𝑓 “ {𝑖}) ∈ V
3332a1i 11 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ∈ V)
345ad7antr 748 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
35 elmapi 8826 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵m 𝑆) → 𝑏: 𝑆𝐵)
3635ad7antlr 749 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑏: 𝑆𝐵)
37 cnvimass 6068 . . . . . . . . . . . . . . . . 17 (𝑓 “ {𝑖}) ⊆ dom 𝑓
38 fdm 6697 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → dom 𝑓 = 𝑆)
3937, 38sseqtrid 3978 . . . . . . . . . . . . . . . 16 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑖}) ⊆ 𝑆)
4039ad3antlr 741 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ⊆ 𝑆)
4140sselda 3936 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙 𝑆)
4236, 41ffvelcdmd 7062 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → (𝑏𝑙) ∈ 𝐵)
4313ad7antr 748 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
4443, 41sseldd 3937 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙𝐵)
452, 4ringcl 20279 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑙) ∈ 𝐵𝑙𝐵) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
4634, 42, 44, 45syl3anc 1389 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
47 fveq2 6863 . . . . . . . . . . . . . 14 (𝑗 = 𝑙 → (𝑏𝑗) = (𝑏𝑙))
48 id 22 . . . . . . . . . . . . . 14 (𝑗 = 𝑙𝑗 = 𝑙)
4947, 48oveq12d 7410 . . . . . . . . . . . . 13 (𝑗 = 𝑙 → ((𝑏𝑗) · 𝑗) = ((𝑏𝑙) · 𝑙))
5049cbvmptv 5203 . . . . . . . . . . . 12 (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑙) · 𝑙))
5146, 50fmptd 7091 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑖})⟶𝐵)
5233mptexd 7204 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
5351ffund 6692 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
54 simp-5r 795 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑏 finSupp 0 )
55 nfv 1933 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 )
56 nfcv 2923 . . . . . . . . . . . . . . . . . . 19 𝑗𝑅
57 nfcv 2923 . . . . . . . . . . . . . . . . . . 19 𝑗 Σg
58 nfmpt1 5198 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
5956, 57, 58nfov 7422 . . . . . . . . . . . . . . . . . 18 𝑗(𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6059nfeq2 2940 . . . . . . . . . . . . . . . . 17 𝑗 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6155, 60nfan 1918 . . . . . . . . . . . . . . . 16 𝑗(((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
62 nfv 1933 . . . . . . . . . . . . . . . 16 𝑗 𝑓: 𝑆𝑆
6361, 62nfan 1918 . . . . . . . . . . . . . . 15 𝑗((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆)
64 nfra1 3285 . . . . . . . . . . . . . . 15 𝑗𝑗 𝑆𝑗 ∈ (𝑓𝑗)
6563, 64nfan 1918 . . . . . . . . . . . . . 14 𝑗(((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
66 nfv 1933 . . . . . . . . . . . . . 14 𝑗 𝑖𝑆
6765, 66nfan 1918 . . . . . . . . . . . . 13 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆)
68 nfcv 2923 . . . . . . . . . . . . 13 𝑗(𝑓 “ {𝑖})
69 nfcv 2923 . . . . . . . . . . . . 13 𝑗(𝑏 supp 0 )
7035ad7antlr 749 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
7170ffnd 6688 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
7225, 17syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
7372ad2antrr 736 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
743fvexi 6877 . . . . . . . . . . . . . . . . 17 0 ∈ V
7574a1i 11 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
7640ssdifd 4098 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
7776sselda 3936 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
7871, 73, 75, 77fvdifsupp 8146 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
7978oveq1d 7407 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
805ad7antr 748 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
8113ad7antr 748 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
8277eldifad 3916 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
8381, 82sseldd 3937 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
842, 4, 3ringlz 20322 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ( 0 · 𝑗) = 0 )
8580, 83, 84syl2anc 593 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
8679, 85eqtrd 2796 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
8767, 68, 69, 86, 33suppss2f 32790 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
88 fsuppsssupp 9324 . . . . . . . . . . . 12 ((((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
8952, 53, 54, 87, 88syl22anc 849 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
902, 3, 28, 33, 51, 89gsumcl 19938 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝐵)
9190fmpttd 7092 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵)
922fvexi 6877 . . . . . . . . . . . 12 𝐵 ∈ V
9392a1i 11 . . . . . . . . . . 11 (𝜑𝐵 ∈ V)
9493, 16elmapd 8817 . . . . . . . . . 10 (𝜑 → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆) ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵))
9594biimpar 481 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
9625, 91, 95syl2anc 593 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
97 breq1 5102 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ))
98 oveq2 7400 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
9998eqeq2d 2772 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σg 𝑎) ↔ 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))))
100 fveq1 6862 . . . . . . . . . . . 12 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎𝑘) = ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘))
101100eleq1d 2846 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎𝑘) ∈ 𝑘 ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
102101ralbidv 3184 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 ↔ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
10397, 99, 1023anbi123d 1456 . . . . . . . . 9 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
104103adantl 485 . . . . . . . 8 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
10525, 16syl 17 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
106105mptexd 7204 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V)
10774a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 0 ∈ V)
108 funmpt 6555 . . . . . . . . . . 11 Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
109108a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
110 simplr 778 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑓: 𝑆𝑆)
111110ffund 6692 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun 𝑓)
112 simp-4r 793 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏 finSupp 0 )
113112fsuppimpd 9312 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑏 supp 0 ) ∈ Fin)
114 imafi 9255 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
115111, 113, 114syl2anc 593 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
116 nfv 1933 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
11765, 116nfan 1918 . . . . . . . . . . . . . . 15 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
118 simpllr 785 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓: 𝑆𝑆)
119118ffund 6692 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
120 snssi 4743 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
121120adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
122 sspreima 7045 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
123119, 121, 122syl2anc 593 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
124 difpreima 7042 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝑓 → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
125119, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
126123, 125sseqtrd 3972 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
127 suppssdm 8152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 supp 0 ) ⊆ dom 𝑏
12835ad6antlr 747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏: 𝑆𝐵)
129127, 128fssdm 6707 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ 𝑆)
130118fdmd 6698 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = 𝑆)
131129, 130sseqtrrd 3973 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
132 sseqin2 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
133132biimpi 218 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
134 dminss 6135 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))
135133, 134eqsstrrdi 3981 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
136131, 135syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
137136sscond 4099 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
138126, 137sstrd 3946 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
139 fimacnv 6710 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓: 𝑆𝑆 → (𝑓𝑆) = 𝑆)
140118, 139syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓𝑆) = 𝑆)
141140difeq1d 4079 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑏 supp 0 )) = ( 𝑆 ∖ (𝑏 supp 0 )))
142138, 141sseqtrd 3972 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
143142sselda 3936 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
144 ssidd 3959 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑏 supp 0 ))
14572adantr 484 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑆 ∈ V)
14674a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 0 ∈ V)
147128, 144, 145, 146suppssr 8170 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
148143, 147syldan 600 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → (𝑏𝑗) = 0 )
149148oveq1d 7407 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1505ad7antr 748 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
15113ad7antr 748 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
15239ad3antlr 741 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ 𝑆)
153152sselda 3936 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 𝑆)
154151, 153sseldd 3937 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗𝐵)
155150, 154, 84syl2anc 593 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ( 0 · 𝑗) = 0 )
156149, 155eqtrd 2796 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = 0 )
157117, 156mpteq2da 5191 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 ))
158157oveq2d 7408 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )))
1595, 27syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ CMnd)
160159cmnmndd 19827 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ Mnd)
161160ad6antr 746 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
1623gsumz 18853 . . . . . . . . . . . . . 14 ((𝑅 ∈ Mnd ∧ (𝑓 “ {𝑖}) ∈ V) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
163161, 32, 162sylancl 595 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
164158, 163eqtrd 2796 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = 0 )
165164, 105suppss2 8175 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
166115, 165ssfid 9209 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
167 isfsupp 9308 . . . . . . . . . . 11 (((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ↔ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)))
168167biimpar 481 . . . . . . . . . 10 ((((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) ∧ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
169106, 107, 109, 166, 168syl22anc 849 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
170 simpllr 785 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
17125, 159syl 17 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑅 ∈ CMnd)
1725ad6antr 746 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
17335ad5antlr 745 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏: 𝑆𝐵)
174173ffvelcdmda 7061 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → (𝑏𝑗) ∈ 𝐵)
17525, 13syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆𝐵)
176175sselda 3936 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑗𝐵)
1772, 4ringcl 20279 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑗) ∈ 𝐵𝑗𝐵) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
178172, 174, 176, 177syl3anc 1389 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
179 eqid 2761 . . . . . . . . . . . 12 (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
18065, 178, 179fmptdf 7094 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)): 𝑆𝐵)
18172mptexd 7204 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
182 funmpt 6555 . . . . . . . . . . . . 13 Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
183182a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
184 nfcv 2923 . . . . . . . . . . . . 13 𝑗 𝑆
185173adantr 484 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
186185ffnd 6688 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
18772adantr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
18874a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 0 ∈ V)
189 simpr 488 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
190186, 187, 188, 189fvdifsupp 8146 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
191190oveq1d 7407 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1925ad6antr 746 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
193175adantr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
194189eldifad 3916 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
195193, 194sseldd 3937 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
196192, 195, 84syl2anc 593 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
197191, 196eqtrd 2796 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
19865, 184, 69, 197, 72suppss2f 32790 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
199 fsuppsssupp 9324 . . . . . . . . . . . 12 ((((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
200181, 183, 112, 198, 199syl22anc 849 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
201 sndisj 5091 . . . . . . . . . . . 12 Disj 𝑖𝑆 {𝑖}
202 disjpreima 32733 . . . . . . . . . . . 12 ((Fun 𝑓Disj 𝑖𝑆 {𝑖}) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
203111, 201, 202sylancl 595 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
204 iunid 5017 . . . . . . . . . . . . 13 𝑖𝑆 {𝑖} = 𝑆
205204imaeq2i 6044 . . . . . . . . . . . 12 (𝑓 𝑖𝑆 {𝑖}) = (𝑓𝑆)
206 iunpreima 32713 . . . . . . . . . . . . 13 (Fun 𝑓 → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
207111, 206syl 17 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
208139ad2antlr 737 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓𝑆) = 𝑆)
209205, 207, 2083eqtr3a 2820 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑖𝑆 (𝑓 “ {𝑖}) = 𝑆)
2102, 3, 171, 72, 105, 180, 200, 203, 209gsumpart 33204 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))))
21140resmptd 6026 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
212211oveq2d 7408 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
213212mpteq2dva 5192 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
214213oveq2d 7408 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
215170, 210, 2143eqtrd 2800 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
216 eqid 2761 . . . . . . . . . . . 12 (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
217 simpr 488 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
218217sneqd 4593 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
219218imaeq2d 6046 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑓 “ {𝑖}) = (𝑓 “ {𝑘}))
220219mpteq1d 5189 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
221220oveq2d 7408 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
222 simpr 488 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘𝑆)
223 ovexd 7427 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ V)
224216, 221, 222, 223fvmptd2 6980 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
225159ad6antr 746 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ CMnd)
22629cnvex 7902 . . . . . . . . . . . . . 14 𝑓 ∈ V
227226imaex 7891 . . . . . . . . . . . . 13 (𝑓 “ {𝑘}) ∈ V
228227a1i 11 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ∈ V)
2295ad6antr 746 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ Ring)
23025, 6syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ⊆ (LIdeal‘𝑅))
231230sselda 3936 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
2328lidlsubg 21273 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
233 subgsubm 19173 . . . . . . . . . . . . . 14 (𝑘 ∈ (SubGrp‘𝑅) → 𝑘 ∈ (SubMnd‘𝑅))
234232, 233syl 17 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubMnd‘𝑅))
235229, 231, 234syl2anc 593 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (SubMnd‘𝑅))
236229adantr 484 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑅 ∈ Ring)
237231adantr 484 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑘 ∈ (LIdeal‘𝑅))
23835ad7antlr 749 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑏: 𝑆𝐵)
239 cnvimass 6068 . . . . . . . . . . . . . . . . . 18 (𝑓 “ {𝑘}) ⊆ dom 𝑓
240239, 38sseqtrid 3978 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑘}) ⊆ 𝑆)
241240ad3antlr 741 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ⊆ 𝑆)
242241sselda 3936 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 𝑆)
243238, 242ffvelcdmd 7062 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑏𝑙) ∈ 𝐵)
244 fveq2 6863 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑙 → (𝑓𝑗) = (𝑓𝑙))
24548, 244eleq12d 2855 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑙 → (𝑗 ∈ (𝑓𝑗) ↔ 𝑙 ∈ (𝑓𝑙)))
246 simpllr 785 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
247245, 246, 242rspcdva 3582 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓𝑙))
248 simp-4r 793 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓: 𝑆𝑆)
249248ffnd 6688 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓 Fn 𝑆)
250 elpreima 7035 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑆 → (𝑙 ∈ (𝑓 “ {𝑘}) ↔ (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘})))
251250biimpa 480 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘}))
252 elsni 4598 . . . . . . . . . . . . . . . . 17 ((𝑓𝑙) ∈ {𝑘} → (𝑓𝑙) = 𝑘)
253251, 252simpl2im 511 . . . . . . . . . . . . . . . 16 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
254249, 253sylancom 597 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
255247, 254eleqtrd 2863 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙𝑘)
2568, 2, 4lidlmcl 21275 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ((𝑏𝑙) ∈ 𝐵𝑙𝑘)) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
257236, 237, 243, 255, 256syl22anc 849 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
25849cbvmptv 5203 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑙) · 𝑙))
259257, 258fmptd 7091 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑘})⟶𝑘)
260228mptexd 7204 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
261259ffund 6692 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
262 simp-5r 795 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑏 finSupp 0 )
263 nfv 1933 . . . . . . . . . . . . . . 15 𝑗 𝑘𝑆
26465, 263nfan 1918 . . . . . . . . . . . . . 14 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆)
265 nfcv 2923 . . . . . . . . . . . . . 14 𝑗(𝑓 “ {𝑘})
26635ad7antlr 749 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
267266ffnd 6688 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
26872ad2antrr 736 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
26974a1i 11 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
270241ssdifd 4098 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
271270sselda 3936 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
272267, 268, 269, 271fvdifsupp 8146 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
273272oveq1d 7407 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
27413ad7antr 748 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
275271eldifad 3916 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
276274, 275sseldd 3937 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
277229, 276, 84syl2an2r 695 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
278273, 277eqtrd 2796 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
279264, 265, 69, 278, 228suppss2f 32790 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
280 fsuppsssupp 9324 . . . . . . . . . . . . 13 ((((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
281260, 261, 262, 279, 280syl22anc 849 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
2823, 225, 228, 235, 259, 281gsumsubmcl 19942 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝑘)
283224, 282eqeltrd 2861 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
284283ralrimiva 3153 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
285169, 215, 2843jca 1140 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
28696, 104, 285rspcedvd 3583 . . . . . . 7 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
287286anasss 470 . . . . . 6 (((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ (𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
28824, 287exlimddv 1954 . . . . 5 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
289288anasss 470 . . . 4 (((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ (𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
290289r19.29an 3165 . . 3 ((𝜑 ∧ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
2915ad4antr 742 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ Ring)
292291adantr 484 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
293 eqid 2761 . . . . . . . . . . . . . 14 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
294293zrhrhm 21543 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
295 zringbas 21485 . . . . . . . . . . . . . 14 ℤ = (Base‘ℤring)
296295, 2rhmf 20512 . . . . . . . . . . . . 13 ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
297292, 294, 2963syl 18 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (ℤRHom‘𝑅):ℤ⟶𝐵)
298 simp-5r 795 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
29974a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
300 ssv 3960 . . . . . . . . . . . . . . . . . 18 ran 𝑎 ⊆ V
301 ssdif 4097 . . . . . . . . . . . . . . . . . 18 (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
302300, 301ax-mp 5 . . . . . . . . . . . . . . . . 17 (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
303302sseli 3932 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) → 𝑚 ∈ (V ∖ { 0 }))
304303adantl 485 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑚 ∈ (V ∖ { 0 }))
305 simp-4r 793 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
306298, 299, 304, 305fsuppinisegfi 32839 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑚}) ∈ Fin)
307 hashcl 14366 . . . . . . . . . . . . . 14 ((𝑎 “ {𝑚}) ∈ Fin → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
308306, 307syl 17 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
309308nn0zd 12590 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℤ)
310297, 309ffvelcdmd 7062 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ 𝐵)
311 eqid 2761 . . . . . . . . . . 11 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))
312310, 311fmptd 7091 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
3132, 3ring0cl 20296 . . . . . . . . . . 11 (𝑅 ∈ Ring → 0𝐵)
314 fconst6g 6749 . . . . . . . . . . 11 ( 0𝐵 → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
315291, 313, 3143syl 18 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
316 disjdif 4425 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
317316a1i 11 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
318312, 315, 317fun2d 6724 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
319 simplll 784 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝜑𝑎 ∈ (𝐵m 𝑆)))
32093, 16elmapd 8817 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑎 ∈ (𝐵m 𝑆) ↔ 𝑎:𝑆𝐵))
321320biimpa 480 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → 𝑎:𝑆𝐵)
322319, 321syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎:𝑆𝐵)
323322ffnd 6688 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
324 elssuni 4896 . . . . . . . . . . . . . . . . 17 (𝑘𝑆𝑘 𝑆)
325324adantl 485 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → 𝑘 𝑆)
326325sseld 3935 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → ((𝑎𝑘) ∈ 𝑘 → (𝑎𝑘) ∈ 𝑆))
327326ralimdva 3173 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆))
328327imp 410 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆)
329 fnfvrnss 7098 . . . . . . . . . . . . 13 ((𝑎 Fn 𝑆 ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆) → ran 𝑎 𝑆)
330323, 328, 329syl2anc 593 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ran 𝑎 𝑆)
331330ssdifssd 4100 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝑆)
332 undif 4435 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ⊆ 𝑆 ↔ ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
333331, 332sylib 220 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
334333feq2d 6671 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
335318, 334mpbid 234 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵)
33692a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝐵 ∈ V)
33717ad4antr 742 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆 ∈ V)
338336, 337elmapd 8817 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆) ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
339335, 338mpbird 259 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆))
340 breq1 5102 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
341 fveq1 6862 . . . . . . . . . . . . 13 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
342341oveq1d 7407 . . . . . . . . . . . 12 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
343342mpteq2dv 5193 . . . . . . . . . . 11 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
344343oveq2d 7408 . . . . . . . . . 10 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
345344eqeq2d 2772 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ↔ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
346340, 345anbi12d 641 . . . . . . . 8 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))))
347346adantl 485 . . . . . . 7 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))) → ((𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))))
348318ffund 6692 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })))
349339elexd 3476 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ V)
35074a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 0 ∈ V)
351322ffund 6692 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun 𝑎)
352319simprd 499 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 ∈ (𝐵m 𝑆))
353 simpllr 785 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 finSupp 0 )
354 fsupprnfi 32844 . . . . . . . . . . . . 13 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
355 diffi 9139 . . . . . . . . . . . . 13 (ran 𝑎 ∈ Fin → (ran 𝑎 ∖ { 0 }) ∈ Fin)
356354, 355syl 17 . . . . . . . . . . . 12 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
357351, 352, 350, 353, 356syl22anc 849 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
358312, 357, 350fdmfifsupp 9318 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) finSupp 0 )
35913ssdifssd 4100 . . . . . . . . . . . . 13 (𝜑 → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
360359ad4antr 742 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
361336, 360ssexd 5279 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
362361, 350fczfsuppd 9329 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
363358, 362fsuppun 9330 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
364 funisfsupp 9310 . . . . . . . . . 10 ((Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∧ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ V ∧ 0 ∈ V) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ↔ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin))
365364biimpar 481 . . . . . . . . 9 (((Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∧ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ V ∧ 0 ∈ V) ∧ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
366348, 349, 350, 363, 365syl31anc 1391 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
367 fvex 6876 . . . . . . . . . . . . . . . 16 ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ V
368367, 311fnmpti 6660 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 })
369368a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }))
370 fnconstg 6748 . . . . . . . . . . . . . . . 16 ( 0 ∈ V → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))
37174, 370ax-mp 5 . . . . . . . . . . . . . . 15 (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))
372371a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))
373316a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
374 simpr 488 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (ran 𝑎 ∖ { 0 }))
375369, 372, 373, 374fvun1d 6956 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗))
376 sneq 4591 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → {𝑚} = {𝑗})
377376imaeq2d 6046 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → (𝑎 “ {𝑚}) = (𝑎 “ {𝑗}))
378377fveq2d 6867 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (♯‘(𝑎 “ {𝑚})) = (♯‘(𝑎 “ {𝑗})))
379378fveq2d 6867 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
380 fvexd 6878 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) ∈ V)
381311, 379, 374, 380fvmptd3 6995 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
382375, 381eqtrd 2796 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
383382oveq1d 7407 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))
384383mpteq2dva 5192 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)))
385384oveq2d 7408 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
386291, 27syl 17 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ CMnd)
387316a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
388 fvun2 6955 . . . . . . . . . . . . . . 15 (((𝑚 ∈ (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 })‘𝑗))
389368, 371, 388mp3an12 1471 . . . . . . . . . . . . . 14 ((((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅ ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
390387, 389sylancom 597 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
39174fvconst2 7184 . . . . . . . . . . . . . 14 (𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
392391adantl 485 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
393390, 392eqtrd 2796 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
394393oveq1d 7407 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
395360sselda 3936 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → 𝑗𝐵)
396291, 395, 84syl2an2r 695 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ( 0 · 𝑗) = 0 )
397394, 396eqtrd 2796 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = 0 )
398291adantr 484 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
399335ffvelcdmda 7061 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
40013ad4antr 742 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆𝐵)
401400sselda 3936 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑗𝐵)
4022, 4ringcl 20279 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵𝑗𝐵) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
403398, 399, 401, 402syl3anc 1389 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
4042, 3, 386, 337, 397, 357, 403, 331gsummptres2 33194 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
405 eqid 2761 . . . . . . . . . . 11 (.g𝑅) = (.g𝑅)
4062, 3, 405, 386, 322, 353gsumhashmul 33208 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
407 simplr 778 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg 𝑎))
408291adantr 484 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
409352adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
41074a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
411302, 374sselid 3934 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (V ∖ { 0 }))
412353adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
413409, 410, 411, 412fsuppinisegfi 32839 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑗}) ∈ Fin)
414 hashcl 14366 . . . . . . . . . . . . . . 15 ((𝑎 “ {𝑗}) ∈ Fin → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
415413, 414syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
416415nn0zd 12590 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
417331, 400sstrd 3946 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
418417sselda 3936 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗𝐵)
419 eqid 2761 . . . . . . . . . . . . . . . . 17 (1r𝑅) = (1r𝑅)
420293, 405, 419zrhmulg 21541 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
421420adantr 484 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
422421oveq1d 7407 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗))
423 simpll 776 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑅 ∈ Ring)
424 simplr 778 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
4252, 419ringidcl 20294 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
426425ad2antrr 736 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (1r𝑅) ∈ 𝐵)
427 simpr 488 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑗𝐵)
4282, 405, 4mulgass2 20338 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((♯‘(𝑎 “ {𝑗})) ∈ ℤ ∧ (1r𝑅) ∈ 𝐵𝑗𝐵)) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
429423, 424, 426, 427, 428syl13anc 1390 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
4302, 4, 419ringlidm 20298 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
431423, 430sylancom 597 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
432431oveq2d 7408 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
433422, 429, 4323eqtrd 2800 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
434408, 416, 418, 433syl21anc 848 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
435434mpteq2dva 5192 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗)))
436435oveq2d 7408 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
437406, 407, 4363eqtr4d 2806 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
438385, 404, 4373eqtr4rd 2807 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
439366, 438jca 519 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
440339, 347, 439rspcedvd 3583 . . . . . 6 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
441440exp41 438 . . . . 5 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → (𝑎 finSupp 0 → (𝑋 = (𝑅 Σg 𝑎) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))))
4424413imp2 1362 . . . 4 (((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ (𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
443442r19.29an 3165 . . 3 ((𝜑 ∧ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
444290, 443impbida 810 . 2 (𝜑 → (∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
44514, 444bitrd 281 1 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 399  w3a 1097   = wceq 1559  wex 1798  wcel 2141  wral 3075  wrex 3085  Vcvv 3453  cdif 3901  cun 3902  cin 3903  wss 3904  c0 4285  {csn 4581   cuni 4864   ciun 4948  Disj wdisj 5066   class class class wbr 5099  cmpt 5180   × cxp 5643  ccnv 5644  dom cdm 5645  ran crn 5646  cres 5647  cima 5648  Fun wfun 6511   Fn wfn 6512  wf 6513  cfv 6517  (class class class)co 7392   supp csupp 8135  m cmap 8803  Fincfn 8923   finSupp cfsupp 9304  0cn0 12478  cz 12565  chash 14340  Basecbs 17228  .rcmulr 17270  0gc0g 17451   Σg cgsu 17452  Mndcmnd 18751  SubMndcsubmnd 18799  .gcmg 19092  SubGrpcsubg 19145  CMndccmn 19803  1rcur 20210  Ringcrg 20262   RingHom crh 20497  LIdealclidl 21256  RSpancrsp 21257  ringczring 21478  ℤRHomczrh 21531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-reg 9537  ax-inf2 9593  ax-ac2 10417  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147  ax-addf 11149  ax-mulf 11150
This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-tp 4586  df-op 4588  df-uni 4865  df-int 4905  df-iun 4950  df-iin 4951  df-disj 5067  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-se 5599  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-isom 6526  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-of 7656  df-om 7843  df-1st 7966  df-2nd 7967  df-supp 8136  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-2o 8433  df-er 8673  df-map 8805  df-ixp 8876  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-fsupp 9305  df-sup 9385  df-oi 9455  df-r1 9719  df-rank 9720  df-card 9894  df-ac 10069  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12479  df-z 12566  df-dec 12686  df-uz 12837  df-fz 13510  df-fzo 13657  df-seq 14012  df-hash 14341  df-struct 17166  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17250  df-plusg 17282  df-mulr 17283  df-starv 17284  df-sca 17285  df-vsca 17286  df-ip 17287  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-hom 17293  df-cco 17294  df-0g 17453  df-gsum 17454  df-prds 17459  df-pws 17461  df-mre 17597  df-mrc 17598  df-acs 17600  df-mgm 18657  df-sgrp 18736  df-mnd 18752  df-mhm 18800  df-submnd 18801  df-grp 18961  df-minusg 18962  df-sbg 18963  df-mulg 19093  df-subg 19148  df-ghm 19237  df-cntz 19340  df-cmn 19805  df-abl 19806  df-mgp 20170  df-rng 20182  df-ur 20211  df-ring 20264  df-cring 20265  df-rhm 20500  df-nzr 20542  df-subrng 20575  df-subrg 20599  df-lmod 20909  df-lss 20979  df-lsp 21019  df-lmhm 21069  df-lbs 21122  df-sra 21220  df-rgmod 21221  df-lidl 21258  df-rsp 21259  df-cnfld 21405  df-zring 21479  df-zrh 21535  df-dsmm 21764  df-frlm 21779  df-uvc 21815
This theorem is referenced by:  zarcmplem  34139
  Copyright terms: Public domain W3C validator