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 31844
Description: Elementhood to 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 3931 . . . . . 6 ((𝜑𝑖𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8 eqid 2736 . . . . . . 7 (LIdeal‘𝑅) = (LIdeal‘𝑅)
92, 8lidlss 20579 . . . . . 6 (𝑖 ∈ (LIdeal‘𝑅) → 𝑖𝐵)
107, 9syl 17 . . . . 5 ((𝜑𝑖𝑆) → 𝑖𝐵)
1110ralrimiva 3139 . . . 4 (𝜑 → ∀𝑖𝑆 𝑖𝐵)
12 unissb 4886 . . . 4 ( 𝑆𝐵 ↔ ∀𝑖𝑆 𝑖𝐵)
1311, 12sylibr 233 . . 3 (𝜑 𝑆𝐵)
141, 2, 3, 4, 5, 13elrsp 31807 . 2 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))
15 fvexd 6834 . . . . . . . . . 10 (𝜑 → (LIdeal‘𝑅) ∈ V)
1615, 6ssexd 5265 . . . . . . . . 9 (𝜑𝑆 ∈ V)
1716uniexd 7649 . . . . . . . 8 (𝜑 𝑆 ∈ V)
18 eluni2 4855 . . . . . . . . . . 11 (𝑗 𝑆 ↔ ∃𝑖𝑆 𝑗𝑖)
1918biimpi 215 . . . . . . . . . 10 (𝑗 𝑆 → ∃𝑖𝑆 𝑗𝑖)
2019adantl 482 . . . . . . . . 9 ((𝜑𝑗 𝑆) → ∃𝑖𝑆 𝑗𝑖)
2120ralrimiva 3139 . . . . . . . 8 (𝜑 → ∀𝑗 𝑆𝑖𝑆 𝑗𝑖)
22 eleq2 2825 . . . . . . . . 9 (𝑖 = (𝑓𝑗) → (𝑗𝑖𝑗 ∈ (𝑓𝑗)))
2322ac6sg 10337 . . . . . . . 8 ( 𝑆 ∈ V → (∀𝑗 𝑆𝑖𝑆 𝑗𝑖 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))))
2417, 21, 23sylc 65 . . . . . . 7 (𝜑 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
2524ad3antrrr 727 . . . . . 6 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
26 simp-5l 782 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝜑)
2726adantr 481 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝜑)
28 ringcmn 19907 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
2927, 5, 283syl 18 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑅 ∈ CMnd)
30 vex 3445 . . . . . . . . . . . . 13 𝑓 ∈ V
31 cnvexg 7831 . . . . . . . . . . . . 13 (𝑓 ∈ V → 𝑓 ∈ V)
32 imaexg 7822 . . . . . . . . . . . . 13 (𝑓 ∈ V → (𝑓 “ {𝑖}) ∈ V)
3330, 31, 32mp2b 10 . . . . . . . . . . . 12 (𝑓 “ {𝑖}) ∈ V
3433a1i 11 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ∈ V)
355ad7antr 735 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
36 elmapi 8700 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵m 𝑆) → 𝑏: 𝑆𝐵)
3736ad7antlr 736 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑏: 𝑆𝐵)
38 cnvimass 6013 . . . . . . . . . . . . . . . . 17 (𝑓 “ {𝑖}) ⊆ dom 𝑓
39 fdm 6654 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → dom 𝑓 = 𝑆)
4038, 39sseqtrid 3983 . . . . . . . . . . . . . . . 16 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑖}) ⊆ 𝑆)
4140ad3antlr 728 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ⊆ 𝑆)
4241sselda 3931 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙 𝑆)
4337, 42ffvelcdmd 7012 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → (𝑏𝑙) ∈ 𝐵)
4413ad7antr 735 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
4544, 42sseldd 3932 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙𝐵)
462, 4ringcl 19887 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑙) ∈ 𝐵𝑙𝐵) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
4735, 43, 45, 46syl3anc 1370 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
48 fveq2 6819 . . . . . . . . . . . . . 14 (𝑗 = 𝑙 → (𝑏𝑗) = (𝑏𝑙))
49 id 22 . . . . . . . . . . . . . 14 (𝑗 = 𝑙𝑗 = 𝑙)
5048, 49oveq12d 7347 . . . . . . . . . . . . 13 (𝑗 = 𝑙 → ((𝑏𝑗) · 𝑗) = ((𝑏𝑙) · 𝑙))
5150cbvmptv 5202 . . . . . . . . . . . 12 (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑙) · 𝑙))
5247, 51fmptd 7038 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑖})⟶𝐵)
5334mptexd 7150 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
5452ffund 6649 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
55 simp-5r 783 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑏 finSupp 0 )
56 nfv 1916 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 )
57 nfcv 2904 . . . . . . . . . . . . . . . . . . 19 𝑗𝑅
58 nfcv 2904 . . . . . . . . . . . . . . . . . . 19 𝑗 Σg
59 nfmpt1 5197 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
6057, 58, 59nfov 7359 . . . . . . . . . . . . . . . . . 18 𝑗(𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6160nfeq2 2921 . . . . . . . . . . . . . . . . 17 𝑗 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6256, 61nfan 1901 . . . . . . . . . . . . . . . 16 𝑗(((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
63 nfv 1916 . . . . . . . . . . . . . . . 16 𝑗 𝑓: 𝑆𝑆
6462, 63nfan 1901 . . . . . . . . . . . . . . 15 𝑗((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆)
65 nfra1 3263 . . . . . . . . . . . . . . 15 𝑗𝑗 𝑆𝑗 ∈ (𝑓𝑗)
6664, 65nfan 1901 . . . . . . . . . . . . . 14 𝑗(((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
67 nfv 1916 . . . . . . . . . . . . . 14 𝑗 𝑖𝑆
6866, 67nfan 1901 . . . . . . . . . . . . 13 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆)
69 nfcv 2904 . . . . . . . . . . . . 13 𝑗(𝑓 “ {𝑖})
70 nfcv 2904 . . . . . . . . . . . . 13 𝑗(𝑏 supp 0 )
7136ad7antlr 736 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
7271ffnd 6646 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
7326, 17syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
7473ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
753fvexi 6833 . . . . . . . . . . . . . . . . 17 0 ∈ V
7675a1i 11 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
7741ssdifd 4086 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
7877sselda 3931 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
7972, 74, 76, 78fvdifsupp 31246 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
8079oveq1d 7344 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
815ad7antr 735 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
8213ad7antr 735 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
8378eldifad 3909 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
8482, 83sseldd 3932 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
852, 4, 3ringlz 19913 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ( 0 · 𝑗) = 0 )
8681, 84, 85syl2anc 584 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
8780, 86eqtrd 2776 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
8868, 69, 70, 87, 34suppss2f 31202 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
89 fsuppsssupp 9234 . . . . . . . . . . . 12 ((((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
9053, 54, 55, 88, 89syl22anc 836 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
912, 3, 29, 34, 52, 90gsumcl 19603 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝐵)
9291fmpttd 7039 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵)
932fvexi 6833 . . . . . . . . . . . 12 𝐵 ∈ V
9493a1i 11 . . . . . . . . . . 11 (𝜑𝐵 ∈ V)
9594, 16elmapd 8692 . . . . . . . . . 10 (𝜑 → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆) ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵))
9695biimpar 478 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
9726, 92, 96syl2anc 584 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
98 breq1 5092 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ))
99 oveq2 7337 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
10099eqeq2d 2747 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σg 𝑎) ↔ 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))))
101 fveq1 6818 . . . . . . . . . . . 12 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎𝑘) = ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘))
102101eleq1d 2821 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎𝑘) ∈ 𝑘 ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
103102ralbidv 3170 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 ↔ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
10498, 100, 1033anbi123d 1435 . . . . . . . . 9 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
105104adantl 482 . . . . . . . 8 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
10626, 16syl 17 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
107106mptexd 7150 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V)
10875a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 0 ∈ V)
109 funmpt 6516 . . . . . . . . . . 11 Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
110109a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
111 simplr 766 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑓: 𝑆𝑆)
112111ffund 6649 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun 𝑓)
113 simp-4r 781 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏 finSupp 0 )
114113fsuppimpd 9225 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑏 supp 0 ) ∈ Fin)
115 imafi 9032 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
116112, 114, 115syl2anc 584 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
117 nfv 1916 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
11866, 117nfan 1901 . . . . . . . . . . . . . . 15 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
119 simpllr 773 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓: 𝑆𝑆)
120119ffund 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
121 snssi 4754 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
122121adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
123 sspreima 6995 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
124120, 122, 123syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
125 difpreima 6992 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝑓 → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
126120, 125syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
127124, 126sseqtrd 3971 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
128 suppssdm 8055 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 supp 0 ) ⊆ dom 𝑏
12936ad6antlr 734 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏: 𝑆𝐵)
130128, 129fssdm 6665 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ 𝑆)
131119fdmd 6656 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = 𝑆)
132130, 131sseqtrrd 3972 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
133 sseqin2 4161 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
134133biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
135 dminss 6085 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))
136134, 135eqsstrrdi 3986 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
137132, 136syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
138137sscond 4087 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
139127, 138sstrd 3941 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
140 fimacnv 6667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓: 𝑆𝑆 → (𝑓𝑆) = 𝑆)
141119, 140syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓𝑆) = 𝑆)
142141difeq1d 4067 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑏 supp 0 )) = ( 𝑆 ∖ (𝑏 supp 0 )))
143139, 142sseqtrd 3971 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
144143sselda 3931 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
145 ssidd 3954 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑏 supp 0 ))
14673adantr 481 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑆 ∈ V)
14775a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 0 ∈ V)
148129, 145, 146, 147suppssr 8074 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
149144, 148syldan 591 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → (𝑏𝑗) = 0 )
150149oveq1d 7344 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1515ad7antr 735 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
15213ad7antr 735 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
15340ad3antlr 728 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ 𝑆)
154153sselda 3931 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 𝑆)
155152, 154sseldd 3932 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗𝐵)
156151, 155, 85syl2anc 584 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ( 0 · 𝑗) = 0 )
157150, 156eqtrd 2776 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = 0 )
158118, 157mpteq2da 5187 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 ))
159158oveq2d 7345 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )))
1605, 28syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ CMnd)
161160cmnmndd 19496 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ Mnd)
162161ad6antr 733 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
1633gsumz 18563 . . . . . . . . . . . . . 14 ((𝑅 ∈ Mnd ∧ (𝑓 “ {𝑖}) ∈ V) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
164162, 33, 163sylancl 586 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
165159, 164eqtrd 2776 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = 0 )
166165, 106suppss2 8078 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
167116, 166ssfid 9124 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
168 isfsupp 9222 . . . . . . . . . . 11 (((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ↔ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)))
169168biimpar 478 . . . . . . . . . 10 ((((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) ∧ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
170107, 108, 110, 167, 169syl22anc 836 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
171 simpllr 773 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
17226, 160syl 17 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑅 ∈ CMnd)
1735ad6antr 733 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
17436ad5antlr 732 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏: 𝑆𝐵)
175174ffvelcdmda 7011 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → (𝑏𝑗) ∈ 𝐵)
17626, 13syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆𝐵)
177176sselda 3931 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑗𝐵)
1782, 4ringcl 19887 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑗) ∈ 𝐵𝑗𝐵) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
179173, 175, 177, 178syl3anc 1370 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
180 eqid 2736 . . . . . . . . . . . 12 (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
18166, 179, 180fmptdf 7041 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)): 𝑆𝐵)
18273mptexd 7150 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
183 funmpt 6516 . . . . . . . . . . . . 13 Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
184183a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
185 nfcv 2904 . . . . . . . . . . . . 13 𝑗 𝑆
186174adantr 481 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
187186ffnd 6646 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
18873adantr 481 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
18975a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 0 ∈ V)
190 simpr 485 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
191187, 188, 189, 190fvdifsupp 31246 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
192191oveq1d 7344 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1935ad6antr 733 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
194176adantr 481 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
195190eldifad 3909 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
196194, 195sseldd 3932 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
197193, 196, 85syl2anc 584 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
198192, 197eqtrd 2776 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
19966, 185, 70, 198, 73suppss2f 31202 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
200 fsuppsssupp 9234 . . . . . . . . . . . 12 ((((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
201182, 184, 113, 199, 200syl22anc 836 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
202 sndisj 5080 . . . . . . . . . . . 12 Disj 𝑖𝑆 {𝑖}
203 disjpreima 31151 . . . . . . . . . . . 12 ((Fun 𝑓Disj 𝑖𝑆 {𝑖}) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
204112, 202, 203sylancl 586 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
205 iunid 5004 . . . . . . . . . . . . 13 𝑖𝑆 {𝑖} = 𝑆
206205imaeq2i 5991 . . . . . . . . . . . 12 (𝑓 𝑖𝑆 {𝑖}) = (𝑓𝑆)
207 iunpreima 31132 . . . . . . . . . . . . 13 (Fun 𝑓 → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
208112, 207syl 17 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
209140ad2antlr 724 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓𝑆) = 𝑆)
210206, 208, 2093eqtr3a 2800 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑖𝑆 (𝑓 “ {𝑖}) = 𝑆)
2112, 3, 172, 73, 106, 181, 201, 204, 210gsumpart 31543 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))))
21241resmptd 5974 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
213212oveq2d 7345 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
214213mpteq2dva 5189 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
215214oveq2d 7345 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
216171, 211, 2153eqtrd 2780 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
217 eqid 2736 . . . . . . . . . . . 12 (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
218 simpr 485 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
219218sneqd 4584 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
220219imaeq2d 5993 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑓 “ {𝑖}) = (𝑓 “ {𝑘}))
221220mpteq1d 5184 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
222221oveq2d 7345 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
223 simpr 485 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘𝑆)
224 ovexd 7364 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ V)
225217, 222, 223, 224fvmptd2 6933 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
226160ad6antr 733 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ CMnd)
22730cnvex 7832 . . . . . . . . . . . . . 14 𝑓 ∈ V
228227imaex 7823 . . . . . . . . . . . . 13 (𝑓 “ {𝑘}) ∈ V
229228a1i 11 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ∈ V)
2305ad6antr 733 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ Ring)
23126, 6syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ⊆ (LIdeal‘𝑅))
232231sselda 3931 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
2338lidlsubg 20584 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
234 subgsubm 18865 . . . . . . . . . . . . . 14 (𝑘 ∈ (SubGrp‘𝑅) → 𝑘 ∈ (SubMnd‘𝑅))
235233, 234syl 17 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubMnd‘𝑅))
236230, 232, 235syl2anc 584 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (SubMnd‘𝑅))
237230adantr 481 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑅 ∈ Ring)
238232adantr 481 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑘 ∈ (LIdeal‘𝑅))
23936ad7antlr 736 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑏: 𝑆𝐵)
240 cnvimass 6013 . . . . . . . . . . . . . . . . . 18 (𝑓 “ {𝑘}) ⊆ dom 𝑓
241240, 39sseqtrid 3983 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑘}) ⊆ 𝑆)
242241ad3antlr 728 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ⊆ 𝑆)
243242sselda 3931 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 𝑆)
244239, 243ffvelcdmd 7012 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑏𝑙) ∈ 𝐵)
245 fveq2 6819 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑙 → (𝑓𝑗) = (𝑓𝑙))
24649, 245eleq12d 2831 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑙 → (𝑗 ∈ (𝑓𝑗) ↔ 𝑙 ∈ (𝑓𝑙)))
247 simpllr 773 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
248246, 247, 243rspcdva 3571 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓𝑙))
249 simp-4r 781 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓: 𝑆𝑆)
250249ffnd 6646 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓 Fn 𝑆)
251 elpreima 6985 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑆 → (𝑙 ∈ (𝑓 “ {𝑘}) ↔ (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘})))
252251biimpa 477 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘}))
253 elsni 4589 . . . . . . . . . . . . . . . . 17 ((𝑓𝑙) ∈ {𝑘} → (𝑓𝑙) = 𝑘)
254252, 253simpl2im 504 . . . . . . . . . . . . . . . 16 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
255250, 254sylancom 588 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
256248, 255eleqtrd 2839 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙𝑘)
2578, 2, 4lidlmcl 20586 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ((𝑏𝑙) ∈ 𝐵𝑙𝑘)) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
258237, 238, 244, 256, 257syl22anc 836 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
25950cbvmptv 5202 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑙) · 𝑙))
260258, 259fmptd 7038 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑘})⟶𝑘)
261229mptexd 7150 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
262260ffund 6649 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
263 simp-5r 783 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑏 finSupp 0 )
264 nfv 1916 . . . . . . . . . . . . . . 15 𝑗 𝑘𝑆
26566, 264nfan 1901 . . . . . . . . . . . . . 14 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆)
266 nfcv 2904 . . . . . . . . . . . . . 14 𝑗(𝑓 “ {𝑘})
26736ad7antlr 736 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
268267ffnd 6646 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
26973ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
27075a1i 11 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
271242ssdifd 4086 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
272271sselda 3931 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
273268, 269, 270, 272fvdifsupp 31246 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
274273oveq1d 7344 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
27513ad7antr 735 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
276272eldifad 3909 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
277275, 276sseldd 3932 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
278230, 277, 85syl2an2r 682 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
279274, 278eqtrd 2776 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
280265, 266, 70, 279, 229suppss2f 31202 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
281 fsuppsssupp 9234 . . . . . . . . . . . . 13 ((((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
282261, 262, 263, 280, 281syl22anc 836 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
2833, 226, 229, 236, 260, 282gsumsubmcl 19607 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝑘)
284225, 283eqeltrd 2837 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
285284ralrimiva 3139 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
286170, 216, 2853jca 1127 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
28797, 105, 286rspcedvd 3572 . . . . . . 7 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
288287anasss 467 . . . . . 6 (((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ (𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
28925, 288exlimddv 1937 . . . . 5 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
290289anasss 467 . . . 4 (((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ (𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
291290r19.29an 3151 . . 3 ((𝜑 ∧ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
2925ad4antr 729 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ Ring)
293292adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
294 eqid 2736 . . . . . . . . . . . . . 14 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
295294zrhrhm 20811 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
296 zringbas 20774 . . . . . . . . . . . . . 14 ℤ = (Base‘ℤring)
297296, 2rhmf 20058 . . . . . . . . . . . . 13 ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
298293, 295, 2973syl 18 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (ℤRHom‘𝑅):ℤ⟶𝐵)
299 simp-5r 783 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
30075a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
301 ssv 3955 . . . . . . . . . . . . . . . . . 18 ran 𝑎 ⊆ V
302 ssdif 4085 . . . . . . . . . . . . . . . . . 18 (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
303301, 302ax-mp 5 . . . . . . . . . . . . . . . . 17 (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
304303sseli 3927 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) → 𝑚 ∈ (V ∖ { 0 }))
305304adantl 482 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑚 ∈ (V ∖ { 0 }))
306 simp-4r 781 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
307299, 300, 305, 306fsuppinisegfi 31249 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑚}) ∈ Fin)
308 hashcl 14163 . . . . . . . . . . . . . 14 ((𝑎 “ {𝑚}) ∈ Fin → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
309307, 308syl 17 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
310309nn0zd 12517 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℤ)
311298, 310ffvelcdmd 7012 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ 𝐵)
312 eqid 2736 . . . . . . . . . . 11 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))
313311, 312fmptd 7038 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
3142, 3ring0cl 19895 . . . . . . . . . . 11 (𝑅 ∈ Ring → 0𝐵)
315 fconst6g 6708 . . . . . . . . . . 11 ( 0𝐵 → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
316292, 314, 3153syl 18 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
317 disjdif 4417 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
318317a1i 11 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
319313, 316, 318fun2d 6683 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
320 simplll 772 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝜑𝑎 ∈ (𝐵m 𝑆)))
32194, 16elmapd 8692 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑎 ∈ (𝐵m 𝑆) ↔ 𝑎:𝑆𝐵))
322321biimpa 477 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → 𝑎:𝑆𝐵)
323320, 322syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎:𝑆𝐵)
324323ffnd 6646 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
325 elssuni 4884 . . . . . . . . . . . . . . . . 17 (𝑘𝑆𝑘 𝑆)
326325adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → 𝑘 𝑆)
327326sseld 3930 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → ((𝑎𝑘) ∈ 𝑘 → (𝑎𝑘) ∈ 𝑆))
328327ralimdva 3160 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆))
329328imp 407 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆)
330 fnfvrnss 7044 . . . . . . . . . . . . 13 ((𝑎 Fn 𝑆 ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆) → ran 𝑎 𝑆)
331324, 329, 330syl2anc 584 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ran 𝑎 𝑆)
332331ssdifssd 4088 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝑆)
333 undif 4427 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ⊆ 𝑆 ↔ ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
334332, 333sylib 217 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
335334feq2d 6631 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
336319, 335mpbid 231 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵)
33793a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝐵 ∈ V)
33817ad4antr 729 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆 ∈ V)
339337, 338elmapd 8692 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆) ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
340336, 339mpbird 256 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆))
341 breq1 5092 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
342 fveq1 6818 . . . . . . . . . . . . 13 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
343342oveq1d 7344 . . . . . . . . . . . 12 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
344343mpteq2dv 5191 . . . . . . . . . . 11 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
345344oveq2d 7345 . . . . . . . . . 10 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
346345eqeq2d 2747 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ↔ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
347341, 346anbi12d 631 . . . . . . . 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 }))‘𝑗) · 𝑗))))))
348347adantl 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 }))‘𝑗) · 𝑗))))))
349319ffund 6649 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })))
350340elexd 3461 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ V)
35175a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 0 ∈ V)
352323ffund 6649 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun 𝑎)
353320simprd 496 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 ∈ (𝐵m 𝑆))
354 simpllr 773 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 finSupp 0 )
355 fsupprnfi 31254 . . . . . . . . . . . . 13 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
356 diffi 9036 . . . . . . . . . . . . 13 (ran 𝑎 ∈ Fin → (ran 𝑎 ∖ { 0 }) ∈ Fin)
357355, 356syl 17 . . . . . . . . . . . 12 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
358352, 353, 351, 354, 357syl22anc 836 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
359313, 358, 351fdmfifsupp 9228 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) finSupp 0 )
36013ssdifssd 4088 . . . . . . . . . . . . 13 (𝜑 → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
361360ad4antr 729 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
362337, 361ssexd 5265 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
363362, 351fczfsuppd 9236 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
364359, 363fsuppun 9237 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
365 funisfsupp 9223 . . . . . . . . . 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))
366365biimpar 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 )
367349, 350, 351, 364, 366syl31anc 1372 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
368 fvex 6832 . . . . . . . . . . . . . . . 16 ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ V
369368, 312fnmpti 6621 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 })
370369a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }))
371 fnconstg 6707 . . . . . . . . . . . . . . . 16 ( 0 ∈ V → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))
37275, 371ax-mp 5 . . . . . . . . . . . . . . 15 (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))
373372a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) Fn ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))
374317a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
375 simpr 485 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (ran 𝑎 ∖ { 0 }))
376370, 373, 374, 375fvun1d 6911 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗))
377 sneq 4582 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → {𝑚} = {𝑗})
378377imaeq2d 5993 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → (𝑎 “ {𝑚}) = (𝑎 “ {𝑗}))
379378fveq2d 6823 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (♯‘(𝑎 “ {𝑚})) = (♯‘(𝑎 “ {𝑗})))
380379fveq2d 6823 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
381 fvexd 6834 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) ∈ V)
382312, 380, 375, 381fvmptd3 6948 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
383376, 382eqtrd 2776 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
384383oveq1d 7344 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))
385384mpteq2dva 5189 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)))
386385oveq2d 7345 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
387292, 28syl 17 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ CMnd)
388317a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
389 fvun2 6910 . . . . . . . . . . . . . . 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 })‘𝑗))
390369, 372, 389mp3an12 1450 . . . . . . . . . . . . . 14 ((((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅ ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
391388, 390sylancom 588 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗))
39275fvconst2 7129 . . . . . . . . . . . . . 14 (𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
393392adantl 482 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
394391, 393eqtrd 2776 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
395394oveq1d 7344 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
396361sselda 3931 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → 𝑗𝐵)
397292, 396, 85syl2an2r 682 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ( 0 · 𝑗) = 0 )
398395, 397eqtrd 2776 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = 0 )
399292adantr 481 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
400336ffvelcdmda 7011 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
40113ad4antr 729 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆𝐵)
402401sselda 3931 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑗𝐵)
4032, 4ringcl 19887 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵𝑗𝐵) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
404399, 400, 402, 403syl3anc 1370 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
4052, 3, 387, 338, 398, 358, 404, 332gsummptres2 31541 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
406 eqid 2736 . . . . . . . . . . 11 (.g𝑅) = (.g𝑅)
4072, 3, 406, 387, 323, 354gsumhashmul 31544 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
408 simplr 766 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg 𝑎))
409292adantr 481 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
410353adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
41175a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
412303, 375sselid 3929 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (V ∖ { 0 }))
413354adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
414410, 411, 412, 413fsuppinisegfi 31249 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑗}) ∈ Fin)
415 hashcl 14163 . . . . . . . . . . . . . . 15 ((𝑎 “ {𝑗}) ∈ Fin → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
416414, 415syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
417416nn0zd 12517 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
418332, 401sstrd 3941 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
419418sselda 3931 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗𝐵)
420 eqid 2736 . . . . . . . . . . . . . . . . 17 (1r𝑅) = (1r𝑅)
421294, 406, 420zrhmulg 20809 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
422421adantr 481 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
423422oveq1d 7344 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗))
424 simpll 764 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑅 ∈ Ring)
425 simplr 766 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
4262, 420ringidcl 19894 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
427426ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (1r𝑅) ∈ 𝐵)
428 simpr 485 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑗𝐵)
4292, 406, 4mulgass2 19927 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((♯‘(𝑎 “ {𝑗})) ∈ ℤ ∧ (1r𝑅) ∈ 𝐵𝑗𝐵)) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
430424, 425, 427, 428, 429syl13anc 1371 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
4312, 4, 420ringlidm 19897 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
432424, 431sylancom 588 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
433432oveq2d 7345 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
434423, 430, 4333eqtrd 2780 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
435409, 417, 419, 434syl21anc 835 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
436435mpteq2dva 5189 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗)))
437436oveq2d 7345 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
438407, 408, 4373eqtr4d 2786 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
439386, 405, 4383eqtr4rd 2787 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
440367, 439jca 512 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
441340, 348, 440rspcedvd 3572 . . . . . 6 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
442441exp41 435 . . . . 5 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → (𝑎 finSupp 0 → (𝑋 = (𝑅 Σg 𝑎) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))))
4434423imp2 1348 . . . 4 (((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ (𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
444443r19.29an 3151 . . 3 ((𝜑 ∧ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
445291, 444impbida 798 . 2 (𝜑 → (∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
44614, 445bitrd 278 1 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wral 3061  wrex 3070  Vcvv 3441  cdif 3894  cun 3895  cin 3896  wss 3897  c0 4268  {csn 4572   cuni 4851   ciun 4938  Disj wdisj 5054   class class class wbr 5089  cmpt 5172   × cxp 5612  ccnv 5613  dom cdm 5614  ran crn 5615  cres 5616  cima 5617  Fun wfun 6467   Fn wfn 6468  wf 6469  cfv 6473  (class class class)co 7329   supp csupp 8039  m cmap 8678  Fincfn 8796   finSupp cfsupp 9218  0cn0 12326  cz 12412  chash 14137  Basecbs 17001  .rcmulr 17052  0gc0g 17239   Σg cgsu 17240  Mndcmnd 18474  SubMndcsubmnd 18518  .gcmg 18788  SubGrpcsubg 18837  CMndccmn 19473  1rcur 19824  Ringcrg 19870   RingHom crh 20043  LIdealclidl 20530  RSpancrsp 20531  ringczring 20768  ℤRHomczrh 20799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-reg 9441  ax-inf2 9490  ax-ac2 10312  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-addf 11043  ax-mulf 11044
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-tp 4577  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-iin 4941  df-disj 5055  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-of 7587  df-om 7773  df-1st 7891  df-2nd 7892  df-supp 8040  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-er 8561  df-map 8680  df-ixp 8749  df-en 8797  df-dom 8798  df-sdom 8799  df-fin 8800  df-fsupp 9219  df-sup 9291  df-oi 9359  df-r1 9613  df-rank 9614  df-card 9788  df-ac 9965  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-nn 12067  df-2 12129  df-3 12130  df-4 12131  df-5 12132  df-6 12133  df-7 12134  df-8 12135  df-9 12136  df-n0 12327  df-z 12413  df-dec 12531  df-uz 12676  df-fz 13333  df-fzo 13476  df-seq 13815  df-hash 14138  df-struct 16937  df-sets 16954  df-slot 16972  df-ndx 16984  df-base 17002  df-ress 17031  df-plusg 17064  df-mulr 17065  df-starv 17066  df-sca 17067  df-vsca 17068  df-ip 17069  df-tset 17070  df-ple 17071  df-ds 17073  df-unif 17074  df-hom 17075  df-cco 17076  df-0g 17241  df-gsum 17242  df-prds 17247  df-pws 17249  df-mre 17384  df-mrc 17385  df-acs 17387  df-mgm 18415  df-sgrp 18464  df-mnd 18475  df-mhm 18519  df-submnd 18520  df-grp 18668  df-minusg 18669  df-sbg 18670  df-mulg 18789  df-subg 18840  df-ghm 18920  df-cntz 19011  df-cmn 19475  df-abl 19476  df-mgp 19808  df-ur 19825  df-ring 19872  df-cring 19873  df-rnghom 20046  df-subrg 20119  df-lmod 20223  df-lss 20292  df-lsp 20332  df-lmhm 20382  df-lbs 20435  df-sra 20532  df-rgmod 20533  df-lidl 20534  df-rsp 20535  df-nzr 20627  df-cnfld 20696  df-zring 20769  df-zrh 20803  df-dsmm 21037  df-frlm 21052  df-uvc 21088
This theorem is referenced by:  zarcmplem  32070
  Copyright terms: Public domain W3C validator