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 33518
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 3922 . . . . . 6 ((𝜑𝑖𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8 eqid 2740 . . . . . . 7 (LIdeal‘𝑅) = (LIdeal‘𝑅)
92, 8lidlss 21212 . . . . . 6 (𝑖 ∈ (LIdeal‘𝑅) → 𝑖𝐵)
107, 9syl 17 . . . . 5 ((𝜑𝑖𝑆) → 𝑖𝐵)
1110ralrimiva 3132 . . . 4 (𝜑 → ∀𝑖𝑆 𝑖𝐵)
12 unissb 4878 . . . 4 ( 𝑆𝐵 ↔ ∀𝑖𝑆 𝑖𝐵)
1311, 12sylibr 235 . . 3 (𝜑 𝑆𝐵)
141, 2, 3, 4, 5, 13elrsp 33462 . 2 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))
15 fvexd 6849 . . . . . . . . . 10 (𝜑 → (LIdeal‘𝑅) ∈ V)
1615, 6ssexd 5259 . . . . . . . . 9 (𝜑𝑆 ∈ V)
1716uniexd 7692 . . . . . . . 8 (𝜑 𝑆 ∈ V)
18 eluni2 4849 . . . . . . . . . 10 (𝑗 𝑆 ↔ ∃𝑖𝑆 𝑗𝑖)
1918bilani 505 . . . . . . . . 9 ((𝜑𝑗 𝑆) → ∃𝑖𝑆 𝑗𝑖)
2019ralrimiva 3132 . . . . . . . 8 (𝜑 → ∀𝑗 𝑆𝑖𝑆 𝑗𝑖)
21 eleq2 2829 . . . . . . . . 9 (𝑖 = (𝑓𝑗) → (𝑗𝑖𝑗 ∈ (𝑓𝑗)))
2221ac6sg 10408 . . . . . . . 8 ( 𝑆 ∈ V → (∀𝑗 𝑆𝑖𝑆 𝑗𝑖 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))))
2317, 20, 22sylc 65 . . . . . . 7 (𝜑 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
2423ad3antrrr 736 . . . . . 6 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
25 simp-5l 790 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝜑)
2625adantr 481 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝜑)
27 ringcmn 20261 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
2826, 5, 273syl 18 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑅 ∈ CMnd)
29 vex 3436 . . . . . . . . . . . . 13 𝑓 ∈ V
30 cnvexg 7871 . . . . . . . . . . . . 13 (𝑓 ∈ V → 𝑓 ∈ V)
31 imaexg 7860 . . . . . . . . . . . . 13 (𝑓 ∈ V → (𝑓 “ {𝑖}) ∈ V)
3229, 30, 31mp2b 10 . . . . . . . . . . . 12 (𝑓 “ {𝑖}) ∈ V
3332a1i 11 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ∈ V)
345ad7antr 744 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
35 elmapi 8793 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵m 𝑆) → 𝑏: 𝑆𝐵)
3635ad7antlr 745 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑏: 𝑆𝐵)
37 cnvimass 6041 . . . . . . . . . . . . . . . . 17 (𝑓 “ {𝑖}) ⊆ dom 𝑓
38 fdm 6671 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → dom 𝑓 = 𝑆)
3937, 38sseqtrid 3964 . . . . . . . . . . . . . . . 16 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑖}) ⊆ 𝑆)
4039ad3antlr 737 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ⊆ 𝑆)
4140sselda 3922 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙 𝑆)
4236, 41ffvelcdmd 7033 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → (𝑏𝑙) ∈ 𝐵)
4313ad7antr 744 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
4443, 41sseldd 3923 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙𝐵)
452, 4ringcl 20229 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑙) ∈ 𝐵𝑙𝐵) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
4634, 42, 44, 45syl3anc 1379 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
47 fveq2 6834 . . . . . . . . . . . . . 14 (𝑗 = 𝑙 → (𝑏𝑗) = (𝑏𝑙))
48 id 22 . . . . . . . . . . . . . 14 (𝑗 = 𝑙𝑗 = 𝑙)
4947, 48oveq12d 7381 . . . . . . . . . . . . 13 (𝑗 = 𝑙 → ((𝑏𝑗) · 𝑗) = ((𝑏𝑙) · 𝑙))
5049cbvmptv 5183 . . . . . . . . . . . 12 (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑙) · 𝑙))
5146, 50fmptd 7062 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑖})⟶𝐵)
5233mptexd 7175 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
5351ffund 6666 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
54 simp-5r 791 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑏 finSupp 0 )
55 nfv 1921 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 )
56 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑗𝑅
57 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑗 Σg
58 nfmpt1 5178 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
5956, 57, 58nfov 7393 . . . . . . . . . . . . . . . . . 18 𝑗(𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6059nfeq2 2919 . . . . . . . . . . . . . . . . 17 𝑗 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6155, 60nfan 1906 . . . . . . . . . . . . . . . 16 𝑗(((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
62 nfv 1921 . . . . . . . . . . . . . . . 16 𝑗 𝑓: 𝑆𝑆
6361, 62nfan 1906 . . . . . . . . . . . . . . 15 𝑗((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆)
64 nfra1 3264 . . . . . . . . . . . . . . 15 𝑗𝑗 𝑆𝑗 ∈ (𝑓𝑗)
6563, 64nfan 1906 . . . . . . . . . . . . . 14 𝑗(((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
66 nfv 1921 . . . . . . . . . . . . . 14 𝑗 𝑖𝑆
6765, 66nfan 1906 . . . . . . . . . . . . 13 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆)
68 nfcv 2902 . . . . . . . . . . . . 13 𝑗(𝑓 “ {𝑖})
69 nfcv 2902 . . . . . . . . . . . . 13 𝑗(𝑏 supp 0 )
7035ad7antlr 745 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
7170ffnd 6663 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
7225, 17syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
7372ad2antrr 732 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
743fvexi 6848 . . . . . . . . . . . . . . . . 17 0 ∈ V
7574a1i 11 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
7640ssdifd 4082 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
7776sselda 3922 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
7871, 73, 75, 77fvdifsupp 8118 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
7978oveq1d 7378 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
805ad7antr 744 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
8113ad7antr 744 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
8277eldifad 3902 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
8381, 82sseldd 3923 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
842, 4, 3ringlz 20272 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ( 0 · 𝑗) = 0 )
8580, 83, 84syl2anc 590 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
8679, 85eqtrd 2775 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
8767, 68, 69, 86, 33suppss2f 32737 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
88 fsuppsssupp 9291 . . . . . . . . . . . 12 ((((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
8952, 53, 54, 87, 88syl22anc 844 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
902, 3, 28, 33, 51, 89gsumcl 19888 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝐵)
9190fmpttd 7063 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵)
922fvexi 6848 . . . . . . . . . . . 12 𝐵 ∈ V
9392a1i 11 . . . . . . . . . . 11 (𝜑𝐵 ∈ V)
9493, 16elmapd 8784 . . . . . . . . . 10 (𝜑 → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆) ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵))
9594biimpar 478 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
9625, 91, 95syl2anc 590 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
97 breq1 5082 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ))
98 oveq2 7371 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
9998eqeq2d 2751 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σg 𝑎) ↔ 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))))
100 fveq1 6833 . . . . . . . . . . . 12 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎𝑘) = ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘))
101100eleq1d 2825 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎𝑘) ∈ 𝑘 ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
102101ralbidv 3163 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 ↔ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
10397, 99, 1023anbi123d 1444 . . . . . . . . 9 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
104103adantl 482 . . . . . . . 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 7175 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V)
10774a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 0 ∈ V)
108 funmpt 6530 . . . . . . . . . . 11 Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
109108a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
110 simplr 774 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑓: 𝑆𝑆)
111110ffund 6666 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun 𝑓)
112 simp-4r 789 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏 finSupp 0 )
113112fsuppimpd 9279 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑏 supp 0 ) ∈ Fin)
114 imafi 9222 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
115111, 113, 114syl2anc 590 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
116 nfv 1921 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
11765, 116nfan 1906 . . . . . . . . . . . . . . 15 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
118 simpllr 781 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓: 𝑆𝑆)
119118ffund 6666 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
120 snssi 4724 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
121120adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
122 sspreima 7016 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
123119, 121, 122syl2anc 590 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
124 difpreima 7013 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝑓 → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
125119, 124syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
126123, 125sseqtrd 3958 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
127 suppssdm 8124 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 supp 0 ) ⊆ dom 𝑏
12835ad6antlr 743 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏: 𝑆𝐵)
129127, 128fssdm 6681 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ 𝑆)
130118fdmd 6672 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = 𝑆)
131129, 130sseqtrrd 3959 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
132 sseqin2 4159 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
133132biimpi 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
134 dminss 6111 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))
135133, 134eqsstrrdi 3967 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
136131, 135syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
137136sscond 4083 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
138126, 137sstrd 3932 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
139 fimacnv 6684 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓: 𝑆𝑆 → (𝑓𝑆) = 𝑆)
140118, 139syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓𝑆) = 𝑆)
141140difeq1d 4063 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑏 supp 0 )) = ( 𝑆 ∖ (𝑏 supp 0 )))
142138, 141sseqtrd 3958 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
143142sselda 3922 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
144 ssidd 3945 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑏 supp 0 ))
14572adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑆 ∈ V)
14674a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 0 ∈ V)
147128, 144, 145, 146suppssr 8142 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
148143, 147syldan 597 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → (𝑏𝑗) = 0 )
149148oveq1d 7378 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1505ad7antr 744 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
15113ad7antr 744 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
15239ad3antlr 737 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ 𝑆)
153152sselda 3922 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 𝑆)
154151, 153sseldd 3923 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗𝐵)
155150, 154, 84syl2anc 590 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ( 0 · 𝑗) = 0 )
156149, 155eqtrd 2775 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = 0 )
157117, 156mpteq2da 5171 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 ))
158157oveq2d 7379 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )))
1595, 27syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ CMnd)
160159cmnmndd 19777 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ Mnd)
161160ad6antr 742 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
1623gsumz 18802 . . . . . . . . . . . . . 14 ((𝑅 ∈ Mnd ∧ (𝑓 “ {𝑖}) ∈ V) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
163161, 32, 162sylancl 592 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
164158, 163eqtrd 2775 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = 0 )
165164, 105suppss2 8147 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
166115, 165ssfid 9176 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
167 isfsupp 9275 . . . . . . . . . . 11 (((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ↔ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)))
168167biimpar 478 . . . . . . . . . 10 ((((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) ∧ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
169106, 107, 109, 166, 168syl22anc 844 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
170 simpllr 781 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
17125, 159syl 17 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑅 ∈ CMnd)
1725ad6antr 742 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
17335ad5antlr 741 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏: 𝑆𝐵)
174173ffvelcdmda 7032 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → (𝑏𝑗) ∈ 𝐵)
17525, 13syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆𝐵)
176175sselda 3922 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑗𝐵)
1772, 4ringcl 20229 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑗) ∈ 𝐵𝑗𝐵) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
178172, 174, 176, 177syl3anc 1379 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
179 eqid 2740 . . . . . . . . . . . 12 (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
18065, 178, 179fmptdf 7065 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)): 𝑆𝐵)
18172mptexd 7175 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
182 funmpt 6530 . . . . . . . . . . . . 13 Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
183182a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
184 nfcv 2902 . . . . . . . . . . . . 13 𝑗 𝑆
185173adantr 481 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
186185ffnd 6663 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
18772adantr 481 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
18874a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 0 ∈ V)
189 simpr 485 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
190186, 187, 188, 189fvdifsupp 8118 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
191190oveq1d 7378 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1925ad6antr 742 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
193175adantr 481 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
194189eldifad 3902 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
195193, 194sseldd 3923 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
196192, 195, 84syl2anc 590 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
197191, 196eqtrd 2775 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
19865, 184, 69, 197, 72suppss2f 32737 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
199 fsuppsssupp 9291 . . . . . . . . . . . 12 ((((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
200181, 183, 112, 198, 199syl22anc 844 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
201 sndisj 5071 . . . . . . . . . . . 12 Disj 𝑖𝑆 {𝑖}
202 disjpreima 32680 . . . . . . . . . . . 12 ((Fun 𝑓Disj 𝑖𝑆 {𝑖}) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
203111, 201, 202sylancl 592 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
204 iunid 4997 . . . . . . . . . . . . 13 𝑖𝑆 {𝑖} = 𝑆
205204imaeq2i 6017 . . . . . . . . . . . 12 (𝑓 𝑖𝑆 {𝑖}) = (𝑓𝑆)
206 iunpreima 32660 . . . . . . . . . . . . 13 (Fun 𝑓 → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
207111, 206syl 17 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
208139ad2antlr 733 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓𝑆) = 𝑆)
209205, 207, 2083eqtr3a 2799 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑖𝑆 (𝑓 “ {𝑖}) = 𝑆)
2102, 3, 171, 72, 105, 180, 200, 203, 209gsumpart 33151 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))))
21140resmptd 5999 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
212211oveq2d 7379 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
213212mpteq2dva 5172 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
214213oveq2d 7379 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
215170, 210, 2143eqtrd 2779 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
216 eqid 2740 . . . . . . . . . . . 12 (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
217 simpr 485 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
218217sneqd 4574 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
219218imaeq2d 6019 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑓 “ {𝑖}) = (𝑓 “ {𝑘}))
220219mpteq1d 5169 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
221220oveq2d 7379 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
222 simpr 485 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘𝑆)
223 ovexd 7398 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ V)
224216, 221, 222, 223fvmptd2 6951 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
225159ad6antr 742 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ CMnd)
22629cnvex 7872 . . . . . . . . . . . . . 14 𝑓 ∈ V
227226imaex 7861 . . . . . . . . . . . . 13 (𝑓 “ {𝑘}) ∈ V
228227a1i 11 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ∈ V)
2295ad6antr 742 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ Ring)
23025, 6syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ⊆ (LIdeal‘𝑅))
231230sselda 3922 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
2328lidlsubg 21223 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
233 subgsubm 19122 . . . . . . . . . . . . . 14 (𝑘 ∈ (SubGrp‘𝑅) → 𝑘 ∈ (SubMnd‘𝑅))
234232, 233syl 17 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubMnd‘𝑅))
235229, 231, 234syl2anc 590 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (SubMnd‘𝑅))
236229adantr 481 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑅 ∈ Ring)
237231adantr 481 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑘 ∈ (LIdeal‘𝑅))
23835ad7antlr 745 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑏: 𝑆𝐵)
239 cnvimass 6041 . . . . . . . . . . . . . . . . . 18 (𝑓 “ {𝑘}) ⊆ dom 𝑓
240239, 38sseqtrid 3964 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑘}) ⊆ 𝑆)
241240ad3antlr 737 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ⊆ 𝑆)
242241sselda 3922 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 𝑆)
243238, 242ffvelcdmd 7033 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑏𝑙) ∈ 𝐵)
244 fveq2 6834 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑙 → (𝑓𝑗) = (𝑓𝑙))
24548, 244eleq12d 2834 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑙 → (𝑗 ∈ (𝑓𝑗) ↔ 𝑙 ∈ (𝑓𝑙)))
246 simpllr 781 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
247245, 246, 242rspcdva 3568 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓𝑙))
248 simp-4r 789 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓: 𝑆𝑆)
249248ffnd 6663 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓 Fn 𝑆)
250 elpreima 7006 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑆 → (𝑙 ∈ (𝑓 “ {𝑘}) ↔ (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘})))
251250biimpa 477 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘}))
252 elsni 4579 . . . . . . . . . . . . . . . . 17 ((𝑓𝑙) ∈ {𝑘} → (𝑓𝑙) = 𝑘)
253251, 252simpl2im 508 . . . . . . . . . . . . . . . 16 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
254249, 253sylancom 594 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
255247, 254eleqtrd 2842 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙𝑘)
2568, 2, 4lidlmcl 21225 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ((𝑏𝑙) ∈ 𝐵𝑙𝑘)) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
257236, 237, 243, 255, 256syl22anc 844 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
25849cbvmptv 5183 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑙) · 𝑙))
259257, 258fmptd 7062 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑘})⟶𝑘)
260228mptexd 7175 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
261259ffund 6666 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
262 simp-5r 791 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑏 finSupp 0 )
263 nfv 1921 . . . . . . . . . . . . . . 15 𝑗 𝑘𝑆
26465, 263nfan 1906 . . . . . . . . . . . . . 14 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆)
265 nfcv 2902 . . . . . . . . . . . . . 14 𝑗(𝑓 “ {𝑘})
26635ad7antlr 745 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
267266ffnd 6663 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
26872ad2antrr 732 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
26974a1i 11 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
270241ssdifd 4082 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
271270sselda 3922 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
272267, 268, 269, 271fvdifsupp 8118 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
273272oveq1d 7378 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
27413ad7antr 744 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
275271eldifad 3902 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
276274, 275sseldd 3923 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
277229, 276, 84syl2an2r 691 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
278273, 277eqtrd 2775 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
279264, 265, 69, 278, 228suppss2f 32737 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
280 fsuppsssupp 9291 . . . . . . . . . . . . 13 ((((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
281260, 261, 262, 279, 280syl22anc 844 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
2823, 225, 228, 235, 259, 281gsumsubmcl 19892 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝑘)
283224, 282eqeltrd 2840 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
284283ralrimiva 3132 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
285169, 215, 2843jca 1134 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
28696, 104, 285rspcedvd 3569 . . . . . . 7 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
287286anasss 467 . . . . . 6 (((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ (𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
28824, 287exlimddv 1942 . . . . 5 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
289288anasss 467 . . . 4 (((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ (𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
290289r19.29an 3144 . . 3 ((𝜑 ∧ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
2915ad4antr 738 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ Ring)
292291adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
293 eqid 2740 . . . . . . . . . . . . . 14 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
294293zrhrhm 21493 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
295 zringbas 21435 . . . . . . . . . . . . . 14 ℤ = (Base‘ℤring)
296295, 2rhmf 20462 . . . . . . . . . . . . 13 ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
297292, 294, 2963syl 18 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (ℤRHom‘𝑅):ℤ⟶𝐵)
298 simp-5r 791 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
29974a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
300 ssv 3946 . . . . . . . . . . . . . . . . . 18 ran 𝑎 ⊆ V
301 ssdif 4081 . . . . . . . . . . . . . . . . . 18 (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
302300, 301ax-mp 5 . . . . . . . . . . . . . . . . 17 (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
303302sseli 3918 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) → 𝑚 ∈ (V ∖ { 0 }))
304303adantl 482 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑚 ∈ (V ∖ { 0 }))
305 simp-4r 789 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
306298, 299, 304, 305fsuppinisegfi 32786 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑚}) ∈ Fin)
307 hashcl 14316 . . . . . . . . . . . . . 14 ((𝑎 “ {𝑚}) ∈ Fin → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
308306, 307syl 17 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
309308nn0zd 12547 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℤ)
310297, 309ffvelcdmd 7033 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ 𝐵)
311 eqid 2740 . . . . . . . . . . 11 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))
312310, 311fmptd 7062 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
3132, 3ring0cl 20246 . . . . . . . . . . 11 (𝑅 ∈ Ring → 0𝐵)
314 fconst6g 6723 . . . . . . . . . . 11 ( 0𝐵 → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
315291, 313, 3143syl 18 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
316 disjdif 4407 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
317316a1i 11 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
318312, 315, 317fun2d 6698 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
319 simplll 780 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝜑𝑎 ∈ (𝐵m 𝑆)))
32093, 16elmapd 8784 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑎 ∈ (𝐵m 𝑆) ↔ 𝑎:𝑆𝐵))
321320biimpa 477 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → 𝑎:𝑆𝐵)
322319, 321syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎:𝑆𝐵)
323322ffnd 6663 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
324 elssuni 4876 . . . . . . . . . . . . . . . . 17 (𝑘𝑆𝑘 𝑆)
325324adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → 𝑘 𝑆)
326325sseld 3921 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → ((𝑎𝑘) ∈ 𝑘 → (𝑎𝑘) ∈ 𝑆))
327326ralimdva 3152 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆))
328327imp 407 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆)
329 fnfvrnss 7069 . . . . . . . . . . . . 13 ((𝑎 Fn 𝑆 ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆) → ran 𝑎 𝑆)
330323, 328, 329syl2anc 590 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ran 𝑎 𝑆)
331330ssdifssd 4084 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝑆)
332 undif 4417 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ⊆ 𝑆 ↔ ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
333331, 332sylib 219 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
334333feq2d 6646 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
335318, 334mpbid 233 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵)
33692a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝐵 ∈ V)
33717ad4antr 738 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆 ∈ V)
338336, 337elmapd 8784 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆) ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
339335, 338mpbird 258 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆))
340 breq1 5082 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
341 fveq1 6833 . . . . . . . . . . . . 13 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
342341oveq1d 7378 . . . . . . . . . . . 12 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
343342mpteq2dv 5173 . . . . . . . . . . 11 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
344343oveq2d 7379 . . . . . . . . . 10 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
345344eqeq2d 2751 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ↔ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
346340, 345anbi12d 638 . . . . . . . 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 482 . . . . . . 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 6666 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })))
349339elexd 3456 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ V)
35074a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 0 ∈ V)
351322ffund 6666 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun 𝑎)
352319simprd 496 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 ∈ (𝐵m 𝑆))
353 simpllr 781 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 finSupp 0 )
354 fsupprnfi 32791 . . . . . . . . . . . . 13 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
355 diffi 9106 . . . . . . . . . . . . 13 (ran 𝑎 ∈ Fin → (ran 𝑎 ∖ { 0 }) ∈ Fin)
356354, 355syl 17 . . . . . . . . . . . 12 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
357351, 352, 350, 353, 356syl22anc 844 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
358312, 357, 350fdmfifsupp 9285 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) finSupp 0 )
35913ssdifssd 4084 . . . . . . . . . . . . 13 (𝜑 → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
360359ad4antr 738 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
361336, 360ssexd 5259 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
362361, 350fczfsuppd 9296 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
363358, 362fsuppun 9297 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
364 funisfsupp 9277 . . . . . . . . . 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 478 . . . . . . . . 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 1381 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
367 fvex 6847 . . . . . . . . . . . . . . . 16 ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ V
368367, 311fnmpti 6635 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 })
369368a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }))
370 fnconstg 6722 . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (ran 𝑎 ∖ { 0 }))
375369, 372, 373, 374fvun1d 6927 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗))
376 sneq 4572 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → {𝑚} = {𝑗})
377376imaeq2d 6019 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → (𝑎 “ {𝑚}) = (𝑎 “ {𝑗}))
378377fveq2d 6838 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (♯‘(𝑎 “ {𝑚})) = (♯‘(𝑎 “ {𝑗})))
379378fveq2d 6838 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
380 fvexd 6849 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) ∈ V)
381311, 379, 374, 380fvmptd3 6966 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
382375, 381eqtrd 2775 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
383382oveq1d 7378 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))
384383mpteq2dva 5172 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)))
385384oveq2d 7379 . . . . . . . . 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 6926 . . . . . . . . . . . . . . 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 1459 . . . . . . . . . . . . . 14 ((((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅ ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
390387, 389sylancom 594 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
39174fvconst2 7155 . . . . . . . . . . . . . 14 (𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
392391adantl 482 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
393390, 392eqtrd 2775 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
394393oveq1d 7378 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
395360sselda 3922 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → 𝑗𝐵)
396291, 395, 84syl2an2r 691 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ( 0 · 𝑗) = 0 )
397394, 396eqtrd 2775 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = 0 )
398291adantr 481 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
399335ffvelcdmda 7032 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
40013ad4antr 738 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆𝐵)
401400sselda 3922 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑗𝐵)
4022, 4ringcl 20229 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵𝑗𝐵) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
403398, 399, 401, 402syl3anc 1379 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
4042, 3, 386, 337, 397, 357, 403, 331gsummptres2 33141 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
405 eqid 2740 . . . . . . . . . . 11 (.g𝑅) = (.g𝑅)
4062, 3, 405, 386, 322, 353gsumhashmul 33155 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
407 simplr 774 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg 𝑎))
408291adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
409352adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
41074a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
411302, 374sselid 3920 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (V ∖ { 0 }))
412353adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
413409, 410, 411, 412fsuppinisegfi 32786 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑗}) ∈ Fin)
414 hashcl 14316 . . . . . . . . . . . . . . 15 ((𝑎 “ {𝑗}) ∈ Fin → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
415413, 414syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
416415nn0zd 12547 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
417331, 400sstrd 3932 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
418417sselda 3922 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗𝐵)
419 eqid 2740 . . . . . . . . . . . . . . . . 17 (1r𝑅) = (1r𝑅)
420293, 405, 419zrhmulg 21491 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
421420adantr 481 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
422421oveq1d 7378 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗))
423 simpll 772 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑅 ∈ Ring)
424 simplr 774 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
4252, 419ringidcl 20244 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
426425ad2antrr 732 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (1r𝑅) ∈ 𝐵)
427 simpr 485 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑗𝐵)
4282, 405, 4mulgass2 20288 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((♯‘(𝑎 “ {𝑗})) ∈ ℤ ∧ (1r𝑅) ∈ 𝐵𝑗𝐵)) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
429423, 424, 426, 427, 428syl13anc 1380 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
4302, 4, 419ringlidm 20248 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
431423, 430sylancom 594 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
432431oveq2d 7379 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
433422, 429, 4323eqtrd 2779 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
434408, 416, 418, 433syl21anc 843 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
435434mpteq2dva 5172 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗)))
436435oveq2d 7379 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
437406, 407, 4363eqtr4d 2785 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
438385, 404, 4373eqtr4rd 2786 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
439366, 438jca 516 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
440339, 347, 439rspcedvd 3569 . . . . . 6 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
441440exp41 435 . . . . 5 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → (𝑎 finSupp 0 → (𝑋 = (𝑅 Σg 𝑎) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))))
4424413imp2 1356 . . . 4 (((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ (𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
443442r19.29an 3144 . . 3 ((𝜑 ∧ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
444290, 443impbida 806 . 2 (𝜑 → (∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
44514, 444bitrd 280 1 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1092   = wceq 1547  wex 1786  wcel 2119  wral 3054  wrex 3064  Vcvv 3432  cdif 3887  cun 3888  cin 3889  wss 3890  c0 4268  {csn 4562   cuni 4845   ciun 4928  Disj wdisj 5046   class class class wbr 5079  cmpt 5160   × cxp 5623  ccnv 5624  dom cdm 5625  ran crn 5626  cres 5627  cima 5628  Fun wfun 6486   Fn wfn 6487  wf 6488  cfv 6492  (class class class)co 7363   supp csupp 8107  m cmap 8770  Fincfn 8890   finSupp cfsupp 9271  0cn0 12435  cz 12522  chash 14290  Basecbs 17177  .rcmulr 17219  0gc0g 17400   Σg cgsu 17401  Mndcmnd 18700  SubMndcsubmnd 18748  .gcmg 19041  SubGrpcsubg 19094  CMndccmn 19753  1rcur 20160  Ringcrg 20212   RingHom crh 20447  LIdealclidl 21206  RSpancrsp 21207  ringczring 21428  ℤRHomczrh 21481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-reg 9504  ax-inf2 9560  ax-ac2 10383  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113  ax-addf 11115  ax-mulf 11116
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-iin 4931  df-disj 5047  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-of 7627  df-om 7814  df-1st 7938  df-2nd 7939  df-supp 8108  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-er 8640  df-map 8772  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9272  df-sup 9352  df-oi 9422  df-r1 9686  df-rank 9687  df-card 9861  df-ac 10036  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-3 12243  df-4 12244  df-5 12245  df-6 12246  df-7 12247  df-8 12248  df-9 12249  df-n0 12436  df-z 12523  df-dec 12643  df-uz 12787  df-fz 13460  df-fzo 13607  df-seq 13962  df-hash 14291  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-mulr 17232  df-starv 17233  df-sca 17234  df-vsca 17235  df-ip 17236  df-tset 17237  df-ple 17238  df-ds 17240  df-unif 17241  df-hom 17242  df-cco 17243  df-0g 17402  df-gsum 17403  df-prds 17408  df-pws 17410  df-mre 17546  df-mrc 17547  df-acs 17549  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-mhm 18749  df-submnd 18750  df-grp 18910  df-minusg 18911  df-sbg 18912  df-mulg 19042  df-subg 19097  df-ghm 19186  df-cntz 19290  df-cmn 19755  df-abl 19756  df-mgp 20120  df-rng 20132  df-ur 20161  df-ring 20214  df-cring 20215  df-rhm 20450  df-nzr 20492  df-subrng 20525  df-subrg 20549  df-lmod 20859  df-lss 20929  df-lsp 20969  df-lmhm 21019  df-lbs 21072  df-sra 21170  df-rgmod 21171  df-lidl 21208  df-rsp 21209  df-cnfld 21355  df-zring 21429  df-zrh 21485  df-dsmm 21714  df-frlm 21729  df-uvc 21765
This theorem is referenced by:  zarcmplem  34072
  Copyright terms: Public domain W3C validator