Metamath Proof Explorer


Theorem elrspunidl

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