Metamath Proof Explorer


Theorem psdmplcl

Description: The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025)

Ref Expression
Hypotheses psdmplcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
psdmplcl.b 𝐵 = ( Base ‘ 𝑃 )
psdmplcl.r ( 𝜑𝑅 ∈ Mnd )
psdmplcl.x ( 𝜑𝑋𝐼 )
psdmplcl.f ( 𝜑𝐹𝐵 )
Assertion psdmplcl ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psdmplcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
2 psdmplcl.b 𝐵 = ( Base ‘ 𝑃 )
3 psdmplcl.r ( 𝜑𝑅 ∈ Mnd )
4 psdmplcl.x ( 𝜑𝑋𝐼 )
5 psdmplcl.f ( 𝜑𝐹𝐵 )
6 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
7 eqid ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
8 mndmgm ( 𝑅 ∈ Mnd → 𝑅 ∈ Mgm )
9 3 8 syl ( 𝜑𝑅 ∈ Mgm )
10 1 6 2 7 mplbasss 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
11 10 5 sselid ( 𝜑𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
12 6 7 9 4 11 psdcl ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
13 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
14 6 7 13 4 11 psdval ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) = ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
15 ovex ( ℕ0m 𝐼 ) ∈ V
16 15 rabex { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V
17 16 a1i ( 𝜑 → { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V )
18 17 mptexd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) ∈ V )
19 fvexd ( 𝜑 → ( 0g𝑅 ) ∈ V )
20 funmpt Fun ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
21 20 a1i ( 𝜑 → Fun ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) )
22 simpr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
23 reldmmpl Rel dom mPoly
24 1 2 23 strov2rcl ( 𝐹𝐵𝐼 ∈ V )
25 5 24 syl ( 𝜑𝐼 ∈ V )
26 13 psrbagsn ( 𝐼 ∈ V → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
27 25 26 syl ( 𝜑 → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
28 27 adantr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
29 13 psrbagaddcl ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
30 22 28 29 syl2anc ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
31 eqidd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
32 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33 1 32 2 13 5 mplelf ( 𝜑𝐹 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
34 33 feqmptd ( 𝜑𝐹 = ( 𝑧 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹𝑧 ) ) )
35 fveq2 ( 𝑧 = ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) → ( 𝐹𝑧 ) = ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
36 30 31 34 35 fmptco ( 𝜑 → ( 𝐹 ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) )
37 eqid ( 0g𝑅 ) = ( 0g𝑅 )
38 1 2 37 5 mplelsfi ( 𝜑𝐹 finSupp ( 0g𝑅 ) )
39 30 fmpttd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
40 ovex ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ V
41 eqid ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
42 40 41 fnmpti ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
43 42 a1i ( 𝜑 → ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
44 dffn3 ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↔ ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ran ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
45 43 44 sylib ( 𝜑 → ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ran ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
46 45 39 fcod ( 𝜑 → ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ran ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
47 46 ffnd ( 𝜑 → ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
48 fnresi ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
49 48 a1i ( 𝜑 → ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) Fn { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
50 13 psrbagf ( 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → 𝑑 : 𝐼 ⟶ ℕ0 )
51 50 adantl ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑑 : 𝐼 ⟶ ℕ0 )
52 51 ffvelcdmda ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → ( 𝑑𝑖 ) ∈ ℕ0 )
53 52 nn0cnd ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → ( 𝑑𝑖 ) ∈ ℂ )
54 ax-1cn 1 ∈ ℂ
55 0cn 0 ∈ ℂ
56 54 55 ifcli if ( 𝑖 = 𝑋 , 1 , 0 ) ∈ ℂ
57 56 a1i ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → if ( 𝑖 = 𝑋 , 1 , 0 ) ∈ ℂ )
58 53 57 pncand ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → ( ( ( 𝑑𝑖 ) + if ( 𝑖 = 𝑋 , 1 , 0 ) ) − if ( 𝑖 = 𝑋 , 1 , 0 ) ) = ( 𝑑𝑖 ) )
59 58 mpteq2dva ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑖𝐼 ↦ ( ( ( 𝑑𝑖 ) + if ( 𝑖 = 𝑋 , 1 , 0 ) ) − if ( 𝑖 = 𝑋 , 1 , 0 ) ) ) = ( 𝑖𝐼 ↦ ( 𝑑𝑖 ) ) )
60 simpr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
61 27 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
62 13 psrbagaddcl ( ( 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∧ ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
63 60 61 62 syl2anc ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
64 13 psrbagf ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) : 𝐼 ⟶ ℕ0 )
65 64 ffnd ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) Fn 𝐼 )
66 63 65 syl ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) Fn 𝐼 )
67 1ex 1 ∈ V
68 c0ex 0 ∈ V
69 67 68 ifex if ( 𝑦 = 𝑋 , 1 , 0 ) ∈ V
70 eqid ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) )
71 69 70 fnmpti ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) Fn 𝐼
72 71 a1i ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) Fn 𝐼 )
73 25 adantr ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝐼 ∈ V )
74 inidm ( 𝐼𝐼 ) = 𝐼
75 50 ffnd ( 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → 𝑑 Fn 𝐼 )
76 75 adantl ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑑 Fn 𝐼 )
77 eqidd ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → ( 𝑑𝑖 ) = ( 𝑑𝑖 ) )
78 eqeq1 ( 𝑦 = 𝑖 → ( 𝑦 = 𝑋𝑖 = 𝑋 ) )
79 78 ifbid ( 𝑦 = 𝑖 → if ( 𝑦 = 𝑋 , 1 , 0 ) = if ( 𝑖 = 𝑋 , 1 , 0 ) )
80 simpr ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → 𝑖𝐼 )
81 67 68 ifex if ( 𝑖 = 𝑋 , 1 , 0 ) ∈ V
82 81 a1i ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → if ( 𝑖 = 𝑋 , 1 , 0 ) ∈ V )
83 70 79 80 82 fvmptd3 ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → ( ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑖 ) = if ( 𝑖 = 𝑋 , 1 , 0 ) )
84 76 72 73 73 74 77 83 ofval ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑖𝐼 ) → ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ‘ 𝑖 ) = ( ( 𝑑𝑖 ) + if ( 𝑖 = 𝑋 , 1 , 0 ) ) )
85 66 72 73 73 74 84 83 offval ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∘f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = ( 𝑖𝐼 ↦ ( ( ( 𝑑𝑖 ) + if ( 𝑖 = 𝑋 , 1 , 0 ) ) − if ( 𝑖 = 𝑋 , 1 , 0 ) ) ) )
86 51 feqmptd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑑 = ( 𝑖𝐼 ↦ ( 𝑑𝑖 ) ) )
87 59 85 86 3eqtr4d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∘f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = 𝑑 )
88 30 adantlr ( ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ∧ 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
89 88 fmpttd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
90 89 60 fvco3d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ‘ 𝑑 ) = ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ 𝑑 ) ) )
91 eqid ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
92 oveq1 ( 𝑘 = 𝑑 → ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
93 ovexd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ V )
94 91 92 60 93 fvmptd3 ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ 𝑑 ) = ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
95 94 fveq2d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ 𝑑 ) ) = ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) )
96 oveq1 ( 𝑏 = ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) → ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∘f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
97 ovexd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∘f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∈ V )
98 41 96 63 97 fvmptd3 ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ‘ ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) = ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∘f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
99 90 95 98 3eqtrd ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ‘ 𝑑 ) = ( ( 𝑑f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ∘f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
100 fvresi ( 𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → ( ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ‘ 𝑑 ) = 𝑑 )
101 100 adantl ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ‘ 𝑑 ) = 𝑑 )
102 87 99 101 3eqtr4d ( ( 𝜑𝑑 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ‘ 𝑑 ) = ( ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ‘ 𝑑 ) )
103 47 49 102 eqfnfvd ( 𝜑 → ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
104 fcof1 ( ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∧ ( ( 𝑏 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑏f − ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) = ( I ↾ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ) → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } –1-1→ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
105 39 103 104 syl2anc ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } –1-1→ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } )
106 38 105 19 5 fsuppco ( 𝜑 → ( 𝐹 ∘ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) finSupp ( 0g𝑅 ) )
107 36 106 eqbrtrrd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) finSupp ( 0g𝑅 ) )
108 107 fsuppimpd ( 𝜑 → ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) supp ( 0g𝑅 ) ) ∈ Fin )
109 ssidd ( 𝜑 → ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) supp ( 0g𝑅 ) ) ⊆ ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) supp ( 0g𝑅 ) ) )
110 eqid ( .g𝑅 ) = ( .g𝑅 )
111 32 110 37 mulgnn0z ( ( 𝑅 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ( .g𝑅 ) ( 0g𝑅 ) ) = ( 0g𝑅 ) )
112 3 111 sylan ( ( 𝜑𝑛 ∈ ℕ0 ) → ( 𝑛 ( .g𝑅 ) ( 0g𝑅 ) ) = ( 0g𝑅 ) )
113 13 psrbagf ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } → 𝑘 : 𝐼 ⟶ ℕ0 )
114 113 adantl ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
115 4 adantr ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → 𝑋𝐼 )
116 114 115 ffvelcdmd ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝑘𝑋 ) ∈ ℕ0 )
117 peano2nn0 ( ( 𝑘𝑋 ) ∈ ℕ0 → ( ( 𝑘𝑋 ) + 1 ) ∈ ℕ0 )
118 116 117 syl ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( ( 𝑘𝑋 ) + 1 ) ∈ ℕ0 )
119 fvexd ( ( 𝜑𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ∈ V )
120 109 112 118 119 19 suppssov2 ( 𝜑 → ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) supp ( 0g𝑅 ) ) ⊆ ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) supp ( 0g𝑅 ) ) )
121 108 120 ssfid ( 𝜑 → ( ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) supp ( 0g𝑅 ) ) ∈ Fin )
122 18 19 21 121 isfsuppd ( 𝜑 → ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( ( ( 𝑘𝑋 ) + 1 ) ( .g𝑅 ) ( 𝐹 ‘ ( 𝑘f + ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) ) ) ) finSupp ( 0g𝑅 ) )
123 14 122 eqbrtrd ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) finSupp ( 0g𝑅 ) )
124 1 6 7 37 2 mplelbas ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 ↔ ( ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) finSupp ( 0g𝑅 ) ) )
125 12 123 124 sylanbrc ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ∈ 𝐵 )