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 33864
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 3934 . . . . . 6 ((𝜑𝑖𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8 eqid 2762 . . . . . . 7 (LIdeal‘𝑅) = (LIdeal‘𝑅)
92, 8lidlss 21405 . . . . . 6 (𝑖 ∈ (LIdeal‘𝑅) → 𝑖𝐵)
107, 9syl 18 . . . . 5 ((𝜑𝑖𝑆) → 𝑖𝐵)
1110ralrimiva 3156 . . . 4 (𝜑 → ∀𝑖𝑆 𝑖𝐵)
12 unissb 4904 . . . 4 ( 𝑆𝐵 ↔ ∀𝑖𝑆 𝑖𝐵)
1311, 12sylibr 237 . . 3 (𝜑 𝑆𝐵)
141, 2, 3, 4, 5, 13elrsp 33814 . 2 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))
15 fvexd 6897 . . . . . . . . . 10 (𝜑 → (LIdeal‘𝑅) ∈ V)
1615, 6ssexd 5293 . . . . . . . . 9 (𝜑𝑆 ∈ V)
1716uniexd 7748 . . . . . . . 8 (𝜑 𝑆 ∈ V)
18 eluni2 4874 . . . . . . . . . 10 (𝑗 𝑆 ↔ ∃𝑖𝑆 𝑗𝑖)
1918bilani 510 . . . . . . . . 9 ((𝜑𝑗 𝑆) → ∃𝑖𝑆 𝑗𝑖)
2019ralrimiva 3156 . . . . . . . 8 (𝜑 → ∀𝑗 𝑆𝑖𝑆 𝑗𝑖)
21 eleq2 2851 . . . . . . . . 9 (𝑖 = (𝑓𝑗) → (𝑗𝑖𝑗 ∈ (𝑓𝑗)))
2221ac6sg 10494 . . . . . . . 8 ( 𝑆 ∈ V → (∀𝑗 𝑆𝑖𝑆 𝑗𝑖 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))))
2317, 20, 22sylc 66 . . . . . . 7 (𝜑 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
2423ad3antrrr 743 . . . . . 6 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
25 simp-5l 797 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝜑)
2625adantr 486 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝜑)
27 ringcmn 20429 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
2826, 5, 273syl 19 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑅 ∈ CMnd)
29 vex 3457 . . . . . . . . . . . . 13 𝑓 ∈ V
30 cnvexg 7925 . . . . . . . . . . . . 13 (𝑓 ∈ V → 𝑓 ∈ V)
31 imaexg 7914 . . . . . . . . . . . . 13 (𝑓 ∈ V → (𝑓 “ {𝑖}) ∈ V)
3229, 30, 31mp2b 10 . . . . . . . . . . . 12 (𝑓 “ {𝑖}) ∈ V
3332a1i 11 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ∈ V)
345ad7antr 751 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
35 elmapi 8852 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵m 𝑆) → 𝑏: 𝑆𝐵)
3635ad7antlr 752 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑏: 𝑆𝐵)
37 cnvimass 6082 . . . . . . . . . . . . . . . . 17 (𝑓 “ {𝑖}) ⊆ dom 𝑓
38 fdm 6716 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → dom 𝑓 = 𝑆)
3937, 38sseqtrid 3976 . . . . . . . . . . . . . . . 16 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑖}) ⊆ 𝑆)
4039ad3antlr 744 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ⊆ 𝑆)
4140sselda 3934 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙 𝑆)
4236, 41ffvelcdmd 7082 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → (𝑏𝑙) ∈ 𝐵)
4313ad7antr 751 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
4443, 41sseldd 3935 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙𝐵)
452, 4ringcl 20395 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑙) ∈ 𝐵𝑙𝐵) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
4634, 42, 44, 45syl3anc 1398 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
47 fveq2 6882 . . . . . . . . . . . . . 14 (𝑗 = 𝑙 → (𝑏𝑗) = (𝑏𝑙))
48 id 23 . . . . . . . . . . . . . 14 (𝑗 = 𝑙𝑗 = 𝑙)
4947, 48oveq12d 7435 . . . . . . . . . . . . 13 (𝑗 = 𝑙 → ((𝑏𝑗) · 𝑗) = ((𝑏𝑙) · 𝑙))
5049cbvmptv 5213 . . . . . . . . . . . 12 (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑙) · 𝑙))
5146, 50fmptd 7111 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑖})⟶𝐵)
5233mptexd 7227 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
5351ffund 6711 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
54 simp-5r 798 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑏 finSupp 0 )
55 nfv 1947 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 )
56 nfcv 2924 . . . . . . . . . . . . . . . . . . 19 𝑗𝑅
57 nfcv 2924 . . . . . . . . . . . . . . . . . . 19 𝑗 Σg
58 nfmpt1 5208 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
5956, 57, 58nfov 7447 . . . . . . . . . . . . . . . . . 18 𝑗(𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6059nfeq2 2941 . . . . . . . . . . . . . . . . 17 𝑗 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6155, 60nfan 1932 . . . . . . . . . . . . . . . 16 𝑗(((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
62 nfv 1947 . . . . . . . . . . . . . . . 16 𝑗 𝑓: 𝑆𝑆
6361, 62nfan 1932 . . . . . . . . . . . . . . 15 𝑗((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆)
64 nfra1 3288 . . . . . . . . . . . . . . 15 𝑗𝑗 𝑆𝑗 ∈ (𝑓𝑗)
6563, 64nfan 1932 . . . . . . . . . . . . . 14 𝑗(((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
66 nfv 1947 . . . . . . . . . . . . . 14 𝑗 𝑖𝑆
6765, 66nfan 1932 . . . . . . . . . . . . 13 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆)
68 nfcv 2924 . . . . . . . . . . . . 13 𝑗(𝑓 “ {𝑖})
69 nfcv 2924 . . . . . . . . . . . . 13 𝑗(𝑏 supp 0 )
7035ad7antlr 752 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
7170ffnd 6707 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
7225, 17syl 18 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
7372ad2antrr 739 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
743fvexi 6896 . . . . . . . . . . . . . . . . 17 0 ∈ V
7574a1i 11 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
7640ssdifd 4095 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
7776sselda 3934 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
7871, 73, 75, 77fvdifsupp 8173 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
7978oveq1d 7432 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
805ad7antr 751 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
8113ad7antr 751 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
8277eldifad 3914 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
8381, 82sseldd 3935 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
842, 4, 3ringlz 20441 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ( 0 · 𝑗) = 0 )
8580, 83, 84syl2anc 596 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
8679, 85eqtrd 2797 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
8767, 68, 69, 86, 33suppss2f 33119 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
88 fsuppsssupp 9355 . . . . . . . . . . . 12 ((((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
8952, 53, 54, 87, 88syl22anc 852 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
902, 3, 28, 33, 51, 89gsumcl 20048 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝐵)
9190fmpttd 7112 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵)
922fvexi 6896 . . . . . . . . . . . 12 𝐵 ∈ V
9392a1i 11 . . . . . . . . . . 11 (𝜑𝐵 ∈ V)
9493, 16elmapd 8843 . . . . . . . . . 10 (𝜑 → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆) ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵))
9594biimpar 483 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
9625, 91, 95syl2anc 596 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
97 breq1 5110 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ))
98 oveq2 7425 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
9998eqeq2d 2773 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σg 𝑎) ↔ 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))))
100 fveq1 6881 . . . . . . . . . . . 12 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎𝑘) = ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘))
101100eleq1d 2847 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎𝑘) ∈ 𝑘 ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
102101ralbidv 3187 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 ↔ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
10397, 99, 1023anbi123d 1464 . . . . . . . . 9 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
104103adantl 487 . . . . . . . 8 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
10525, 16syl 18 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
106105mptexd 7227 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V)
10774a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 0 ∈ V)
108 funmpt 6575 . . . . . . . . . . 11 Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
109108a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
110 simplr 781 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑓: 𝑆𝑆)
111110ffund 6711 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun 𝑓)
112 simp-4r 796 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏 finSupp 0 )
113112fsuppimpd 9343 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑏 supp 0 ) ∈ Fin)
114 imafi 9289 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
115111, 113, 114syl2anc 596 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
116 nfv 1947 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
11765, 116nfan 1932 . . . . . . . . . . . . . . 15 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
118 simpllr 788 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓: 𝑆𝑆)
119118ffund 6711 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
120 snssi 4749 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
121120adantl 487 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
122 sspreima 7064 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
123119, 121, 122syl2anc 596 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
124 difpreima 7061 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝑓 → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
125119, 124syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
126123, 125sseqtrd 3970 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
127 suppssdm 8179 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 supp 0 ) ⊆ dom 𝑏
12835ad6antlr 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏: 𝑆𝐵)
129127, 128fssdm 6726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ 𝑆)
130118fdmd 6717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = 𝑆)
131129, 130sseqtrrd 3971 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
132 sseqin2 4172 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
133132biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
134 dminss 6148 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))
135133, 134eqsstrrdi 3979 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
136131, 135syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
137136sscond 4096 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
138126, 137sstrd 3944 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
139 fimacnv 6729 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓: 𝑆𝑆 → (𝑓𝑆) = 𝑆)
140118, 139syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓𝑆) = 𝑆)
141140difeq1d 4076 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑏 supp 0 )) = ( 𝑆 ∖ (𝑏 supp 0 )))
142138, 141sseqtrd 3970 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
143142sselda 3934 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
144 ssidd 3957 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑏 supp 0 ))
14572adantr 486 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑆 ∈ V)
14674a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 0 ∈ V)
147128, 144, 145, 146suppssr 8197 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
148143, 147syldan 603 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → (𝑏𝑗) = 0 )
149148oveq1d 7432 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1505ad7antr 751 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
15113ad7antr 751 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
15239ad3antlr 744 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ 𝑆)
153152sselda 3934 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 𝑆)
154151, 153sseldd 3935 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗𝐵)
155150, 154, 84syl2anc 596 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ( 0 · 𝑗) = 0 )
156149, 155eqtrd 2797 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = 0 )
157117, 156mpteq2da 5201 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 ))
158157oveq2d 7433 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )))
1595, 27syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ CMnd)
160159cmnmndd 19937 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ Mnd)
161160ad6antr 749 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
1623gsumz 18951 . . . . . . . . . . . . . 14 ((𝑅 ∈ Mnd ∧ (𝑓 “ {𝑖}) ∈ V) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
163161, 32, 162sylancl 598 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
164158, 163eqtrd 2797 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = 0 )
165164, 105suppss2 8202 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
166115, 165ssfid 9243 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
167 isfsupp 9339 . . . . . . . . . . 11 (((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ↔ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)))
168167biimpar 483 . . . . . . . . . 10 ((((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) ∧ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
169106, 107, 109, 166, 168syl22anc 852 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
170 simpllr 788 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
17125, 159syl 18 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑅 ∈ CMnd)
1725ad6antr 749 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
17335ad5antlr 748 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏: 𝑆𝐵)
174173ffvelcdmda 7081 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → (𝑏𝑗) ∈ 𝐵)
17525, 13syl 18 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆𝐵)
176175sselda 3934 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑗𝐵)
1772, 4ringcl 20395 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑗) ∈ 𝐵𝑗𝐵) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
178172, 174, 176, 177syl3anc 1398 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
179 eqid 2762 . . . . . . . . . . . 12 (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
18065, 178, 179fmptdf 7114 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)): 𝑆𝐵)
18172mptexd 7227 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
182 funmpt 6575 . . . . . . . . . . . . 13 Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
183182a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
184 nfcv 2924 . . . . . . . . . . . . 13 𝑗 𝑆
185173adantr 486 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
186185ffnd 6707 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
18772adantr 486 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
18874a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 0 ∈ V)
189 simpr 490 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
190186, 187, 188, 189fvdifsupp 8173 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
191190oveq1d 7432 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1925ad6antr 749 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
193175adantr 486 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
194189eldifad 3914 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
195193, 194sseldd 3935 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
196192, 195, 84syl2anc 596 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
197191, 196eqtrd 2797 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
19865, 184, 69, 197, 72suppss2f 33119 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
199 fsuppsssupp 9355 . . . . . . . . . . . 12 ((((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
200181, 183, 112, 198, 199syl22anc 852 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
201 sndisj 5099 . . . . . . . . . . . 12 Disj 𝑖𝑆 {𝑖}
202 disjpreima 33065 . . . . . . . . . . . 12 ((Fun 𝑓Disj 𝑖𝑆 {𝑖}) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
203111, 201, 202sylancl 598 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
204 iunid 5023 . . . . . . . . . . . . 13 𝑖𝑆 {𝑖} = 𝑆
205204imaeq2i 6058 . . . . . . . . . . . 12 (𝑓 𝑖𝑆 {𝑖}) = (𝑓𝑆)
206 iunpreima 7065 . . . . . . . . . . . . 13 (Fun 𝑓 → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
207111, 206syl 18 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
208139ad2antlr 740 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓𝑆) = 𝑆)
209205, 207, 2083eqtr3a 2821 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑖𝑆 (𝑓 “ {𝑖}) = 𝑆)
2102, 3, 171, 72, 105, 180, 200, 203, 209gsumpart 33511 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))))
21140resmptd 6040 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
212211oveq2d 7433 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
213212mpteq2dva 5202 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
214213oveq2d 7433 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
215170, 210, 2143eqtrd 2801 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
216 eqid 2762 . . . . . . . . . . . 12 (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
217 simpr 490 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
218217sneqd 4599 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
219218imaeq2d 6060 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑓 “ {𝑖}) = (𝑓 “ {𝑘}))
220219mpteq1d 5199 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
221220oveq2d 7433 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
222 simpr 490 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘𝑆)
223 ovexd 7452 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ V)
224216, 221, 222, 223fvmptd2 6999 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
225159ad6antr 749 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ CMnd)
22629cnvex 7926 . . . . . . . . . . . . . 14 𝑓 ∈ V
227226imaex 7915 . . . . . . . . . . . . 13 (𝑓 “ {𝑘}) ∈ V
228227a1i 11 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ∈ V)
2295ad6antr 749 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ Ring)
23025, 6syl 18 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ⊆ (LIdeal‘𝑅))
231230sselda 3934 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
2328lidlsubg 21417 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
233 subgsubm 19278 . . . . . . . . . . . . . 14 (𝑘 ∈ (SubGrp‘𝑅) → 𝑘 ∈ (SubMnd‘𝑅))
234232, 233syl 18 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubMnd‘𝑅))
235229, 231, 234syl2anc 596 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (SubMnd‘𝑅))
236229adantr 486 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑅 ∈ Ring)
237231adantr 486 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑘 ∈ (LIdeal‘𝑅))
23835ad7antlr 752 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑏: 𝑆𝐵)
239 cnvimass 6082 . . . . . . . . . . . . . . . . . 18 (𝑓 “ {𝑘}) ⊆ dom 𝑓
240239, 38sseqtrid 3976 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑘}) ⊆ 𝑆)
241240ad3antlr 744 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ⊆ 𝑆)
242241sselda 3934 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 𝑆)
243238, 242ffvelcdmd 7082 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑏𝑙) ∈ 𝐵)
244 fveq2 6882 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑙 → (𝑓𝑗) = (𝑓𝑙))
24548, 244eleq12d 2856 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑙 → (𝑗 ∈ (𝑓𝑗) ↔ 𝑙 ∈ (𝑓𝑙)))
246 simpllr 788 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
247245, 246, 242rspcdva 3580 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓𝑙))
248 simp-4r 796 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓: 𝑆𝑆)
249248ffnd 6707 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓 Fn 𝑆)
250 elpreima 7054 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑆 → (𝑙 ∈ (𝑓 “ {𝑘}) ↔ (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘})))
251250biimpa 482 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘}))
252 elsni 4604 . . . . . . . . . . . . . . . . 17 ((𝑓𝑙) ∈ {𝑘} → (𝑓𝑙) = 𝑘)
253251, 252simpl2im 513 . . . . . . . . . . . . . . . 16 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
254249, 253sylancom 600 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
255247, 254eleqtrd 2864 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙𝑘)
2568, 2, 4lidlmcl 21419 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ((𝑏𝑙) ∈ 𝐵𝑙𝑘)) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
257236, 237, 243, 255, 256syl22anc 852 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
25849cbvmptv 5213 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑙) · 𝑙))
259257, 258fmptd 7111 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑘})⟶𝑘)
260228mptexd 7227 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
261259ffund 6711 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
262 simp-5r 798 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑏 finSupp 0 )
263 nfv 1947 . . . . . . . . . . . . . . 15 𝑗 𝑘𝑆
26465, 263nfan 1932 . . . . . . . . . . . . . 14 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆)
265 nfcv 2924 . . . . . . . . . . . . . 14 𝑗(𝑓 “ {𝑘})
26635ad7antlr 752 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
267266ffnd 6707 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
26872ad2antrr 739 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
26974a1i 11 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
270241ssdifd 4095 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
271270sselda 3934 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
272267, 268, 269, 271fvdifsupp 8173 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
273272oveq1d 7432 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
27413ad7antr 751 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
275271eldifad 3914 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
276274, 275sseldd 3935 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
277229, 276, 84syl2an2r 698 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
278273, 277eqtrd 2797 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
279264, 265, 69, 278, 228suppss2f 33119 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
280 fsuppsssupp 9355 . . . . . . . . . . . . 13 ((((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
281260, 261, 262, 279, 280syl22anc 852 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
2823, 225, 228, 235, 259, 281gsumsubmcl 20052 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝑘)
283224, 282eqeltrd 2862 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
284283ralrimiva 3156 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
285169, 215, 2843jca 1146 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
28696, 104, 285rspcedvd 3581 . . . . . . 7 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
287286anasss 472 . . . . . 6 (((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ (𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
28824, 287exlimddv 1968 . . . . 5 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
289288anasss 472 . . . 4 (((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ (𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
290289r19.29an 3168 . . 3 ((𝜑 ∧ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
2915ad4antr 745 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ Ring)
292291adantr 486 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
293 eqid 2762 . . . . . . . . . . . . . 14 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
294293zrhrhm 21730 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
295 zringbas 21672 . . . . . . . . . . . . . 14 ℤ = (Base‘ℤring)
296295, 2rhmf 20632 . . . . . . . . . . . . 13 ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
297292, 294, 2963syl 19 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (ℤRHom‘𝑅):ℤ⟶𝐵)
298 simp-5r 798 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
29974a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
300 ssv 3958 . . . . . . . . . . . . . . . . . 18 ran 𝑎 ⊆ V
301 ssdif 4094 . . . . . . . . . . . . . . . . . 18 (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
302300, 301ax-mp 5 . . . . . . . . . . . . . . . . 17 (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
303302sseli 3930 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) → 𝑚 ∈ (V ∖ { 0 }))
304303adantl 487 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑚 ∈ (V ∖ { 0 }))
305 simp-4r 796 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
306298, 299, 304, 305fsuppinisegfi 33167 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑚}) ∈ Fin)
307 hashcl 14424 . . . . . . . . . . . . . 14 ((𝑎 “ {𝑚}) ∈ Fin → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
308306, 307syl 18 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
309308nn0zd 12644 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℤ)
310297, 309ffvelcdmd 7082 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ 𝐵)
311 eqid 2762 . . . . . . . . . . 11 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))
312310, 311fmptd 7111 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
3132, 3ring0cl 20414 . . . . . . . . . . 11 (𝑅 ∈ Ring → 0𝐵)
314 fconst6g 6768 . . . . . . . . . . 11 ( 0𝐵 → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
315291, 313, 3143syl 19 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
316 disjdif 4429 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
317316a1i 11 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
318312, 315, 317fun2d 6743 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
319 simplll 787 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝜑𝑎 ∈ (𝐵m 𝑆)))
32093, 16elmapd 8843 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑎 ∈ (𝐵m 𝑆) ↔ 𝑎:𝑆𝐵))
321320biimpa 482 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → 𝑎:𝑆𝐵)
322319, 321syl 18 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎:𝑆𝐵)
323322ffnd 6707 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
324 elssuni 4902 . . . . . . . . . . . . . . . . 17 (𝑘𝑆𝑘 𝑆)
325324adantl 487 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → 𝑘 𝑆)
326325sseld 3933 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → ((𝑎𝑘) ∈ 𝑘 → (𝑎𝑘) ∈ 𝑆))
327326ralimdva 3176 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆))
328327imp 412 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆)
329 fnfvrnss 7118 . . . . . . . . . . . . 13 ((𝑎 Fn 𝑆 ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆) → ran 𝑎 𝑆)
330323, 328, 329syl2anc 596 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ran 𝑎 𝑆)
331330ssdifssd 4097 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝑆)
332 undif 4441 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ⊆ 𝑆 ↔ ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
333331, 332sylib 221 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
334333feq2d 6690 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
335318, 334mpbid 235 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵)
33692a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝐵 ∈ V)
33717ad4antr 745 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆 ∈ V)
338336, 337elmapd 8843 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆) ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
339335, 338mpbird 260 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆))
340 breq1 5110 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
341 fveq1 6881 . . . . . . . . . . . . 13 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
342341oveq1d 7432 . . . . . . . . . . . 12 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
343342mpteq2dv 5203 . . . . . . . . . . 11 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
344343oveq2d 7433 . . . . . . . . . 10 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
345344eqeq2d 2773 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ↔ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
346340, 345anbi12d 644 . . . . . . . 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 487 . . . . . . 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 6711 . . . . . . . . 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 6711 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun 𝑎)
352319simprd 501 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 ∈ (𝐵m 𝑆))
353 simpllr 788 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 finSupp 0 )
354 fsupprnfi 33172 . . . . . . . . . . . . 13 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
355 diffi 9173 . . . . . . . . . . . . 13 (ran 𝑎 ∈ Fin → (ran 𝑎 ∖ { 0 }) ∈ Fin)
356354, 355syl 18 . . . . . . . . . . . 12 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
357351, 352, 350, 353, 356syl22anc 852 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
358312, 357, 350fdmfifsupp 9349 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) finSupp 0 )
35913ssdifssd 4097 . . . . . . . . . . . . 13 (𝜑 → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
360359ad4antr 745 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
361336, 360ssexd 5293 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
362361, 350fczfsuppd 9360 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
363358, 362fsuppun 9361 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
364 funisfsupp 9341 . . . . . . . . . 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 483 . . . . . . . . 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 1400 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
367 fvex 6895 . . . . . . . . . . . . . . . 16 ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ V
368367, 311fnmpti 6679 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 })
369368a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }))
370 fnconstg 6767 . . . . . . . . . . . . . . . 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 490 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (ran 𝑎 ∖ { 0 }))
375369, 372, 373, 374fvun1d 6975 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗))
376 sneq 4597 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → {𝑚} = {𝑗})
377376imaeq2d 6060 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → (𝑎 “ {𝑚}) = (𝑎 “ {𝑗}))
378377fveq2d 6886 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (♯‘(𝑎 “ {𝑚})) = (♯‘(𝑎 “ {𝑗})))
379378fveq2d 6886 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
380 fvexd 6897 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) ∈ V)
381311, 379, 374, 380fvmptd3 7014 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
382375, 381eqtrd 2797 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
383382oveq1d 7432 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))
384383mpteq2dva 5202 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)))
385384oveq2d 7433 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
386291, 27syl 18 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ CMnd)
387316a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
388 fvun2 6974 . . . . . . . . . . . . . . 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 1480 . . . . . . . . . . . . . 14 ((((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅ ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
390387, 389sylancom 600 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
39174fvconst2 7207 . . . . . . . . . . . . . 14 (𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
392391adantl 487 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
393390, 392eqtrd 2797 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
394393oveq1d 7432 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
395360sselda 3934 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → 𝑗𝐵)
396291, 395, 84syl2an2r 698 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ( 0 · 𝑗) = 0 )
397394, 396eqtrd 2797 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = 0 )
398291adantr 486 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
399335ffvelcdmda 7081 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
40013ad4antr 745 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆𝐵)
401400sselda 3934 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑗𝐵)
4022, 4ringcl 20395 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵𝑗𝐵) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
403398, 399, 401, 402syl3anc 1398 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
4042, 3, 386, 337, 397, 357, 403, 331gsummptres2 33501 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
405 eqid 2762 . . . . . . . . . . 11 (.g𝑅) = (.g𝑅)
4062, 3, 405, 386, 322, 353gsumhashmul 33515 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
407 simplr 781 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg 𝑎))
408291adantr 486 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
409352adantr 486 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
41074a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
411302, 374sselid 3932 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (V ∖ { 0 }))
412353adantr 486 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
413409, 410, 411, 412fsuppinisegfi 33167 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑗}) ∈ Fin)
414 hashcl 14424 . . . . . . . . . . . . . . 15 ((𝑎 “ {𝑗}) ∈ Fin → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
415413, 414syl 18 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
416415nn0zd 12644 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
417331, 400sstrd 3944 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
418417sselda 3934 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗𝐵)
419 eqid 2762 . . . . . . . . . . . . . . . . 17 (1r𝑅) = (1r𝑅)
420293, 405, 419zrhmulg 21728 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
421420adantr 486 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
422421oveq1d 7432 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗))
423 simpll 779 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑅 ∈ Ring)
424 simplr 781 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
4252, 419ringidcl 20412 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
426425ad2antrr 739 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (1r𝑅) ∈ 𝐵)
427 simpr 490 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑗𝐵)
4282, 405, 4mulgass2 20457 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((♯‘(𝑎 “ {𝑗})) ∈ ℤ ∧ (1r𝑅) ∈ 𝐵𝑗𝐵)) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
429423, 424, 426, 427, 428syl13anc 1399 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
4302, 4, 419ringlidm 20416 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
431423, 430sylancom 600 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
432431oveq2d 7433 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
433422, 429, 4323eqtrd 2801 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
434408, 416, 418, 433syl21anc 851 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
435434mpteq2dva 5202 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗)))
436435oveq2d 7433 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
437406, 407, 4363eqtr4d 2807 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
438385, 404, 4373eqtr4rd 2808 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
439366, 438jca 521 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
440339, 347, 439rspcedvd 3581 . . . . . 6 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
441440exp41 440 . . . . 5 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → (𝑎 finSupp 0 → (𝑋 = (𝑅 Σg 𝑎) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))))
4424413imp2 1368 . . . 4 (((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ (𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
443442r19.29an 3168 . . 3 ((𝜑 ∧ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
444290, 443impbida 813 . 2 (𝜑 → (∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
44514, 444bitrd 282 1 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209  wa 401  w3a 1103   = wceq 1570  wex 1812  wcel 2145  wral 3078  wrex 3088  Vcvv 3453  cdif 3899  cun 3900  cin 3901  wss 3902  c0 4282  {csn 4587   cuni 4870   ciun 4954  Disj wdisj 5074   class class class wbr 5107  cmpt 5190   × cxp 5657  ccnv 5658  dom cdm 5659  ran crn 5660  cres 5661  cima 5662  Fun wfun 6531   Fn wfn 6532  wf 6533  cfv 6537  (class class class)co 7417   supp csupp 8162  m cmap 8830  Fincfn 8956   finSupp cfsupp 9335  0cn0 12532  cz 12619  chash 14398  Basecbs 17307  .rcmulr 17349  0gc0g 17530   Σg cgsu 17531  Mndcmnd 18842  SubMndcsubmnd 18896  .gcmg 19196  SubGrpcsubg 19249  CMndccmn 19913  1rcur 20326  Ringcrg 20378   RingHom crh 20616  LIdealclidl 21399  RSpancrsp 21400  ringczring 21665  ℤRHomczrh 21718
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-reg 9568  ax-inf2 9624  ax-ac2 10469  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-addf 11207  ax-mulf 11208
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-disj 5075  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-of 7682  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8163  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-ixp 8909  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-fsupp 9336  df-sup 9416  df-oi 9486  df-r1 9750  df-rank 9751  df-scott 9872  df-card 9948  df-ac 10123  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-nn 12262  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336  df-8 12337  df-9 12338  df-n0 12533  df-z 12620  df-dec 12741  df-uz 12892  df-fz 13566  df-fzo 13714  df-seq 14070  df-hash 14399  df-struct 17245  df-sets 17262  df-slot 17280  df-ndx 17292  df-base 17308  df-ress 17329  df-plusg 17361  df-mulr 17362  df-starv 17363  df-sca 17364  df-vsca 17365  df-ip 17366  df-tset 17367  df-ple 17368  df-ds 17370  df-unif 17371  df-hom 17372  df-cco 17373  df-0g 17532  df-gsum 17533  df-prds 17538  df-pws 17540  df-mre 17676  df-mrc 17677  df-acs 17679  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-mhm 18897  df-submnd 18898  df-grp 19066  df-minusg 19067  df-sbg 19068  df-mulg 19197  df-subg 19252  df-ghm 19347  df-cntz 19450  df-cmn 19915  df-abl 19916  df-mgp 20280  df-rng 20294  df-ur 20327  df-ring 20380  df-cring 20381  df-rhm 20619  df-nzr 20679  df-subrng 20714  df-subrg 20738  df-lmod 21052  df-lss 21122  df-lsp 21162  df-lmhm 21212  df-lbs 21265  df-sra 21363  df-rgmod 21364  df-lidl 21401  df-rsp 21402  df-cnfld 21592  df-zring 21666  df-zrh 21722  df-dsmm 21951  df-frlm 21966  df-uvc 22002
This theorem is used by:  zarcmplem  34399
  Copyright terms: Public domain W3C validator