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 33399
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 3946 . . . . . 6 ((𝜑𝑖𝑆) → 𝑖 ∈ (LIdeal‘𝑅))
8 eqid 2729 . . . . . . 7 (LIdeal‘𝑅) = (LIdeal‘𝑅)
92, 8lidlss 21122 . . . . . 6 (𝑖 ∈ (LIdeal‘𝑅) → 𝑖𝐵)
107, 9syl 17 . . . . 5 ((𝜑𝑖𝑆) → 𝑖𝐵)
1110ralrimiva 3125 . . . 4 (𝜑 → ∀𝑖𝑆 𝑖𝐵)
12 unissb 4903 . . . 4 ( 𝑆𝐵 ↔ ∀𝑖𝑆 𝑖𝐵)
1311, 12sylibr 234 . . 3 (𝜑 𝑆𝐵)
141, 2, 3, 4, 5, 13elrsp 33343 . 2 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))
15 fvexd 6873 . . . . . . . . . 10 (𝜑 → (LIdeal‘𝑅) ∈ V)
1615, 6ssexd 5279 . . . . . . . . 9 (𝜑𝑆 ∈ V)
1716uniexd 7718 . . . . . . . 8 (𝜑 𝑆 ∈ V)
18 eluni2 4875 . . . . . . . . . . 11 (𝑗 𝑆 ↔ ∃𝑖𝑆 𝑗𝑖)
1918biimpi 216 . . . . . . . . . 10 (𝑗 𝑆 → ∃𝑖𝑆 𝑗𝑖)
2019adantl 481 . . . . . . . . 9 ((𝜑𝑗 𝑆) → ∃𝑖𝑆 𝑗𝑖)
2120ralrimiva 3125 . . . . . . . 8 (𝜑 → ∀𝑗 𝑆𝑖𝑆 𝑗𝑖)
22 eleq2 2817 . . . . . . . . 9 (𝑖 = (𝑓𝑗) → (𝑗𝑖𝑗 ∈ (𝑓𝑗)))
2322ac6sg 10441 . . . . . . . 8 ( 𝑆 ∈ V → (∀𝑗 𝑆𝑖𝑆 𝑗𝑖 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))))
2417, 21, 23sylc 65 . . . . . . 7 (𝜑 → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
2524ad3antrrr 730 . . . . . 6 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑓(𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)))
26 simp-5l 784 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝜑)
2726adantr 480 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝜑)
28 ringcmn 20191 . . . . . . . . . . . 12 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
2927, 5, 283syl 18 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑅 ∈ CMnd)
30 vex 3451 . . . . . . . . . . . . 13 𝑓 ∈ V
31 cnvexg 7900 . . . . . . . . . . . . 13 (𝑓 ∈ V → 𝑓 ∈ V)
32 imaexg 7889 . . . . . . . . . . . . 13 (𝑓 ∈ V → (𝑓 “ {𝑖}) ∈ V)
3330, 31, 32mp2b 10 . . . . . . . . . . . 12 (𝑓 “ {𝑖}) ∈ V
3433a1i 11 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ∈ V)
355ad7antr 738 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
36 elmapi 8822 . . . . . . . . . . . . . . 15 (𝑏 ∈ (𝐵m 𝑆) → 𝑏: 𝑆𝐵)
3736ad7antlr 739 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑏: 𝑆𝐵)
38 cnvimass 6053 . . . . . . . . . . . . . . . . 17 (𝑓 “ {𝑖}) ⊆ dom 𝑓
39 fdm 6697 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → dom 𝑓 = 𝑆)
4038, 39sseqtrid 3989 . . . . . . . . . . . . . . . 16 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑖}) ⊆ 𝑆)
4140ad3antlr 731 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑓 “ {𝑖}) ⊆ 𝑆)
4241sselda 3946 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙 𝑆)
4337, 42ffvelcdmd 7057 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → (𝑏𝑙) ∈ 𝐵)
4413ad7antr 738 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
4544, 42sseldd 3947 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → 𝑙𝐵)
462, 4ringcl 20159 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑙) ∈ 𝐵𝑙𝐵) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
4735, 43, 45, 46syl3anc 1373 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑙) · 𝑙) ∈ 𝐵)
48 fveq2 6858 . . . . . . . . . . . . . 14 (𝑗 = 𝑙 → (𝑏𝑗) = (𝑏𝑙))
49 id 22 . . . . . . . . . . . . . 14 (𝑗 = 𝑙𝑗 = 𝑙)
5048, 49oveq12d 7405 . . . . . . . . . . . . 13 (𝑗 = 𝑙 → ((𝑏𝑗) · 𝑗) = ((𝑏𝑙) · 𝑙))
5150cbvmptv 5211 . . . . . . . . . . . 12 (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑙) · 𝑙))
5247, 51fmptd 7086 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑖})⟶𝐵)
5334mptexd 7198 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
5452ffund 6692 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
55 simp-5r 785 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → 𝑏 finSupp 0 )
56 nfv 1914 . . . . . . . . . . . . . . . . 17 𝑗((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 )
57 nfcv 2891 . . . . . . . . . . . . . . . . . . 19 𝑗𝑅
58 nfcv 2891 . . . . . . . . . . . . . . . . . . 19 𝑗 Σg
59 nfmpt1 5206 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
6057, 58, 59nfov 7417 . . . . . . . . . . . . . . . . . 18 𝑗(𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6160nfeq2 2909 . . . . . . . . . . . . . . . . 17 𝑗 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
6256, 61nfan 1899 . . . . . . . . . . . . . . . 16 𝑗(((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
63 nfv 1914 . . . . . . . . . . . . . . . 16 𝑗 𝑓: 𝑆𝑆
6462, 63nfan 1899 . . . . . . . . . . . . . . 15 𝑗((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆)
65 nfra1 3261 . . . . . . . . . . . . . . 15 𝑗𝑗 𝑆𝑗 ∈ (𝑓𝑗)
6664, 65nfan 1899 . . . . . . . . . . . . . 14 𝑗(((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
67 nfv 1914 . . . . . . . . . . . . . 14 𝑗 𝑖𝑆
6866, 67nfan 1899 . . . . . . . . . . . . 13 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆)
69 nfcv 2891 . . . . . . . . . . . . 13 𝑗(𝑓 “ {𝑖})
70 nfcv 2891 . . . . . . . . . . . . 13 𝑗(𝑏 supp 0 )
7136ad7antlr 739 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
7271ffnd 6689 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
7326, 17syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ∈ V)
7473ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
753fvexi 6872 . . . . . . . . . . . . . . . . 17 0 ∈ V
7675a1i 11 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
7741ssdifd 4108 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
7877sselda 3946 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
7972, 74, 76, 78fvdifsupp 8150 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
8079oveq1d 7402 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
815ad7antr 738 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
8213ad7antr 738 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
8378eldifad 3926 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
8482, 83sseldd 3947 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
852, 4, 3ringlz 20202 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ( 0 · 𝑗) = 0 )
8681, 84, 85syl2anc 584 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
8780, 86eqtrd 2764 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑖}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
8868, 69, 70, 87, 34suppss2f 32562 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
89 fsuppsssupp 9332 . . . . . . . . . . . 12 ((((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
9053, 54, 55, 88, 89syl22anc 838 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
912, 3, 29, 34, 52, 90gsumcl 19845 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝐵)
9291fmpttd 7087 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵)
932fvexi 6872 . . . . . . . . . . . 12 𝐵 ∈ V
9493a1i 11 . . . . . . . . . . 11 (𝜑𝐵 ∈ V)
9594, 16elmapd 8813 . . . . . . . . . 10 (𝜑 → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆) ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵))
9695biimpar 477 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))):𝑆𝐵) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
9726, 92, 96syl2anc 584 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ (𝐵m 𝑆))
98 breq1 5110 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎 finSupp 0 ↔ (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ))
99 oveq2 7395 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
10099eqeq2d 2740 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑋 = (𝑅 Σg 𝑎) ↔ 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))))
101 fveq1 6857 . . . . . . . . . . . 12 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (𝑎𝑘) = ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘))
102101eleq1d 2813 . . . . . . . . . . 11 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎𝑘) ∈ 𝑘 ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
103102ralbidv 3156 . . . . . . . . . 10 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 ↔ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
10498, 100, 1033anbi123d 1438 . . . . . . . . 9 (𝑎 = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) → ((𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ↔ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)))
105104adantl 481 . . . . . . . 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 7198 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V)
10875a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 0 ∈ V)
109 funmpt 6554 . . . . . . . . . . 11 Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
110109a1i 11 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
111 simplr 768 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑓: 𝑆𝑆)
112111ffund 6692 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun 𝑓)
113 simp-4r 783 . . . . . . . . . . . . 13 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏 finSupp 0 )
114113fsuppimpd 9320 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑏 supp 0 ) ∈ Fin)
115 imafi 9264 . . . . . . . . . . . 12 ((Fun 𝑓 ∧ (𝑏 supp 0 ) ∈ Fin) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
116112, 114, 115syl2anc 584 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 “ (𝑏 supp 0 )) ∈ Fin)
117 nfv 1914 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))
11866, 117nfan 1899 . . . . . . . . . . . . . . 15 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
119 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑓: 𝑆𝑆)
120119ffund 6692 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → Fun 𝑓)
121 snssi 4772 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
122121adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 ))))
123 sspreima 7040 . . . . . . . . . . . . . . . . . . . . . . 23 ((Fun 𝑓 ∧ {𝑖} ⊆ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
124120, 122, 123syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))))
125 difpreima 7037 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝑓 → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
126120, 125syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) = ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
127124, 126sseqtrd 3983 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))))
128 suppssdm 8156 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 supp 0 ) ⊆ dom 𝑏
12936ad6antlr 737 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑏: 𝑆𝐵)
130128, 129fssdm 6707 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ 𝑆)
131119fdmd 6698 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → dom 𝑓 = 𝑆)
132130, 131sseqtrrd 3984 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ dom 𝑓)
133 sseqin2 4186 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 supp 0 ) ⊆ dom 𝑓 ↔ (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
134133biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (dom 𝑓 ∩ (𝑏 supp 0 )) = (𝑏 supp 0 ))
135 dminss 6126 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom 𝑓 ∩ (𝑏 supp 0 )) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))
136134, 135eqsstrrdi 3992 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 supp 0 ) ⊆ dom 𝑓 → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
137132, 136syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑓 “ (𝑓 “ (𝑏 supp 0 ))))
138137sscond 4109 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑓 “ (𝑓 “ (𝑏 supp 0 )))) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
139127, 138sstrd 3957 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ((𝑓𝑆) ∖ (𝑏 supp 0 )))
140 fimacnv 6710 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓: 𝑆𝑆 → (𝑓𝑆) = 𝑆)
141119, 140syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓𝑆) = 𝑆)
142141difeq1d 4088 . . . . . . . . . . . . . . . . . . . 20 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → ((𝑓𝑆) ∖ (𝑏 supp 0 )) = ( 𝑆 ∖ (𝑏 supp 0 )))
143139, 142sseqtrd 3983 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
144143sselda 3946 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
145 ssidd 3970 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑏 supp 0 ) ⊆ (𝑏 supp 0 ))
14673adantr 480 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑆 ∈ V)
14775a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 0 ∈ V)
148129, 145, 146, 147suppssr 8174 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
149144, 148syldan 591 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → (𝑏𝑗) = 0 )
150149oveq1d 7402 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1515ad7antr 738 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑅 ∈ Ring)
15213ad7antr 738 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑆𝐵)
15340ad3antlr 731 . . . . . . . . . . . . . . . . . . 19 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑓 “ {𝑖}) ⊆ 𝑆)
154153sselda 3946 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗 𝑆)
155152, 154sseldd 3947 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → 𝑗𝐵)
156151, 155, 85syl2anc 584 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ( 0 · 𝑗) = 0 )
157150, 156eqtrd 2764 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) ∧ 𝑗 ∈ (𝑓 “ {𝑖})) → ((𝑏𝑗) · 𝑗) = 0 )
158118, 157mpteq2da 5199 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 ))
159158oveq2d 7403 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )))
1605, 28syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ CMnd)
161160cmnmndd 19734 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ Mnd)
162161ad6antr 736 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → 𝑅 ∈ Mnd)
1633gsumz 18763 . . . . . . . . . . . . . 14 ((𝑅 ∈ Mnd ∧ (𝑓 “ {𝑖}) ∈ V) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
164162, 33, 163sylancl 586 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ 0 )) = 0 )
165159, 164eqtrd 2764 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖 ∈ (𝑆 ∖ (𝑓 “ (𝑏 supp 0 )))) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = 0 )
166165, 106suppss2 8179 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ⊆ (𝑓 “ (𝑏 supp 0 )))
167116, 166ssfid 9212 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)
168 isfsupp 9316 . . . . . . . . . . 11 (((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 ↔ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)))
169168biimpar 477 . . . . . . . . . 10 ((((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∈ V ∧ 0 ∈ V) ∧ (Fun (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) ∧ ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) supp 0 ) ∈ Fin)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
170107, 108, 110, 167, 169syl22anc 838 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0 )
171 simpllr 775 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))
17226, 160syl 17 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑅 ∈ CMnd)
1735ad6antr 736 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
17436ad5antlr 735 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑏: 𝑆𝐵)
175174ffvelcdmda 7056 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → (𝑏𝑗) ∈ 𝐵)
17626, 13syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆𝐵)
177176sselda 3946 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → 𝑗𝐵)
1782, 4ringcl 20159 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ (𝑏𝑗) ∈ 𝐵𝑗𝐵) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
179173, 175, 177, 178syl3anc 1373 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 𝑆) → ((𝑏𝑗) · 𝑗) ∈ 𝐵)
180 eqid 2729 . . . . . . . . . . . 12 (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
18166, 179, 180fmptdf 7089 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)): 𝑆𝐵)
18273mptexd 7198 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
183 funmpt 6554 . . . . . . . . . . . . 13 Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))
184183a1i 11 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))
185 nfcv 2891 . . . . . . . . . . . . 13 𝑗 𝑆
186174adantr 480 . . . . . . . . . . . . . . . . 17 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
187186ffnd 6689 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
18873adantr 480 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
18975a1i 11 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 0 ∈ V)
190 simpr 484 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
191187, 188, 189, 190fvdifsupp 8150 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
192191oveq1d 7402 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
1935ad6antr 736 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑅 ∈ Ring)
194176adantr 480 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
195190eldifad 3926 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
196194, 195sseldd 3947 . . . . . . . . . . . . . . 15 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
197193, 196, 85syl2anc 584 . . . . . . . . . . . . . 14 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
198192, 197eqtrd 2764 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
19966, 185, 70, 198, 73suppss2f 32562 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
200 fsuppsssupp 9332 . . . . . . . . . . . 12 ((((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
201182, 184, 113, 199, 200syl22anc 838 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
202 sndisj 5099 . . . . . . . . . . . 12 Disj 𝑖𝑆 {𝑖}
203 disjpreima 32513 . . . . . . . . . . . 12 ((Fun 𝑓Disj 𝑖𝑆 {𝑖}) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
204112, 202, 203sylancl 586 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → Disj 𝑖𝑆 (𝑓 “ {𝑖}))
205 iunid 5024 . . . . . . . . . . . . 13 𝑖𝑆 {𝑖} = 𝑆
206205imaeq2i 6029 . . . . . . . . . . . 12 (𝑓 𝑖𝑆 {𝑖}) = (𝑓𝑆)
207 iunpreima 32493 . . . . . . . . . . . . 13 (Fun 𝑓 → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
208112, 207syl 17 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓 𝑖𝑆 {𝑖}) = 𝑖𝑆 (𝑓 “ {𝑖}))
209140ad2antlr 727 . . . . . . . . . . . 12 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑓𝑆) = 𝑆)
210206, 208, 2093eqtr3a 2788 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑖𝑆 (𝑓 “ {𝑖}) = 𝑆)
2112, 3, 172, 73, 106, 181, 201, 204, 210gsumpart 32997 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))))
21241resmptd 6011 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})) = (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))
213212oveq2d 7403 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑖𝑆) → (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
214213mpteq2dva 5200 . . . . . . . . . . 11 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖})))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))))
215214oveq2d 7403 . . . . . . . . . 10 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg ((𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) ↾ (𝑓 “ {𝑖}))))) = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
216171, 211, 2153eqtrd 2768 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))))
217 eqid 2729 . . . . . . . . . . . 12 (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) = (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))
218 simpr 484 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
219218sneqd 4601 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → {𝑖} = {𝑘})
220219imaeq2d 6031 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑓 “ {𝑖}) = (𝑓 “ {𝑘}))
221220mpteq1d 5197 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
222221oveq2d 7403 . . . . . . . . . . . 12 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑖 = 𝑘) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
223 simpr 484 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘𝑆)
224 ovexd 7422 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ V)
225217, 222, 223, 224fvmptd2 6976 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) = (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))))
226160ad6antr 736 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ CMnd)
22730cnvex 7901 . . . . . . . . . . . . . 14 𝑓 ∈ V
228227imaex 7890 . . . . . . . . . . . . 13 (𝑓 “ {𝑘}) ∈ V
229228a1i 11 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ∈ V)
2305ad6antr 736 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑅 ∈ Ring)
23126, 6syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → 𝑆 ⊆ (LIdeal‘𝑅))
232231sselda 3946 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (LIdeal‘𝑅))
2338lidlsubg 21133 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubGrp‘𝑅))
234 subgsubm 19080 . . . . . . . . . . . . . 14 (𝑘 ∈ (SubGrp‘𝑅) → 𝑘 ∈ (SubMnd‘𝑅))
235233, 234syl 17 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) → 𝑘 ∈ (SubMnd‘𝑅))
236230, 232, 235syl2anc 584 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑘 ∈ (SubMnd‘𝑅))
237230adantr 480 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑅 ∈ Ring)
238232adantr 480 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑘 ∈ (LIdeal‘𝑅))
23936ad7antlr 739 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑏: 𝑆𝐵)
240 cnvimass 6053 . . . . . . . . . . . . . . . . . 18 (𝑓 “ {𝑘}) ⊆ dom 𝑓
241240, 39sseqtrid 3989 . . . . . . . . . . . . . . . . 17 (𝑓: 𝑆𝑆 → (𝑓 “ {𝑘}) ⊆ 𝑆)
242241ad3antlr 731 . . . . . . . . . . . . . . . 16 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑓 “ {𝑘}) ⊆ 𝑆)
243242sselda 3946 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 𝑆)
244239, 243ffvelcdmd 7057 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑏𝑙) ∈ 𝐵)
245 fveq2 6858 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑙 → (𝑓𝑗) = (𝑓𝑙))
24649, 245eleq12d 2822 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑙 → (𝑗 ∈ (𝑓𝑗) ↔ 𝑙 ∈ (𝑓𝑙)))
247 simpllr 775 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))
248246, 247, 243rspcdva 3589 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙 ∈ (𝑓𝑙))
249 simp-4r 783 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓: 𝑆𝑆)
250249ffnd 6689 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑓 Fn 𝑆)
251 elpreima 7030 . . . . . . . . . . . . . . . . . 18 (𝑓 Fn 𝑆 → (𝑙 ∈ (𝑓 “ {𝑘}) ↔ (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘})))
252251biimpa 476 . . . . . . . . . . . . . . . . 17 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑙 𝑆 ∧ (𝑓𝑙) ∈ {𝑘}))
253 elsni 4606 . . . . . . . . . . . . . . . . 17 ((𝑓𝑙) ∈ {𝑘} → (𝑓𝑙) = 𝑘)
254252, 253simpl2im 503 . . . . . . . . . . . . . . . 16 ((𝑓 Fn 𝑆𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
255250, 254sylancom 588 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → (𝑓𝑙) = 𝑘)
256248, 255eleqtrd 2830 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → 𝑙𝑘)
2578, 2, 4lidlmcl 21135 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ 𝑘 ∈ (LIdeal‘𝑅)) ∧ ((𝑏𝑙) ∈ 𝐵𝑙𝑘)) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
258237, 238, 244, 256, 257syl22anc 838 . . . . . . . . . . . . 13 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑙 ∈ (𝑓 “ {𝑘})) → ((𝑏𝑙) · 𝑙) ∈ 𝑘)
25950cbvmptv 5211 . . . . . . . . . . . . 13 (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) = (𝑙 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑙) · 𝑙))
260258, 259fmptd 7086 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)):(𝑓 “ {𝑘})⟶𝑘)
261229mptexd 7198 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V)
262260ffund 6692 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)))
263 simp-5r 785 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → 𝑏 finSupp 0 )
264 nfv 1914 . . . . . . . . . . . . . . 15 𝑗 𝑘𝑆
26566, 264nfan 1899 . . . . . . . . . . . . . 14 𝑗((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆)
266 nfcv 2891 . . . . . . . . . . . . . 14 𝑗(𝑓 “ {𝑘})
26736ad7antlr 739 . . . . . . . . . . . . . . . . . 18 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏: 𝑆𝐵)
268267ffnd 6689 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑏 Fn 𝑆)
26973ad2antrr 726 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆 ∈ V)
27075a1i 11 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 0 ∈ V)
271242ssdifd 4108 . . . . . . . . . . . . . . . . . 18 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 )) ⊆ ( 𝑆 ∖ (𝑏 supp 0 )))
272271sselda 3946 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 ∈ ( 𝑆 ∖ (𝑏 supp 0 )))
273268, 269, 270, 272fvdifsupp 8150 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → (𝑏𝑗) = 0 )
274273oveq1d 7402 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = ( 0 · 𝑗))
27513ad7antr 738 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑆𝐵)
276272eldifad 3926 . . . . . . . . . . . . . . . . 17 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗 𝑆)
277275, 276sseldd 3947 . . . . . . . . . . . . . . . 16 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → 𝑗𝐵)
278230, 277, 85syl2an2r 685 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ( 0 · 𝑗) = 0 )
279274, 278eqtrd 2764 . . . . . . . . . . . . . 14 ((((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) ∧ 𝑗 ∈ ((𝑓 “ {𝑘}) ∖ (𝑏 supp 0 ))) → ((𝑏𝑗) · 𝑗) = 0 )
280265, 266, 70, 279, 229suppss2f 32562 . . . . . . . . . . . . 13 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))
281 fsuppsssupp 9332 . . . . . . . . . . . . 13 ((((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) ∈ V ∧ Fun (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∧ (𝑏 finSupp 0 ∧ ((𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) supp 0 ) ⊆ (𝑏 supp 0 ))) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
282261, 262, 263, 280, 281syl22anc 838 . . . . . . . . . . . 12 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗)) finSupp 0 )
2833, 226, 229, 236, 260, 282gsumsubmcl 19849 . . . . . . . . . . 11 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑘}) ↦ ((𝑏𝑗) · 𝑗))) ∈ 𝑘)
284225, 283eqeltrd 2828 . . . . . . . . . 10 (((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) ∧ 𝑘𝑆) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
285284ralrimiva 3125 . . . . . . . . 9 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘)
286170, 216, 2853jca 1128 . . . . . . . 8 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗)))) finSupp 0𝑋 = (𝑅 Σg (𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))) ∧ ∀𝑘𝑆 ((𝑖𝑆 ↦ (𝑅 Σg (𝑗 ∈ (𝑓 “ {𝑖}) ↦ ((𝑏𝑗) · 𝑗))))‘𝑘) ∈ 𝑘))
28797, 105, 286rspcedvd 3590 . . . . . . 7 ((((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ 𝑓: 𝑆𝑆) ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗)) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
288287anasss 466 . . . . . 6 (((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ∧ (𝑓: 𝑆𝑆 ∧ ∀𝑗 𝑆𝑗 ∈ (𝑓𝑗))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
28925, 288exlimddv 1935 . . . . 5 ((((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
290289anasss 466 . . . 4 (((𝜑𝑏 ∈ (𝐵m 𝑆)) ∧ (𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
291290r19.29an 3137 . . 3 ((𝜑 ∧ ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))) → ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘))
2925ad4antr 732 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑅 ∈ Ring)
293292adantr 480 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
294 eqid 2729 . . . . . . . . . . . . . 14 (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
295294zrhrhm 21421 . . . . . . . . . . . . 13 (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
296 zringbas 21363 . . . . . . . . . . . . . 14 ℤ = (Base‘ℤring)
297296, 2rhmf 20394 . . . . . . . . . . . . 13 ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
298293, 295, 2973syl 18 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (ℤRHom‘𝑅):ℤ⟶𝐵)
299 simp-5r 785 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
30075a1i 11 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
301 ssv 3971 . . . . . . . . . . . . . . . . . 18 ran 𝑎 ⊆ V
302 ssdif 4107 . . . . . . . . . . . . . . . . . 18 (ran 𝑎 ⊆ V → (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 }))
303301, 302ax-mp 5 . . . . . . . . . . . . . . . . 17 (ran 𝑎 ∖ { 0 }) ⊆ (V ∖ { 0 })
304303sseli 3942 . . . . . . . . . . . . . . . 16 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) → 𝑚 ∈ (V ∖ { 0 }))
305304adantl 481 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑚 ∈ (V ∖ { 0 }))
306 simp-4r 783 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
307299, 300, 305, 306fsuppinisegfi 32610 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑚}) ∈ Fin)
308 hashcl 14321 . . . . . . . . . . . . . 14 ((𝑎 “ {𝑚}) ∈ Fin → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
309307, 308syl 17 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℕ0)
310309nn0zd 12555 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑚})) ∈ ℤ)
311298, 310ffvelcdmd 7057 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑚 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ 𝐵)
312 eqid 2729 . . . . . . . . . . 11 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) = (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))
313311, 312fmptd 7086 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))):(ran 𝑎 ∖ { 0 })⟶𝐵)
3142, 3ring0cl 20176 . . . . . . . . . . 11 (𝑅 ∈ Ring → 0𝐵)
315 fconst6g 6749 . . . . . . . . . . 11 ( 0𝐵 → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
316292, 314, 3153syl 18 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }):( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))⟶𝐵)
317 disjdif 4435 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅
318317a1i 11 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∩ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = ∅)
319313, 316, 318fun2d 6724 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵)
320 simplll 774 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝜑𝑎 ∈ (𝐵m 𝑆)))
32194, 16elmapd 8813 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑎 ∈ (𝐵m 𝑆) ↔ 𝑎:𝑆𝐵))
322321biimpa 476 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → 𝑎:𝑆𝐵)
323320, 322syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎:𝑆𝐵)
324323ffnd 6689 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 Fn 𝑆)
325 elssuni 4901 . . . . . . . . . . . . . . . . 17 (𝑘𝑆𝑘 𝑆)
326325adantl 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → 𝑘 𝑆)
327326sseld 3945 . . . . . . . . . . . . . . 15 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ 𝑘𝑆) → ((𝑎𝑘) ∈ 𝑘 → (𝑎𝑘) ∈ 𝑆))
328327ralimdva 3145 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆))
329328imp 406 . . . . . . . . . . . . 13 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆)
330 fnfvrnss 7093 . . . . . . . . . . . . 13 ((𝑎 Fn 𝑆 ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑆) → ran 𝑎 𝑆)
331324, 329, 330syl2anc 584 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ran 𝑎 𝑆)
332331ssdifssd 4110 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝑆)
333 undif 4445 . . . . . . . . . . 11 ((ran 𝑎 ∖ { 0 }) ⊆ 𝑆 ↔ ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
334332, 333sylib 218 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) = 𝑆)
335334feq2d 6672 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })):((ran 𝑎 ∖ { 0 }) ∪ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })))⟶𝐵 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
336319, 335mpbid 232 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵)
33793a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝐵 ∈ V)
33817ad4antr 732 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆 ∈ V)
339337, 338elmapd 8813 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆) ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })): 𝑆𝐵))
340336, 339mpbird 257 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ (𝐵m 𝑆))
341 breq1 5110 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏 finSupp 0 ↔ ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 ))
342 fveq1 6857 . . . . . . . . . . . . 13 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑏𝑗) = (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗))
343342oveq1d 7402 . . . . . . . . . . . 12 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → ((𝑏𝑗) · 𝑗) = ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))
344343mpteq2dv 5201 . . . . . . . . . . 11 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)) = (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))
345344oveq2d 7403 . . . . . . . . . 10 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
346345eqeq2d 2740 . . . . . . . . 9 (𝑏 = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) → (𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))) ↔ 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
347341, 346anbi12d 632 . . . . . . . 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 481 . . . . . . 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 6692 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })))
350340elexd 3471 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) ∈ V)
35175a1i 11 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 0 ∈ V)
352323ffund 6692 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → Fun 𝑎)
353320simprd 495 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 ∈ (𝐵m 𝑆))
354 simpllr 775 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑎 finSupp 0 )
355 fsupprnfi 32615 . . . . . . . . . . . . 13 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → ran 𝑎 ∈ Fin)
356 diffi 9139 . . . . . . . . . . . . 13 (ran 𝑎 ∈ Fin → (ran 𝑎 ∖ { 0 }) ∈ Fin)
357355, 356syl 17 . . . . . . . . . . . 12 (((Fun 𝑎𝑎 ∈ (𝐵m 𝑆)) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 )) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
358352, 353, 351, 354, 357syl22anc 838 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ∈ Fin)
359313, 358, 351fdmfifsupp 9326 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) finSupp 0 )
36013ssdifssd 4110 . . . . . . . . . . . . 13 (𝜑 → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
361360ad4antr 732 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ⊆ 𝐵)
362337, 361ssexd 5279 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) ∈ V)
363362, 351fczfsuppd 9337 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }) finSupp 0 )
364359, 363fsuppun 9338 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) supp 0 ) ∈ Fin)
365 funisfsupp 9318 . . . . . . . . . 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 477 . . . . . . . . 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 1375 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0 )
368 fvex 6871 . . . . . . . . . . . . . . . 16 ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) ∈ V
369368, 312fnmpti 6661 . . . . . . . . . . . . . . 15 (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 })
370369a1i 11 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) Fn (ran 𝑎 ∖ { 0 }))
371 fnconstg 6748 . . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (ran 𝑎 ∖ { 0 }))
376370, 373, 374, 375fvun1d 6954 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗))
377 sneq 4599 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → {𝑚} = {𝑗})
378377imaeq2d 6031 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → (𝑎 “ {𝑚}) = (𝑎 “ {𝑗}))
379378fveq2d 6862 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (♯‘(𝑎 “ {𝑚})) = (♯‘(𝑎 “ {𝑗})))
380379fveq2d 6862 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
381 fvexd 6873 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) ∈ V)
382312, 380, 375, 381fvmptd3 6991 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚}))))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
383376, 382eqtrd 2764 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))))
384383oveq1d 7402 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))
385384mpteq2dva 5200 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)))
386385oveq2d 7403 . . . . . . . . 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 6953 . . . . . . . . . . . . . . 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 1453 . . . . . . . . . . . . . 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 7178 . . . . . . . . . . . . . 14 (𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
393392adantl 481 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })‘𝑗) = 0 )
394391, 393eqtrd 2764 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) = 0 )
395394oveq1d 7402 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = ( 0 · 𝑗))
396361sselda 3946 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → 𝑗𝐵)
397292, 396, 85syl2an2r 685 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ( 0 · 𝑗) = 0 )
398395, 397eqtrd 2764 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ ( 𝑆 ∖ (ran 𝑎 ∖ { 0 }))) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) = 0 )
399292adantr 480 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑅 ∈ Ring)
400336ffvelcdmda 7056 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵)
40113ad4antr 732 . . . . . . . . . . . 12 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑆𝐵)
402401sselda 3946 . . . . . . . . . . 11 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → 𝑗𝐵)
4032, 4ringcl 20159 . . . . . . . . . . 11 ((𝑅 ∈ Ring ∧ (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) ∈ 𝐵𝑗𝐵) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
404399, 400, 402, 403syl3anc 1373 . . . . . . . . . 10 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 𝑆) → ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗) ∈ 𝐵)
4052, 3, 387, 338, 398, 358, 404, 332gsummptres2 32993 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
406 eqid 2729 . . . . . . . . . . 11 (.g𝑅) = (.g𝑅)
4072, 3, 406, 387, 323, 354gsumhashmul 33001 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg 𝑎) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
408 simplr 768 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg 𝑎))
409292adantr 480 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑅 ∈ Ring)
410353adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 ∈ (𝐵m 𝑆))
41175a1i 11 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 0 ∈ V)
412303, 375sselid 3944 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗 ∈ (V ∖ { 0 }))
413354adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑎 finSupp 0 )
414410, 411, 412, 413fsuppinisegfi 32610 . . . . . . . . . . . . . . 15 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (𝑎 “ {𝑗}) ∈ Fin)
415 hashcl 14321 . . . . . . . . . . . . . . 15 ((𝑎 “ {𝑗}) ∈ Fin → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
416414, 415syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℕ0)
417416nn0zd 12555 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
418332, 401sstrd 3957 . . . . . . . . . . . . . 14 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (ran 𝑎 ∖ { 0 }) ⊆ 𝐵)
419418sselda 3946 . . . . . . . . . . . . 13 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → 𝑗𝐵)
420 eqid 2729 . . . . . . . . . . . . . . . . 17 (1r𝑅) = (1r𝑅)
421294, 406, 420zrhmulg 21419 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
422421adantr 480 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)))
423422oveq1d 7402 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗))
424 simpll 766 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑅 ∈ Ring)
425 simplr 768 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (♯‘(𝑎 “ {𝑗})) ∈ ℤ)
4262, 420ringidcl 20174 . . . . . . . . . . . . . . . 16 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐵)
427426ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (1r𝑅) ∈ 𝐵)
428 simpr 484 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → 𝑗𝐵)
4292, 406, 4mulgass2 20218 . . . . . . . . . . . . . . 15 ((𝑅 ∈ Ring ∧ ((♯‘(𝑎 “ {𝑗})) ∈ ℤ ∧ (1r𝑅) ∈ 𝐵𝑗𝐵)) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
430424, 425, 427, 428, 429syl13anc 1374 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((♯‘(𝑎 “ {𝑗}))(.g𝑅)(1r𝑅)) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)))
4312, 4, 420ringlidm 20178 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
432424, 431sylancom 588 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((1r𝑅) · 𝑗) = 𝑗)
433432oveq2d 7403 . . . . . . . . . . . . . 14 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → ((♯‘(𝑎 “ {𝑗}))(.g𝑅)((1r𝑅) · 𝑗)) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
434423, 430, 4333eqtrd 2768 . . . . . . . . . . . . 13 (((𝑅 ∈ Ring ∧ (♯‘(𝑎 “ {𝑗})) ∈ ℤ) ∧ 𝑗𝐵) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
435409, 417, 419, 434syl21anc 837 . . . . . . . . . . . 12 ((((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) ∧ 𝑗 ∈ (ran 𝑎 ∖ { 0 })) → (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗) = ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))
436435mpteq2dva 5200 . . . . . . . . . . 11 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗)) = (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗)))
437436oveq2d 7403 . . . . . . . . . 10 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))) = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((♯‘(𝑎 “ {𝑗}))(.g𝑅)𝑗))))
438407, 408, 4373eqtr4d 2774 . . . . . . . . 9 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 ∈ (ran 𝑎 ∖ { 0 }) ↦ (((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑗}))) · 𝑗))))
439386, 405, 4383eqtr4rd 2775 . . . . . . . 8 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → 𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗))))
440367, 439jca 511 . . . . . . 7 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → (((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 })) finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((((𝑚 ∈ (ran 𝑎 ∖ { 0 }) ↦ ((ℤRHom‘𝑅)‘(♯‘(𝑎 “ {𝑚})))) ∪ (( 𝑆 ∖ (ran 𝑎 ∖ { 0 })) × { 0 }))‘𝑗) · 𝑗)))))
441340, 348, 440rspcedvd 3590 . . . . . 6 (((((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = (𝑅 Σg 𝑎)) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
442441exp41 434 . . . . 5 ((𝜑𝑎 ∈ (𝐵m 𝑆)) → (𝑎 finSupp 0 → (𝑋 = (𝑅 Σg 𝑎) → (∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘 → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗))))))))
4434423imp2 1350 . . . 4 (((𝜑𝑎 ∈ (𝐵m 𝑆)) ∧ (𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
444443r19.29an 3137 . . 3 ((𝜑 ∧ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)) → ∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))))
445291, 444impbida 800 . 2 (𝜑 → (∃𝑏 ∈ (𝐵m 𝑆)(𝑏 finSupp 0𝑋 = (𝑅 Σg (𝑗 𝑆 ↦ ((𝑏𝑗) · 𝑗)))) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
44614, 445bitrd 279 1 (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1540  wex 1779  wcel 2109  wral 3044  wrex 3053  Vcvv 3447  cdif 3911  cun 3912  cin 3913  wss 3914  c0 4296  {csn 4589   cuni 4871   ciun 4955  Disj wdisj 5074   class class class wbr 5107  cmpt 5188   × cxp 5636  ccnv 5637  dom cdm 5638  ran crn 5639  cres 5640  cima 5641  Fun wfun 6505   Fn wfn 6506  wf 6507  cfv 6511  (class class class)co 7387   supp csupp 8139  m cmap 8799  Fincfn 8918   finSupp cfsupp 9312  0cn0 12442  cz 12529  chash 14295  Basecbs 17179  .rcmulr 17221  0gc0g 17402   Σg cgsu 17403  Mndcmnd 18661  SubMndcsubmnd 18709  .gcmg 18999  SubGrpcsubg 19052  CMndccmn 19710  1rcur 20090  Ringcrg 20142   RingHom crh 20378  LIdealclidl 21116  RSpancrsp 21117  ringczring 21356  ℤRHomczrh 21409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-reg 9545  ax-inf2 9594  ax-ac2 10416  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-addf 11147  ax-mulf 11148
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-disj 5075  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-om 7843  df-1st 7968  df-2nd 7969  df-supp 8140  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-2o 8435  df-er 8671  df-map 8801  df-ixp 8871  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-fsupp 9313  df-sup 9393  df-oi 9463  df-r1 9717  df-rank 9718  df-card 9892  df-ac 10069  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-n0 12443  df-z 12530  df-dec 12650  df-uz 12794  df-fz 13469  df-fzo 13616  df-seq 13967  df-hash 14296  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-mre 17547  df-mrc 17548  df-acs 17550  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-mhm 18710  df-submnd 18711  df-grp 18868  df-minusg 18869  df-sbg 18870  df-mulg 19000  df-subg 19055  df-ghm 19145  df-cntz 19249  df-cmn 19712  df-abl 19713  df-mgp 20050  df-rng 20062  df-ur 20091  df-ring 20144  df-cring 20145  df-rhm 20381  df-nzr 20422  df-subrng 20455  df-subrg 20479  df-lmod 20768  df-lss 20838  df-lsp 20878  df-lmhm 20929  df-lbs 20982  df-sra 21080  df-rgmod 21081  df-lidl 21118  df-rsp 21119  df-cnfld 21265  df-zring 21357  df-zrh 21413  df-dsmm 21641  df-frlm 21656  df-uvc 21692
This theorem is referenced by:  zarcmplem  33871
  Copyright terms: Public domain W3C validator