Metamath Proof Explorer


Theorem elrspunidl

Description: Elementhood to the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024)

Ref Expression
Hypotheses elrspunidl.n 𝑁 = ( RSpan ‘ 𝑅 )
elrspunidl.b 𝐵 = ( Base ‘ 𝑅 )
elrspunidl.1 0 = ( 0g𝑅 )
elrspunidl.x · = ( .r𝑅 )
elrspunidl.r ( 𝜑𝑅 ∈ Ring )
elrspunidl.i ( 𝜑𝑆 ⊆ ( LIdeal ‘ 𝑅 ) )
Assertion elrspunidl ( 𝜑 → ( 𝑋 ∈ ( 𝑁 𝑆 ) ↔ ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 elrspunidl.n 𝑁 = ( RSpan ‘ 𝑅 )
2 elrspunidl.b 𝐵 = ( Base ‘ 𝑅 )
3 elrspunidl.1 0 = ( 0g𝑅 )
4 elrspunidl.x · = ( .r𝑅 )
5 elrspunidl.r ( 𝜑𝑅 ∈ Ring )
6 elrspunidl.i ( 𝜑𝑆 ⊆ ( LIdeal ‘ 𝑅 ) )
7 6 sselda ( ( 𝜑𝑖𝑆 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
8 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
9 2 8 lidlss ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖𝐵 )
10 7 9 syl ( ( 𝜑𝑖𝑆 ) → 𝑖𝐵 )
11 10 ralrimiva ( 𝜑 → ∀ 𝑖𝑆 𝑖𝐵 )
12 unissb ( 𝑆𝐵 ↔ ∀ 𝑖𝑆 𝑖𝐵 )
13 11 12 sylibr ( 𝜑 𝑆𝐵 )
14 1 2 3 4 5 13 elrsp ( 𝜑 → ( 𝑋 ∈ ( 𝑁 𝑆 ) ↔ ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) )
15 fvexd ( 𝜑 → ( LIdeal ‘ 𝑅 ) ∈ V )
16 15 6 ssexd ( 𝜑𝑆 ∈ V )
17 16 uniexd ( 𝜑 𝑆 ∈ V )
18 eluni2 ( 𝑗 𝑆 ↔ ∃ 𝑖𝑆 𝑗𝑖 )
19 18 biimpi ( 𝑗 𝑆 → ∃ 𝑖𝑆 𝑗𝑖 )
20 19 adantl ( ( 𝜑𝑗 𝑆 ) → ∃ 𝑖𝑆 𝑗𝑖 )
21 20 ralrimiva ( 𝜑 → ∀ 𝑗 𝑆𝑖𝑆 𝑗𝑖 )
22 eleq2 ( 𝑖 = ( 𝑓𝑗 ) → ( 𝑗𝑖𝑗 ∈ ( 𝑓𝑗 ) ) )
23 22 ac6sg ( 𝑆 ∈ V → ( ∀ 𝑗 𝑆𝑖𝑆 𝑗𝑖 → ∃ 𝑓 ( 𝑓 : 𝑆𝑆 ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ) )
24 17 21 23 sylc ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑆𝑆 ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) )
25 24 ad3antrrr ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑆𝑆 ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) )
26 simp-5l ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝜑 )
27 26 adantr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → 𝜑 )
28 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
29 27 5 28 3syl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → 𝑅 ∈ CMnd )
30 vex 𝑓 ∈ V
31 cnvexg ( 𝑓 ∈ V → 𝑓 ∈ V )
32 imaexg ( 𝑓 ∈ V → ( 𝑓 “ { 𝑖 } ) ∈ V )
33 30 31 32 mp2b ( 𝑓 “ { 𝑖 } ) ∈ V
34 33 a1i ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑓 “ { 𝑖 } ) ∈ V )
35 5 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑅 ∈ Ring )
36 elmapi ( 𝑏 ∈ ( 𝐵m 𝑆 ) → 𝑏 : 𝑆𝐵 )
37 36 ad7antlr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑏 : 𝑆𝐵 )
38 cnvimass ( 𝑓 “ { 𝑖 } ) ⊆ dom 𝑓
39 fdm ( 𝑓 : 𝑆𝑆 → dom 𝑓 = 𝑆 )
40 38 39 sseqtrid ( 𝑓 : 𝑆𝑆 → ( 𝑓 “ { 𝑖 } ) ⊆ 𝑆 )
41 40 ad3antlr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑓 “ { 𝑖 } ) ⊆ 𝑆 )
42 41 sselda ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑙 𝑆 )
43 37 42 ffvelrnd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → ( 𝑏𝑙 ) ∈ 𝐵 )
44 13 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑆𝐵 )
45 44 42 sseldd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑙𝐵 )
46 2 4 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑏𝑙 ) ∈ 𝐵𝑙𝐵 ) → ( ( 𝑏𝑙 ) · 𝑙 ) ∈ 𝐵 )
47 35 43 45 46 syl3anc ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ) → ( ( 𝑏𝑙 ) · 𝑙 ) ∈ 𝐵 )
48 fveq2 ( 𝑗 = 𝑙 → ( 𝑏𝑗 ) = ( 𝑏𝑙 ) )
49 id ( 𝑗 = 𝑙𝑗 = 𝑙 )
50 48 49 oveq12d ( 𝑗 = 𝑙 → ( ( 𝑏𝑗 ) · 𝑗 ) = ( ( 𝑏𝑙 ) · 𝑙 ) )
51 50 cbvmptv ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) = ( 𝑙 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑙 ) · 𝑙 ) )
52 47 51 fmptd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) : ( 𝑓 “ { 𝑖 } ) ⟶ 𝐵 )
53 34 mptexd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ∈ V )
54 52 ffund ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → Fun ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
55 simp-5r ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → 𝑏 finSupp 0 )
56 nfv 𝑗 ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 )
57 nfcv 𝑗 𝑅
58 nfcv 𝑗 Σg
59 nfmpt1 𝑗 ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) )
60 57 58 59 nfov 𝑗 ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
61 60 nfeq2 𝑗 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
62 56 61 nfan 𝑗 ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
63 nfv 𝑗 𝑓 : 𝑆𝑆
64 62 63 nfan 𝑗 ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 )
65 nfra1 𝑗𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 )
66 64 65 nfan 𝑗 ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) )
67 nfv 𝑗 𝑖𝑆
68 66 67 nfan 𝑗 ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 )
69 nfcv 𝑗 ( 𝑓 “ { 𝑖 } )
70 nfcv 𝑗 ( 𝑏 supp 0 )
71 36 ad7antlr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑏 : 𝑆𝐵 )
72 71 ffnd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑏 Fn 𝑆 )
73 26 17 syl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑆 ∈ V )
74 73 ad2antrr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑆 ∈ V )
75 3 fvexi 0 ∈ V
76 75 a1i ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 0 ∈ V )
77 41 ssdifd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ⊆ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
78 77 sselda ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
79 72 74 76 78 fvdifsupp ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑏𝑗 ) = 0 )
80 79 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = ( 0 · 𝑗 ) )
81 5 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑅 ∈ Ring )
82 13 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑆𝐵 )
83 78 eldifad ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑗 𝑆 )
84 82 83 sseldd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑗𝐵 )
85 2 4 3 ringlz ( ( 𝑅 ∈ Ring ∧ 𝑗𝐵 ) → ( 0 · 𝑗 ) = 0 )
86 81 84 85 syl2anc ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( 0 · 𝑗 ) = 0 )
87 80 86 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑖 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = 0 )
88 68 69 70 87 34 suppss2f ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) supp 0 ) ⊆ ( 𝑏 supp 0 ) )
89 fsuppsssupp ( ( ( ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ∈ V ∧ Fun ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ∧ ( 𝑏 finSupp 0 ∧ ( ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) supp 0 ) ⊆ ( 𝑏 supp 0 ) ) ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) finSupp 0 )
90 53 54 55 88 89 syl22anc ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) finSupp 0 )
91 2 3 29 34 52 90 gsumcl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ∈ 𝐵 )
92 91 fmpttd ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) : 𝑆𝐵 )
93 2 fvexi 𝐵 ∈ V
94 93 a1i ( 𝜑𝐵 ∈ V )
95 94 16 elmapd ( 𝜑 → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∈ ( 𝐵m 𝑆 ) ↔ ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) : 𝑆𝐵 ) )
96 95 biimpar ( ( 𝜑 ∧ ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) : 𝑆𝐵 ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∈ ( 𝐵m 𝑆 ) )
97 26 92 96 syl2anc ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∈ ( 𝐵m 𝑆 ) )
98 breq1 ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( 𝑎 finSupp 0 ↔ ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0 ) )
99 oveq2 ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( 𝑅 Σg 𝑎 ) = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) )
100 99 eqeq2d ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( 𝑋 = ( 𝑅 Σg 𝑎 ) ↔ 𝑋 = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) ) )
101 fveq1 ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( 𝑎𝑘 ) = ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) )
102 101 eleq1d ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( ( 𝑎𝑘 ) ∈ 𝑘 ↔ ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) )
103 102 ralbidv ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ↔ ∀ 𝑘𝑆 ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) )
104 98 100 103 3anbi123d ( 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ( ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ↔ ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0𝑋 = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) ∧ ∀ 𝑘𝑆 ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) ) )
105 104 adantl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑎 = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) → ( ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ↔ ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0𝑋 = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) ∧ ∀ 𝑘𝑆 ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) ) )
106 26 16 syl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑆 ∈ V )
107 106 mptexd ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∈ V )
108 75 a1i ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 0 ∈ V )
109 funmpt Fun ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
110 109 a1i ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → Fun ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) )
111 simplr ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑓 : 𝑆𝑆 )
112 111 ffund ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → Fun 𝑓 )
113 simp-4r ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑏 finSupp 0 )
114 113 fsuppimpd ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑏 supp 0 ) ∈ Fin )
115 imafi ( ( Fun 𝑓 ∧ ( 𝑏 supp 0 ) ∈ Fin ) → ( 𝑓 “ ( 𝑏 supp 0 ) ) ∈ Fin )
116 112 114 115 syl2anc ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑓 “ ( 𝑏 supp 0 ) ) ∈ Fin )
117 nfv 𝑗 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) )
118 66 117 nfan 𝑗 ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) )
119 simpllr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → 𝑓 : 𝑆𝑆 )
120 119 ffund ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → Fun 𝑓 )
121 snssi ( 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) → { 𝑖 } ⊆ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) )
122 121 adantl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → { 𝑖 } ⊆ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) )
123 sspreima ( ( Fun 𝑓 ∧ { 𝑖 } ⊆ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ { 𝑖 } ) ⊆ ( 𝑓 “ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) )
124 120 122 123 syl2anc ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ { 𝑖 } ) ⊆ ( 𝑓 “ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) )
125 difpreima ( Fun 𝑓 → ( 𝑓 “ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) = ( ( 𝑓𝑆 ) ∖ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) )
126 120 125 syl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) = ( ( 𝑓𝑆 ) ∖ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) )
127 124 126 sseqtrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ { 𝑖 } ) ⊆ ( ( 𝑓𝑆 ) ∖ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) )
128 suppssdm ( 𝑏 supp 0 ) ⊆ dom 𝑏
129 36 ad6antlr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → 𝑏 : 𝑆𝐵 )
130 128 129 fssdm ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑏 supp 0 ) ⊆ 𝑆 )
131 119 fdmd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → dom 𝑓 = 𝑆 )
132 130 131 sseqtrrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑏 supp 0 ) ⊆ dom 𝑓 )
133 sseqin2 ( ( 𝑏 supp 0 ) ⊆ dom 𝑓 ↔ ( dom 𝑓 ∩ ( 𝑏 supp 0 ) ) = ( 𝑏 supp 0 ) )
134 133 biimpi ( ( 𝑏 supp 0 ) ⊆ dom 𝑓 → ( dom 𝑓 ∩ ( 𝑏 supp 0 ) ) = ( 𝑏 supp 0 ) )
135 dminss ( dom 𝑓 ∩ ( 𝑏 supp 0 ) ) ⊆ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) )
136 134 135 eqsstrrdi ( ( 𝑏 supp 0 ) ⊆ dom 𝑓 → ( 𝑏 supp 0 ) ⊆ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) )
137 132 136 syl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑏 supp 0 ) ⊆ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) )
138 137 sscond ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( ( 𝑓𝑆 ) ∖ ( 𝑓 “ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ⊆ ( ( 𝑓𝑆 ) ∖ ( 𝑏 supp 0 ) ) )
139 127 138 sstrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ { 𝑖 } ) ⊆ ( ( 𝑓𝑆 ) ∖ ( 𝑏 supp 0 ) ) )
140 fimacnv ( 𝑓 : 𝑆𝑆 → ( 𝑓𝑆 ) = 𝑆 )
141 119 140 syl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓𝑆 ) = 𝑆 )
142 141 difeq1d ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( ( 𝑓𝑆 ) ∖ ( 𝑏 supp 0 ) ) = ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
143 139 142 sseqtrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ { 𝑖 } ) ⊆ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
144 143 sselda ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
145 ssidd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑏 supp 0 ) ⊆ ( 𝑏 supp 0 ) )
146 73 adantr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → 𝑆 ∈ V )
147 75 a1i ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → 0 ∈ V )
148 129 145 146 147 suppssr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑏𝑗 ) = 0 )
149 144 148 syldan ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → ( 𝑏𝑗 ) = 0 )
150 149 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = ( 0 · 𝑗 ) )
151 5 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑅 ∈ Ring )
152 13 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑆𝐵 )
153 40 ad3antlr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑓 “ { 𝑖 } ) ⊆ 𝑆 )
154 153 sselda ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑗 𝑆 )
155 152 154 sseldd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → 𝑗𝐵 )
156 151 155 85 syl2anc ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → ( 0 · 𝑗 ) = 0 )
157 150 156 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) ∧ 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = 0 )
158 118 157 mpteq2da ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) = ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ 0 ) )
159 158 oveq2d ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ 0 ) ) )
160 5 28 syl ( 𝜑𝑅 ∈ CMnd )
161 160 cmnmndd ( 𝜑𝑅 ∈ Mnd )
162 161 ad6antr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → 𝑅 ∈ Mnd )
163 3 gsumz ( ( 𝑅 ∈ Mnd ∧ ( 𝑓 “ { 𝑖 } ) ∈ V ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ 0 ) ) = 0 )
164 162 33 163 sylancl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ 0 ) ) = 0 )
165 159 164 eqtrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖 ∈ ( 𝑆 ∖ ( 𝑓 “ ( 𝑏 supp 0 ) ) ) ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) = 0 )
166 165 106 suppss2 ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) supp 0 ) ⊆ ( 𝑓 “ ( 𝑏 supp 0 ) ) )
167 116 166 ssfid ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) supp 0 ) ∈ Fin )
168 isfsupp ( ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0 ↔ ( Fun ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) supp 0 ) ∈ Fin ) ) )
169 168 biimpar ( ( ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∈ V ∧ 0 ∈ V ) ∧ ( Fun ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) supp 0 ) ∈ Fin ) ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0 )
170 107 108 110 167 169 syl22anc ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0 )
171 simpllr ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
172 26 160 syl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑅 ∈ CMnd )
173 5 ad6antr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 𝑆 ) → 𝑅 ∈ Ring )
174 36 ad5antlr ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑏 : 𝑆𝐵 )
175 174 ffvelrnda ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 𝑆 ) → ( 𝑏𝑗 ) ∈ 𝐵 )
176 26 13 syl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑆𝐵 )
177 176 sselda ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 𝑆 ) → 𝑗𝐵 )
178 2 4 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑏𝑗 ) ∈ 𝐵𝑗𝐵 ) → ( ( 𝑏𝑗 ) · 𝑗 ) ∈ 𝐵 )
179 173 175 177 178 syl3anc ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 𝑆 ) → ( ( 𝑏𝑗 ) · 𝑗 ) ∈ 𝐵 )
180 eqid ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) = ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) )
181 66 179 180 fmptdf ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) : 𝑆𝐵 )
182 73 mptexd ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ∈ V )
183 funmpt Fun ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) )
184 183 a1i ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → Fun ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
185 nfcv 𝑗 𝑆
186 174 adantr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑏 : 𝑆𝐵 )
187 186 ffnd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑏 Fn 𝑆 )
188 73 adantr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑆 ∈ V )
189 75 a1i ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 0 ∈ V )
190 simpr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
191 187 188 189 190 fvdifsupp ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑏𝑗 ) = 0 )
192 191 oveq1d ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = ( 0 · 𝑗 ) )
193 5 ad6antr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑅 ∈ Ring )
194 176 adantr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑆𝐵 )
195 190 eldifad ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑗 𝑆 )
196 194 195 sseldd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → 𝑗𝐵 )
197 193 196 85 syl2anc ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → ( 0 · 𝑗 ) = 0 )
198 192 197 eqtrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = 0 )
199 66 185 70 198 73 suppss2f ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) supp 0 ) ⊆ ( 𝑏 supp 0 ) )
200 fsuppsssupp ( ( ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ∈ V ∧ Fun ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ∧ ( 𝑏 finSupp 0 ∧ ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) supp 0 ) ⊆ ( 𝑏 supp 0 ) ) ) → ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) finSupp 0 )
201 182 184 113 199 200 syl22anc ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) finSupp 0 )
202 sndisj Disj 𝑖𝑆 { 𝑖 }
203 disjpreima ( ( Fun 𝑓Disj 𝑖𝑆 { 𝑖 } ) → Disj 𝑖𝑆 ( 𝑓 “ { 𝑖 } ) )
204 112 202 203 sylancl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → Disj 𝑖𝑆 ( 𝑓 “ { 𝑖 } ) )
205 iunid 𝑖𝑆 { 𝑖 } = 𝑆
206 205 imaeq2i ( 𝑓 𝑖𝑆 { 𝑖 } ) = ( 𝑓𝑆 )
207 iunpreima ( Fun 𝑓 → ( 𝑓 𝑖𝑆 { 𝑖 } ) = 𝑖𝑆 ( 𝑓 “ { 𝑖 } ) )
208 112 207 syl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑓 𝑖𝑆 { 𝑖 } ) = 𝑖𝑆 ( 𝑓 “ { 𝑖 } ) )
209 140 ad2antlr ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑓𝑆 ) = 𝑆 )
210 206 208 209 3eqtr3a ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑖𝑆 ( 𝑓 “ { 𝑖 } ) = 𝑆 )
211 2 3 172 73 106 181 201 204 210 gsumpart ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ↾ ( 𝑓 “ { 𝑖 } ) ) ) ) ) )
212 41 resmptd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ↾ ( 𝑓 “ { 𝑖 } ) ) = ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
213 212 oveq2d ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑖𝑆 ) → ( 𝑅 Σg ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ↾ ( 𝑓 “ { 𝑖 } ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
214 213 mpteq2dva ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑖𝑆 ↦ ( 𝑅 Σg ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ↾ ( 𝑓 “ { 𝑖 } ) ) ) ) = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) )
215 214 oveq2d ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ↾ ( 𝑓 “ { 𝑖 } ) ) ) ) ) = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) )
216 171 211 215 3eqtrd ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑋 = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) )
217 eqid ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) = ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
218 simpr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑖 = 𝑘 ) → 𝑖 = 𝑘 )
219 218 sneqd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑖 = 𝑘 ) → { 𝑖 } = { 𝑘 } )
220 219 imaeq2d ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑖 = 𝑘 ) → ( 𝑓 “ { 𝑖 } ) = ( 𝑓 “ { 𝑘 } ) )
221 220 mpteq1d ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑖 = 𝑘 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) = ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
222 221 oveq2d ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑖 = 𝑘 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
223 simpr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → 𝑘𝑆 )
224 ovexd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ∈ V )
225 217 222 223 224 fvmptd2 ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) )
226 160 ad6antr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → 𝑅 ∈ CMnd )
227 30 cnvex 𝑓 ∈ V
228 227 imaex ( 𝑓 “ { 𝑘 } ) ∈ V
229 228 a1i ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑓 “ { 𝑘 } ) ∈ V )
230 5 ad6antr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → 𝑅 ∈ Ring )
231 26 6 syl ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → 𝑆 ⊆ ( LIdeal ‘ 𝑅 ) )
232 231 sselda ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) )
233 8 lidlsubg ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑘 ∈ ( SubGrp ‘ 𝑅 ) )
234 subgsubm ( 𝑘 ∈ ( SubGrp ‘ 𝑅 ) → 𝑘 ∈ ( SubMnd ‘ 𝑅 ) )
235 233 234 syl ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑘 ∈ ( SubMnd ‘ 𝑅 ) )
236 230 232 235 syl2anc ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → 𝑘 ∈ ( SubMnd ‘ 𝑅 ) )
237 230 adantr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑅 ∈ Ring )
238 232 adantr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑘 ∈ ( LIdeal ‘ 𝑅 ) )
239 36 ad7antlr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑏 : 𝑆𝐵 )
240 cnvimass ( 𝑓 “ { 𝑘 } ) ⊆ dom 𝑓
241 240 39 sseqtrid ( 𝑓 : 𝑆𝑆 → ( 𝑓 “ { 𝑘 } ) ⊆ 𝑆 )
242 241 ad3antlr ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑓 “ { 𝑘 } ) ⊆ 𝑆 )
243 242 sselda ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑙 𝑆 )
244 239 243 ffvelrnd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → ( 𝑏𝑙 ) ∈ 𝐵 )
245 fveq2 ( 𝑗 = 𝑙 → ( 𝑓𝑗 ) = ( 𝑓𝑙 ) )
246 49 245 eleq12d ( 𝑗 = 𝑙 → ( 𝑗 ∈ ( 𝑓𝑗 ) ↔ 𝑙 ∈ ( 𝑓𝑙 ) ) )
247 simpllr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) )
248 246 247 243 rspcdva ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑙 ∈ ( 𝑓𝑙 ) )
249 simp-4r ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑓 : 𝑆𝑆 )
250 249 ffnd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑓 Fn 𝑆 )
251 elpreima ( 𝑓 Fn 𝑆 → ( 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ↔ ( 𝑙 𝑆 ∧ ( 𝑓𝑙 ) ∈ { 𝑘 } ) ) )
252 251 biimpa ( ( 𝑓 Fn 𝑆𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → ( 𝑙 𝑆 ∧ ( 𝑓𝑙 ) ∈ { 𝑘 } ) )
253 elsni ( ( 𝑓𝑙 ) ∈ { 𝑘 } → ( 𝑓𝑙 ) = 𝑘 )
254 252 253 simpl2im ( ( 𝑓 Fn 𝑆𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → ( 𝑓𝑙 ) = 𝑘 )
255 250 254 sylancom ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → ( 𝑓𝑙 ) = 𝑘 )
256 248 255 eleqtrd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → 𝑙𝑘 )
257 8 2 4 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝑘 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑏𝑙 ) ∈ 𝐵𝑙𝑘 ) ) → ( ( 𝑏𝑙 ) · 𝑙 ) ∈ 𝑘 )
258 237 238 244 256 257 syl22anc ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ) → ( ( 𝑏𝑙 ) · 𝑙 ) ∈ 𝑘 )
259 50 cbvmptv ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) = ( 𝑙 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑙 ) · 𝑙 ) )
260 258 259 fmptd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) : ( 𝑓 “ { 𝑘 } ) ⟶ 𝑘 )
261 229 mptexd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ∈ V )
262 260 ffund ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → Fun ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) )
263 simp-5r ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → 𝑏 finSupp 0 )
264 nfv 𝑗 𝑘𝑆
265 66 264 nfan 𝑗 ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 )
266 nfcv 𝑗 ( 𝑓 “ { 𝑘 } )
267 36 ad7antlr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑏 : 𝑆𝐵 )
268 267 ffnd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑏 Fn 𝑆 )
269 73 ad2antrr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑆 ∈ V )
270 75 a1i ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 0 ∈ V )
271 242 ssdifd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ⊆ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
272 271 sselda ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑗 ∈ ( 𝑆 ∖ ( 𝑏 supp 0 ) ) )
273 268 269 270 272 fvdifsupp ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( 𝑏𝑗 ) = 0 )
274 273 oveq1d ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = ( 0 · 𝑗 ) )
275 13 ad7antr ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑆𝐵 )
276 272 eldifad ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑗 𝑆 )
277 275 276 sseldd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → 𝑗𝐵 )
278 230 277 85 syl2an2r ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( 0 · 𝑗 ) = 0 )
279 274 278 eqtrd ( ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) ∧ 𝑗 ∈ ( ( 𝑓 “ { 𝑘 } ) ∖ ( 𝑏 supp 0 ) ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = 0 )
280 265 266 70 279 229 suppss2f ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) supp 0 ) ⊆ ( 𝑏 supp 0 ) )
281 fsuppsssupp ( ( ( ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ∈ V ∧ Fun ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ∧ ( 𝑏 finSupp 0 ∧ ( ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) supp 0 ) ⊆ ( 𝑏 supp 0 ) ) ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) finSupp 0 )
282 261 262 263 280 281 syl22anc ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) finSupp 0 )
283 3 226 229 236 260 282 gsumsubmcl ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑘 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ∈ 𝑘 )
284 225 283 eqeltrd ( ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ∧ 𝑘𝑆 ) → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 )
285 284 ralrimiva ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ∀ 𝑘𝑆 ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 )
286 170 216 285 3jca ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) finSupp 0𝑋 = ( 𝑅 Σg ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) ∧ ∀ 𝑘𝑆 ( ( 𝑖𝑆 ↦ ( 𝑅 Σg ( 𝑗 ∈ ( 𝑓 “ { 𝑖 } ) ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ‘ 𝑘 ) ∈ 𝑘 ) )
287 97 105 286 rspcedvd ( ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ 𝑓 : 𝑆𝑆 ) ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) → ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) )
288 287 anasss ( ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ∧ ( 𝑓 : 𝑆𝑆 ∧ ∀ 𝑗 𝑆 𝑗 ∈ ( 𝑓𝑗 ) ) ) → ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) )
289 25 288 exlimddv ( ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑏 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) → ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) )
290 289 anasss ( ( ( 𝜑𝑏 ∈ ( 𝐵m 𝑆 ) ) ∧ ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) → ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) )
291 290 r19.29an ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) → ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) )
292 5 ad4antr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑅 ∈ Ring )
293 292 adantr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
294 eqid ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
295 294 zrhrhm ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
296 zringbas ℤ = ( Base ‘ ℤring )
297 296 2 rhmf ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ 𝐵 )
298 293 295 297 3syl ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ 𝐵 )
299 simp-5r ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑎 ∈ ( 𝐵m 𝑆 ) )
300 75 a1i ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 0 ∈ V )
301 ssv ran 𝑎 ⊆ V
302 ssdif ( ran 𝑎 ⊆ V → ( ran 𝑎 ∖ { 0 } ) ⊆ ( V ∖ { 0 } ) )
303 301 302 ax-mp ( ran 𝑎 ∖ { 0 } ) ⊆ ( V ∖ { 0 } )
304 303 sseli ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) → 𝑚 ∈ ( V ∖ { 0 } ) )
305 304 adantl ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑚 ∈ ( V ∖ { 0 } ) )
306 simp-4r ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑎 finSupp 0 )
307 299 300 305 306 fsuppinisegfi ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( 𝑎 “ { 𝑚 } ) ∈ Fin )
308 hashcl ( ( 𝑎 “ { 𝑚 } ) ∈ Fin → ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ∈ ℕ0 )
309 307 308 syl ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ∈ ℕ0 )
310 309 nn0zd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ∈ ℤ )
311 298 310 ffvelrnd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ∈ 𝐵 )
312 eqid ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) = ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) )
313 311 312 fmptd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) : ( ran 𝑎 ∖ { 0 } ) ⟶ 𝐵 )
314 2 3 ring0cl ( 𝑅 ∈ Ring → 0𝐵 )
315 fconst6g ( 0𝐵 → ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) : ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ⟶ 𝐵 )
316 292 314 315 3syl ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) : ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ⟶ 𝐵 )
317 disjdif ( ( ran 𝑎 ∖ { 0 } ) ∩ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = ∅
318 317 a1i ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( ran 𝑎 ∖ { 0 } ) ∩ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = ∅ )
319 313 316 318 fun2d ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) : ( ( ran 𝑎 ∖ { 0 } ) ∪ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) ⟶ 𝐵 )
320 simplll ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) )
321 94 16 elmapd ( 𝜑 → ( 𝑎 ∈ ( 𝐵m 𝑆 ) ↔ 𝑎 : 𝑆𝐵 ) )
322 321 biimpa ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) → 𝑎 : 𝑆𝐵 )
323 320 322 syl ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑎 : 𝑆𝐵 )
324 323 ffnd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑎 Fn 𝑆 )
325 elssuni ( 𝑘𝑆𝑘 𝑆 )
326 325 adantl ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ 𝑘𝑆 ) → 𝑘 𝑆 )
327 326 sseld ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ 𝑘𝑆 ) → ( ( 𝑎𝑘 ) ∈ 𝑘 → ( 𝑎𝑘 ) ∈ 𝑆 ) )
328 327 ralimdva ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) → ( ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 → ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑆 ) )
329 328 imp ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑆 )
330 fnfvrnss ( ( 𝑎 Fn 𝑆 ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑆 ) → ran 𝑎 𝑆 )
331 324 329 330 syl2anc ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ran 𝑎 𝑆 )
332 331 ssdifssd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ran 𝑎 ∖ { 0 } ) ⊆ 𝑆 )
333 undif ( ( ran 𝑎 ∖ { 0 } ) ⊆ 𝑆 ↔ ( ( ran 𝑎 ∖ { 0 } ) ∪ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = 𝑆 )
334 332 333 sylib ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( ran 𝑎 ∖ { 0 } ) ∪ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = 𝑆 )
335 334 feq2d ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) : ( ( ran 𝑎 ∖ { 0 } ) ∪ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) ⟶ 𝐵 ↔ ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) : 𝑆𝐵 ) )
336 319 335 mpbid ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) : 𝑆𝐵 )
337 93 a1i ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝐵 ∈ V )
338 17 ad4antr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑆 ∈ V )
339 337 338 elmapd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ∈ ( 𝐵m 𝑆 ) ↔ ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) : 𝑆𝐵 ) )
340 336 339 mpbird ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ∈ ( 𝐵m 𝑆 ) )
341 breq1 ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( 𝑏 finSupp 0 ↔ ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) finSupp 0 ) )
342 fveq1 ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( 𝑏𝑗 ) = ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) )
343 342 oveq1d ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( ( 𝑏𝑗 ) · 𝑗 ) = ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) )
344 343 mpteq2dv ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) = ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) )
345 344 oveq2d ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) )
346 345 eqeq2d ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ↔ 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) ) )
347 341 346 anbi12d ( 𝑏 = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) → ( ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ↔ ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) ) ) )
348 347 adantl ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵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 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) ) ) )
349 319 ffund ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → Fun ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) )
350 340 elexd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ∈ V )
351 75 a1i ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 0 ∈ V )
352 323 ffund ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → Fun 𝑎 )
353 320 simprd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑎 ∈ ( 𝐵m 𝑆 ) )
354 simpllr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑎 finSupp 0 )
355 fsupprnfi ( ( ( Fun 𝑎𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 ) ) → ran 𝑎 ∈ Fin )
356 diffi ( ran 𝑎 ∈ Fin → ( ran 𝑎 ∖ { 0 } ) ∈ Fin )
357 355 356 syl ( ( ( Fun 𝑎𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ ( 0 ∈ V ∧ 𝑎 finSupp 0 ) ) → ( ran 𝑎 ∖ { 0 } ) ∈ Fin )
358 352 353 351 354 357 syl22anc ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ran 𝑎 ∖ { 0 } ) ∈ Fin )
359 313 358 351 fdmfifsupp ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) finSupp 0 )
360 13 ssdifssd ( 𝜑 → ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ⊆ 𝐵 )
361 360 ad4antr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ⊆ 𝐵 )
362 337 361 ssexd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ∈ V )
363 362 351 fczfsuppd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) finSupp 0 )
364 359 363 fsuppun ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) supp 0 ) ∈ Fin )
365 funisfsupp ( ( 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 ) )
366 365 biimpar ( ( ( 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 )
367 349 350 351 364 366 syl31anc ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) finSupp 0 )
368 fvex ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ∈ V
369 368 312 fnmpti ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) Fn ( ran 𝑎 ∖ { 0 } )
370 369 a1i ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) Fn ( ran 𝑎 ∖ { 0 } ) )
371 fnconstg ( 0 ∈ V → ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) Fn ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) )
372 75 371 ax-mp ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) Fn ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) )
373 372 a1i ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) Fn ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) )
374 317 a1i ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ran 𝑎 ∖ { 0 } ) ∩ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = ∅ )
375 simpr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) )
376 370 373 374 375 fvun1d ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) = ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ‘ 𝑗 ) )
377 sneq ( 𝑚 = 𝑗 → { 𝑚 } = { 𝑗 } )
378 377 imaeq2d ( 𝑚 = 𝑗 → ( 𝑎 “ { 𝑚 } ) = ( 𝑎 “ { 𝑗 } ) )
379 378 fveq2d ( 𝑚 = 𝑗 → ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) = ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) )
380 379 fveq2d ( 𝑚 = 𝑗 → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) )
381 fvexd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) ∈ V )
382 312 380 375 381 fvmptd3 ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ‘ 𝑗 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) )
383 376 382 eqtrd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) = ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) )
384 383 oveq1d ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) )
385 384 mpteq2dva ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) = ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) ) )
386 385 oveq2d ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) ) ) )
387 292 28 syl ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑅 ∈ CMnd )
388 317 a1i ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ran 𝑎 ∖ { 0 } ) ∩ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = ∅ )
389 fvun2 ( ( ( 𝑚 ∈ ( 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 } ) ‘ 𝑗 ) )
390 369 372 389 mp3an12 ( ( ( ( ran 𝑎 ∖ { 0 } ) ∩ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) = ∅ ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) = ( ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ‘ 𝑗 ) )
391 388 390 sylancom ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) = ( ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ‘ 𝑗 ) )
392 75 fvconst2 ( 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ‘ 𝑗 ) = 0 )
393 392 adantl ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ‘ 𝑗 ) = 0 )
394 391 393 eqtrd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) = 0 )
395 394 oveq1d ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) = ( 0 · 𝑗 ) )
396 361 sselda ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → 𝑗𝐵 )
397 292 396 85 syl2an2r ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( 0 · 𝑗 ) = 0 )
398 395 397 eqtrd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) ) → ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) = 0 )
399 292 adantr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 𝑆 ) → 𝑅 ∈ Ring )
400 336 ffvelrnda ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 𝑆 ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) ∈ 𝐵 )
401 13 ad4antr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑆𝐵 )
402 401 sselda ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 𝑆 ) → 𝑗𝐵 )
403 2 4 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) ∈ 𝐵𝑗𝐵 ) → ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ∈ 𝐵 )
404 399 400 402 403 syl3anc ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 𝑆 ) → ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ∈ 𝐵 )
405 2 3 387 338 398 358 404 332 gsummptres2 ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) )
406 eqid ( .g𝑅 ) = ( .g𝑅 )
407 2 3 406 387 323 354 gsumhashmul ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑅 Σg 𝑎 ) = ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) 𝑗 ) ) ) )
408 simplr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑋 = ( 𝑅 Σg 𝑎 ) )
409 292 adantr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
410 353 adantr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑎 ∈ ( 𝐵m 𝑆 ) )
411 75 a1i ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 0 ∈ V )
412 303 375 sselid ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑗 ∈ ( V ∖ { 0 } ) )
413 354 adantr ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑎 finSupp 0 )
414 410 411 412 413 fsuppinisegfi ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( 𝑎 “ { 𝑗 } ) ∈ Fin )
415 hashcl ( ( 𝑎 “ { 𝑗 } ) ∈ Fin → ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℕ0 )
416 414 415 syl ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℕ0 )
417 416 nn0zd ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ )
418 332 401 sstrd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ran 𝑎 ∖ { 0 } ) ⊆ 𝐵 )
419 418 sselda ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → 𝑗𝐵 )
420 eqid ( 1r𝑅 ) = ( 1r𝑅 )
421 294 406 420 zrhmulg ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( 1r𝑅 ) ) )
422 421 adantr ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( 1r𝑅 ) ) )
423 422 oveq1d ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) = ( ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( 1r𝑅 ) ) · 𝑗 ) )
424 simpll ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → 𝑅 ∈ Ring )
425 simplr ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ )
426 2 420 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ 𝐵 )
427 426 ad2antrr ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( 1r𝑅 ) ∈ 𝐵 )
428 simpr ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → 𝑗𝐵 )
429 2 406 4 mulgass2 ( ( 𝑅 ∈ Ring ∧ ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ∧ ( 1r𝑅 ) ∈ 𝐵𝑗𝐵 ) ) → ( ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( 1r𝑅 ) ) · 𝑗 ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( ( 1r𝑅 ) · 𝑗 ) ) )
430 424 425 427 428 429 syl13anc ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( 1r𝑅 ) ) · 𝑗 ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( ( 1r𝑅 ) · 𝑗 ) ) )
431 2 4 420 ringlidm ( ( 𝑅 ∈ Ring ∧ 𝑗𝐵 ) → ( ( 1r𝑅 ) · 𝑗 ) = 𝑗 )
432 424 431 sylancom ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ( 1r𝑅 ) · 𝑗 ) = 𝑗 )
433 432 oveq2d ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) ( ( 1r𝑅 ) · 𝑗 ) ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) 𝑗 ) )
434 423 430 433 3eqtrd ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ∈ ℤ ) ∧ 𝑗𝐵 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) 𝑗 ) )
435 409 417 419 434 syl21anc ( ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ∧ 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) = ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) 𝑗 ) )
436 435 mpteq2dva ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) ) = ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) 𝑗 ) ) )
437 436 oveq2d ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ( .g𝑅 ) 𝑗 ) ) ) )
438 407 408 437 3eqtr4d ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑋 = ( 𝑅 Σg ( 𝑗 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑗 } ) ) ) · 𝑗 ) ) ) )
439 386 405 438 3eqtr4rd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → 𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) )
440 367 439 jca ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( ( ( 𝑚 ∈ ( ran 𝑎 ∖ { 0 } ) ↦ ( ( ℤRHom ‘ 𝑅 ) ‘ ( ♯ ‘ ( 𝑎 “ { 𝑚 } ) ) ) ) ∪ ( ( 𝑆 ∖ ( ran 𝑎 ∖ { 0 } ) ) × { 0 } ) ) ‘ 𝑗 ) · 𝑗 ) ) ) ) )
441 340 348 440 rspcedvd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ 𝑎 finSupp 0 ) ∧ 𝑋 = ( 𝑅 Σg 𝑎 ) ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) → ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) )
442 441 exp41 ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) → ( 𝑎 finSupp 0 → ( 𝑋 = ( 𝑅 Σg 𝑎 ) → ( ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 → ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ) ) ) )
443 442 3imp2 ( ( ( 𝜑𝑎 ∈ ( 𝐵m 𝑆 ) ) ∧ ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ) → ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) )
444 443 r19.29an ( ( 𝜑 ∧ ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ) → ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) )
445 291 444 impbida ( 𝜑 → ( ∃ 𝑏 ∈ ( 𝐵m 𝑆 ) ( 𝑏 finSupp 0𝑋 = ( 𝑅 Σg ( 𝑗 𝑆 ↦ ( ( 𝑏𝑗 ) · 𝑗 ) ) ) ) ↔ ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ) )
446 14 445 bitrd ( 𝜑 → ( 𝑋 ∈ ( 𝑁 𝑆 ) ↔ ∃ 𝑎 ∈ ( 𝐵m 𝑆 ) ( 𝑎 finSupp 0𝑋 = ( 𝑅 Σg 𝑎 ) ∧ ∀ 𝑘𝑆 ( 𝑎𝑘 ) ∈ 𝑘 ) ) )