| Step | Hyp | Ref | Expression | 
						
							| 1 |  | psdvsca.s | ⊢ 𝑆  =  ( 𝐼  mPwSer  𝑅 ) | 
						
							| 2 |  | psdvsca.b | ⊢ 𝐵  =  ( Base ‘ 𝑆 ) | 
						
							| 3 |  | psdvsca.m | ⊢  ·   =  (  ·𝑠  ‘ 𝑆 ) | 
						
							| 4 |  | psdvsca.k | ⊢ 𝐾  =  ( Base ‘ 𝑅 ) | 
						
							| 5 |  | psdvsca.r | ⊢ ( 𝜑  →  𝑅  ∈  CRing ) | 
						
							| 6 |  | psdvsca.x | ⊢ ( 𝜑  →  𝑋  ∈  𝐼 ) | 
						
							| 7 |  | psdvsca.f | ⊢ ( 𝜑  →  𝐹  ∈  𝐵 ) | 
						
							| 8 |  | psdvsca.c | ⊢ ( 𝜑  →  𝐶  ∈  𝐾 ) | 
						
							| 9 |  | eqid | ⊢ ( Base ‘ 𝑅 )  =  ( Base ‘ 𝑅 ) | 
						
							| 10 |  | eqid | ⊢ { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  =  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } | 
						
							| 11 | 5 | crngringd | ⊢ ( 𝜑  →  𝑅  ∈  Ring ) | 
						
							| 12 |  | ringmgm | ⊢ ( 𝑅  ∈  Ring  →  𝑅  ∈  Mgm ) | 
						
							| 13 | 11 12 | syl | ⊢ ( 𝜑  →  𝑅  ∈  Mgm ) | 
						
							| 14 | 1 3 4 2 11 8 7 | psrvscacl | ⊢ ( 𝜑  →  ( 𝐶  ·  𝐹 )  ∈  𝐵 ) | 
						
							| 15 | 1 2 13 6 14 | psdcl | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶  ·  𝐹 ) )  ∈  𝐵 ) | 
						
							| 16 | 1 9 10 2 15 | psrelbas | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶  ·  𝐹 ) ) : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 17 | 16 | ffnd | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶  ·  𝐹 ) )  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 18 | 1 2 13 6 7 | psdcl | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∈  𝐵 ) | 
						
							| 19 | 1 3 4 2 11 8 18 | psrvscacl | ⊢ ( 𝜑  →  ( 𝐶  ·  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) )  ∈  𝐵 ) | 
						
							| 20 | 1 9 10 2 19 | psrelbas | ⊢ ( 𝜑  →  ( 𝐶  ·  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ ( Base ‘ 𝑅 ) ) | 
						
							| 21 | 20 | ffnd | ⊢ ( 𝜑  →  ( 𝐶  ·  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) )  Fn  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 22 | 11 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑅  ∈  Ring ) | 
						
							| 23 | 10 | psrbagf | ⊢ ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  →  𝑑 : 𝐼 ⟶ ℕ0 ) | 
						
							| 24 | 23 | adantl | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑑 : 𝐼 ⟶ ℕ0 ) | 
						
							| 25 | 6 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑋  ∈  𝐼 ) | 
						
							| 26 | 24 25 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑑 ‘ 𝑋 )  ∈  ℕ0 ) | 
						
							| 27 |  | peano2nn0 | ⊢ ( ( 𝑑 ‘ 𝑋 )  ∈  ℕ0  →  ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℕ0 ) | 
						
							| 28 | 27 | nn0zd | ⊢ ( ( 𝑑 ‘ 𝑋 )  ∈  ℕ0  →  ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℤ ) | 
						
							| 29 | 26 28 | syl | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℤ ) | 
						
							| 30 | 8 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐶  ∈  𝐾 ) | 
						
							| 31 | 1 4 10 2 7 | psrelbas | ⊢ ( 𝜑  →  𝐹 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ 𝐾 ) | 
						
							| 32 | 31 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐹 : { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ⟶ 𝐾 ) | 
						
							| 33 |  | simpr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 34 |  | reldmpsr | ⊢ Rel  dom   mPwSer | 
						
							| 35 | 1 2 34 | strov2rcl | ⊢ ( 𝐹  ∈  𝐵  →  𝐼  ∈  V ) | 
						
							| 36 | 7 35 | syl | ⊢ ( 𝜑  →  𝐼  ∈  V ) | 
						
							| 37 | 10 | psrbagsn | ⊢ ( 𝐼  ∈  V  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 38 | 36 37 | syl | ⊢ ( 𝜑  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 39 | 38 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 40 | 10 | psrbagaddcl | ⊢ ( ( 𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin }  ∧  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 41 | 33 39 40 | syl2anc | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) )  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } ) | 
						
							| 42 | 32 41 | ffvelcdmd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  𝐾 ) | 
						
							| 43 |  | eqid | ⊢ ( .g ‘ 𝑅 )  =  ( .g ‘ 𝑅 ) | 
						
							| 44 |  | eqid | ⊢ ( .r ‘ 𝑅 )  =  ( .r ‘ 𝑅 ) | 
						
							| 45 | 4 43 44 | mulgass3 | ⊢ ( ( 𝑅  ∈  Ring  ∧  ( ( ( 𝑑 ‘ 𝑋 )  +  1 )  ∈  ℤ  ∧  𝐶  ∈  𝐾  ∧  ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  ∈  𝐾 ) )  →  ( 𝐶 ( .r ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 46 | 22 29 30 42 45 | syl13anc | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐶 ( .r ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 47 | 7 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  𝐹  ∈  𝐵 ) | 
						
							| 48 | 1 2 10 25 47 33 | psdcoef | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 49 | 48 | oveq2d | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐶 ( .r ‘ 𝑅 ) ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) )  =  ( 𝐶 ( .r ‘ 𝑅 ) ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 50 | 1 3 4 2 44 10 30 47 41 | psrvscaval | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝐶  ·  𝐹 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) )  =  ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 51 | 50 | oveq2d | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐶  ·  𝐹 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) ) | 
						
							| 52 | 46 49 51 | 3eqtr4rd | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐶  ·  𝐹 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) )  =  ( 𝐶 ( .r ‘ 𝑅 ) ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) ) ) | 
						
							| 53 | 14 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( 𝐶  ·  𝐹 )  ∈  𝐵 ) | 
						
							| 54 | 1 2 10 25 53 33 | psdcoef | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶  ·  𝐹 ) ) ‘ 𝑑 )  =  ( ( ( 𝑑 ‘ 𝑋 )  +  1 ) ( .g ‘ 𝑅 ) ( ( 𝐶  ·  𝐹 ) ‘ ( 𝑑  ∘f   +  ( 𝑦  ∈  𝐼  ↦  if ( 𝑦  =  𝑋 ,  1 ,  0 ) ) ) ) ) ) | 
						
							| 55 | 18 | adantr | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 )  ∈  𝐵 ) | 
						
							| 56 | 1 3 4 2 44 10 30 55 33 | psrvscaval | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( 𝐶  ·  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) ‘ 𝑑 )  =  ( 𝐶 ( .r ‘ 𝑅 ) ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ‘ 𝑑 ) ) ) | 
						
							| 57 | 52 54 56 | 3eqtr4d | ⊢ ( ( 𝜑  ∧  𝑑  ∈  { ℎ  ∈  ( ℕ0  ↑m  𝐼 )  ∣  ( ◡ ℎ  “  ℕ )  ∈  Fin } )  →  ( ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶  ·  𝐹 ) ) ‘ 𝑑 )  =  ( ( 𝐶  ·  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) ‘ 𝑑 ) ) | 
						
							| 58 | 17 21 57 | eqfnfvd | ⊢ ( 𝜑  →  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ ( 𝐶  ·  𝐹 ) )  =  ( 𝐶  ·  ( ( ( 𝐼  mPSDer  𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) ) |