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