| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdadd.s | ⊢ 𝑆  =  ( 𝐼  mPwSer  𝑅 ) | 
						
							| 2 |  | psdadd.b | ⊢ 𝐵  =  ( Base ‘ 𝑆 ) | 
						
							| 3 |  | psdadd.p | ⊢  +   =  ( +g ‘ 𝑆 ) | 
						
							| 4 |  | psdadd.r | ⊢ ( 𝜑  →  𝑅  ∈  CMnd ) | 
						
							| 5 |  | psdadd.x | ⊢ ( 𝜑  →  𝑋  ∈  𝐼 ) | 
						
							| 6 |  | psdadd.f | ⊢ ( 𝜑  →  𝐹  ∈  𝐵 ) | 
						
							| 7 |  | psdadd.g | ⊢ ( 𝜑  →  𝐺  ∈  𝐵 ) | 
						
							| 8 |  | eqid | ⊢ { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  =  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } | 
						
							| 9 | 1 2 8 5 6 | psdval | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  =  ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 10 | 1 2 8 5 7 | psdval | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 )  =  ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 11 | 9 10 | oveq12d | ⊢ ( 𝜑  →  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∘f  ( +g ‘ 𝑅 ) ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) )  =  ( ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  ∘f  ( +g ‘ 𝑅 ) ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) ) | 
						
							| 12 |  | ovex | ⊢ ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  ∈  V | 
						
							| 13 |  | eqid | ⊢ ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 14 | 12 13 | fnmpti | ⊢ ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } | 
						
							| 15 | 14 | a1i | ⊢ ( 𝜑  →  ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 16 |  | ovex | ⊢ ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  ∈  V | 
						
							| 17 |  | eqid | ⊢ ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 18 | 16 17 | fnmpti | ⊢ ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } | 
						
							| 19 | 18 | a1i | ⊢ ( 𝜑  →  ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 20 |  | ovex | ⊢ ( ℕ0  ↑m  𝐼 )  ∈  V | 
						
							| 21 | 20 | rabex | ⊢ { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∈  V | 
						
							| 22 | 21 | a1i | ⊢ ( 𝜑  →  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∈  V ) | 
						
							| 23 |  | inidm | ⊢ ( { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∩  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  =  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } | 
						
							| 24 |  | fveq1 | ⊢ ( 𝑏  =  𝑑  →  ( 𝑏 ‘ 𝑋 )  =  ( 𝑑 ‘ 𝑋 ) ) | 
						
							| 25 | 24 | oveq1d | ⊢ ( 𝑏  =  𝑑  →  ( ( 𝑏 ‘ 𝑋 )  +  1 )  =  ( ( 𝑑 ‘ 𝑋 )  +  1 ) ) | 
						
							| 26 |  | fvoveq1 | ⊢ ( 𝑏  =  𝑑  →  ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) | 
						
							| 27 | 25 26 | oveq12d | ⊢ ( 𝑏  =  𝑑  →  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 28 |  | simpr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 29 |  | ovexd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  ∈  V ) | 
						
							| 30 | 13 27 28 29 | fvmptd3 | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ‘ 𝑑 )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 31 |  | fvoveq1 | ⊢ ( 𝑏  =  𝑑  →  ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) | 
						
							| 32 | 25 31 | oveq12d | ⊢ ( 𝑏  =  𝑑  →  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 33 |  | ovexd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  ∈  V ) | 
						
							| 34 | 17 32 28 33 | fvmptd3 | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ‘ 𝑑 )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 35 | 15 19 22 22 23 30 34 | offval | ⊢ ( 𝜑  →  ( ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  ∘f  ( +g ‘ 𝑅 ) ( 𝑏  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑏 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑏  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) )  =  ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) ) | 
						
							| 36 |  | eqid | ⊢ ( +g ‘ 𝑅 )  =  ( +g ‘ 𝑅 ) | 
						
							| 37 | 1 2 36 3 6 7 | psradd | ⊢ ( 𝜑  →  ( 𝐹  +  𝐺 )  =  ( 𝐹  ∘f  ( +g ‘ 𝑅 ) 𝐺 ) ) | 
						
							| 38 | 37 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐹  +  𝐺 )  =  ( 𝐹  ∘f  ( +g ‘ 𝑅 ) 𝐺 ) ) | 
						
							| 39 | 38 | fveq1d | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( ( 𝐹  ∘f  ( +g ‘ 𝑅 ) 𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) | 
						
							| 40 |  | reldmpsr | ⊢ Rel  dom   mPwSer | 
						
							| 41 | 1 2 40 | strov2rcl | ⊢ ( 𝐹  ∈  𝐵  →  𝐼  ∈  V ) | 
						
							| 42 | 6 41 | syl | ⊢ ( 𝜑  →  𝐼  ∈  V ) | 
						
							| 43 | 8 | psrbagsn | ⊢ ( 𝐼  ∈  V  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 44 | 42 43 | syl | ⊢ ( 𝜑  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 45 | 44 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 46 | 8 | psrbagaddcl | ⊢ ( ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∧  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 47 | 28 45 46 | syl2anc | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 48 |  | eqid | ⊢ ( Base ‘ 𝑅 )  =  ( Base ‘ 𝑅 ) | 
						
							| 49 | 1 48 8 2 6 | psrelbas | ⊢ ( 𝜑  →  𝐹 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 50 | 49 | ffnd | ⊢ ( 𝜑  →  𝐹  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 51 | 1 48 8 2 7 | psrelbas | ⊢ ( 𝜑  →  𝐺 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 52 | 51 | ffnd | ⊢ ( 𝜑  →  𝐺  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 53 |  | eqidd | ⊢ ( ( 𝜑  ∧  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) | 
						
							| 54 |  | eqidd | ⊢ ( ( 𝜑  ∧  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) | 
						
							| 55 | 50 52 22 22 23 53 54 | ofval | ⊢ ( ( 𝜑  ∧  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝐹  ∘f  ( +g ‘ 𝑅 ) 𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 56 | 47 55 | syldan | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝐹  ∘f  ( +g ‘ 𝑅 ) 𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 57 | 39 56 | eqtrd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 58 | 57 | oveq2d | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 59 | 4 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑅  ∈  CMnd ) | 
						
							| 60 | 8 | psrbagf | ⊢ ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  →  𝑑 : 𝐼 ⟶ ℕ0 ) | 
						
							| 61 | 60 | adantl | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑑 : 𝐼 ⟶ ℕ0 ) | 
						
							| 62 | 5 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑋  ∈  𝐼 ) | 
						
							| 63 | 61 62 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑑 ‘ 𝑋 )  ∈  ℕ0 ) | 
						
							| 64 |  | peano2nn0 | ⊢ ( ( 𝑑 ‘ 𝑋 )  ∈  ℕ0  →  ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℕ0 ) | 
						
							| 65 | 63 64 | syl | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℕ0 ) | 
						
							| 66 | 6 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐹  ∈  𝐵 ) | 
						
							| 67 | 1 48 8 2 66 | psrelbas | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐹 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 68 | 67 47 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  ( Base ‘ 𝑅 ) ) | 
						
							| 69 | 51 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐺 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 70 | 69 47 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  ( Base ‘ 𝑅 ) ) | 
						
							| 71 |  | eqid | ⊢ ( .g ‘ 𝑅 )  =  ( .g ‘ 𝑅 ) | 
						
							| 72 | 48 71 36 | mulgnn0di | ⊢ ( ( 𝑅  ∈  CMnd  ∧  ( ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℕ0  ∧  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  ( Base ‘ 𝑅 )  ∧  ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  ( Base ‘ 𝑅 ) ) )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 73 | 59 65 68 70 72 | syl13anc | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ( +g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 74 | 58 73 | eqtr2d | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 75 | 74 | mpteq2dva | ⊢ ( 𝜑  →  ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ( +g ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐺 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) )  =  ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 76 | 11 35 75 | 3eqtrd | ⊢ ( 𝜑  →  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∘f  ( +g ‘ 𝑅 ) ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) )  =  ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 77 | 4 | cmnmndd | ⊢ ( 𝜑  →  𝑅  ∈  Mnd ) | 
						
							| 78 |  | mndmgm | ⊢ ( 𝑅  ∈  Mnd  →  𝑅  ∈  Mgm ) | 
						
							| 79 | 77 78 | syl | ⊢ ( 𝜑  →  𝑅  ∈  Mgm ) | 
						
							| 80 | 1 2 79 5 6 | psdcl | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∈  𝐵 ) | 
						
							| 81 | 1 2 79 5 7 | psdcl | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 )  ∈  𝐵 ) | 
						
							| 82 | 1 2 36 3 80 81 | psradd | ⊢ ( 𝜑  →  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  +  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) )  =  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∘f  ( +g ‘ 𝑅 ) ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) ) | 
						
							| 83 | 1 2 3 79 6 7 | psraddcl | ⊢ ( 𝜑  →  ( 𝐹  +  𝐺 )  ∈  𝐵 ) | 
						
							| 84 | 1 2 8 5 83 | psdval | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐹  +  𝐺 ) )  =  ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ↦  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐹  +  𝐺 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 85 | 76 82 84 | 3eqtr4rd | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐹  +  𝐺 ) )  =  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  +  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐺 ) ) ) |