This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psdpw

Description: Power rule for partial derivative of power series. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses psdpw.s 
|- S = ( I mPwSer R )
psdpw.b 
|- B = ( Base ` S )
psdpw.g 
|- .x. = ( .g ` S )
psdpw.t 
|- .xb = ( .r ` S )
psdpw.m 
|- M = ( mulGrp ` S )
psdpw.e 
|- .^ = ( .g ` M )
psdpw.r 
|- ( ph -> R e. CRing )
psdpw.x 
|- ( ph -> X e. I )
psdpw.f 
|- ( ph -> F e. B )
psdpw.n 
|- ( ph -> N e. NN )
Assertion psdpw 
|- ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( N .^ F ) ) = ( ( N .x. ( ( N - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )

Proof

Step Hyp Ref Expression
1 psdpw.s 
 |-  S = ( I mPwSer R )
2 psdpw.b 
 |-  B = ( Base ` S )
3 psdpw.g 
 |-  .x. = ( .g ` S )
4 psdpw.t 
 |-  .xb = ( .r ` S )
5 psdpw.m 
 |-  M = ( mulGrp ` S )
6 psdpw.e 
 |-  .^ = ( .g ` M )
7 psdpw.r 
 |-  ( ph -> R e. CRing )
8 psdpw.x 
 |-  ( ph -> X e. I )
9 psdpw.f 
 |-  ( ph -> F e. B )
10 psdpw.n 
 |-  ( ph -> N e. NN )
11 fvoveq1 
 |-  ( n = 1 -> ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( ( I mPSDer R ) ` X ) ` ( 1 .^ F ) ) )
12 id 
 |-  ( n = 1 -> n = 1 )
13 oveq1 
 |-  ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
14 1m1e0 
 |-  ( 1 - 1 ) = 0
15 13 14 eqtrdi 
 |-  ( n = 1 -> ( n - 1 ) = 0 )
16 15 oveq1d 
 |-  ( n = 1 -> ( ( n - 1 ) .^ F ) = ( 0 .^ F ) )
17 12 16 oveq12d 
 |-  ( n = 1 -> ( n .x. ( ( n - 1 ) .^ F ) ) = ( 1 .x. ( 0 .^ F ) ) )
18 17 oveq1d 
 |-  ( n = 1 -> ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( 1 .x. ( 0 .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
19 11 18 eqeq12d 
 |-  ( n = 1 -> ( ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) <-> ( ( ( I mPSDer R ) ` X ) ` ( 1 .^ F ) ) = ( ( 1 .x. ( 0 .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
20 fvoveq1 
 |-  ( n = m -> ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) )
21 id 
 |-  ( n = m -> n = m )
22 oveq1 
 |-  ( n = m -> ( n - 1 ) = ( m - 1 ) )
23 22 oveq1d 
 |-  ( n = m -> ( ( n - 1 ) .^ F ) = ( ( m - 1 ) .^ F ) )
24 21 23 oveq12d 
 |-  ( n = m -> ( n .x. ( ( n - 1 ) .^ F ) ) = ( m .x. ( ( m - 1 ) .^ F ) ) )
25 24 oveq1d 
 |-  ( n = m -> ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
26 20 25 eqeq12d 
 |-  ( n = m -> ( ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) <-> ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
27 fvoveq1 
 |-  ( n = ( m + 1 ) -> ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( ( I mPSDer R ) ` X ) ` ( ( m + 1 ) .^ F ) ) )
28 id 
 |-  ( n = ( m + 1 ) -> n = ( m + 1 ) )
29 oveq1 
 |-  ( n = ( m + 1 ) -> ( n - 1 ) = ( ( m + 1 ) - 1 ) )
30 29 oveq1d 
 |-  ( n = ( m + 1 ) -> ( ( n - 1 ) .^ F ) = ( ( ( m + 1 ) - 1 ) .^ F ) )
31 28 30 oveq12d 
 |-  ( n = ( m + 1 ) -> ( n .x. ( ( n - 1 ) .^ F ) ) = ( ( m + 1 ) .x. ( ( ( m + 1 ) - 1 ) .^ F ) ) )
32 31 oveq1d 
 |-  ( n = ( m + 1 ) -> ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( m + 1 ) .x. ( ( ( m + 1 ) - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
33 27 32 eqeq12d 
 |-  ( n = ( m + 1 ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) <-> ( ( ( I mPSDer R ) ` X ) ` ( ( m + 1 ) .^ F ) ) = ( ( ( m + 1 ) .x. ( ( ( m + 1 ) - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
34 fvoveq1 
 |-  ( n = N -> ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( ( I mPSDer R ) ` X ) ` ( N .^ F ) ) )
35 id 
 |-  ( n = N -> n = N )
36 oveq1 
 |-  ( n = N -> ( n - 1 ) = ( N - 1 ) )
37 36 oveq1d 
 |-  ( n = N -> ( ( n - 1 ) .^ F ) = ( ( N - 1 ) .^ F ) )
38 35 37 oveq12d 
 |-  ( n = N -> ( n .x. ( ( n - 1 ) .^ F ) ) = ( N .x. ( ( N - 1 ) .^ F ) ) )
39 38 oveq1d 
 |-  ( n = N -> ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( N .x. ( ( N - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
40 34 39 eqeq12d 
 |-  ( n = N -> ( ( ( ( I mPSDer R ) ` X ) ` ( n .^ F ) ) = ( ( n .x. ( ( n - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) <-> ( ( ( I mPSDer R ) ` X ) ` ( N .^ F ) ) = ( ( N .x. ( ( N - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
41 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
42 reldmpsr 
 |-  Rel dom mPwSer
43 42 1 2 elbasov 
 |-  ( F e. B -> ( I e. _V /\ R e. _V ) )
44 9 43 syl 
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
45 44 simpld 
 |-  ( ph -> I e. _V )
46 1 45 7 psrcrng 
 |-  ( ph -> S e. CRing )
47 46 crngringd 
 |-  ( ph -> S e. Ring )
48 7 crnggrpd 
 |-  ( ph -> R e. Grp )
49 48 grpmgmd 
 |-  ( ph -> R e. Mgm )
50 1 2 49 8 9 psdcl 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
51 2 4 41 47 50 ringlidmd 
 |-  ( ph -> ( ( 1r ` S ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( I mPSDer R ) ` X ) ` F ) )
52 5 2 mgpbas 
 |-  B = ( Base ` M )
53 5 41 ringidval 
 |-  ( 1r ` S ) = ( 0g ` M )
54 52 53 6 mulg0 
 |-  ( F e. B -> ( 0 .^ F ) = ( 1r ` S ) )
55 9 54 syl 
 |-  ( ph -> ( 0 .^ F ) = ( 1r ` S ) )
56 55 oveq2d 
 |-  ( ph -> ( 1 .x. ( 0 .^ F ) ) = ( 1 .x. ( 1r ` S ) ) )
57 2 41 47 ringidcld 
 |-  ( ph -> ( 1r ` S ) e. B )
58 2 3 mulg1 
 |-  ( ( 1r ` S ) e. B -> ( 1 .x. ( 1r ` S ) ) = ( 1r ` S ) )
59 57 58 syl 
 |-  ( ph -> ( 1 .x. ( 1r ` S ) ) = ( 1r ` S ) )
60 56 59 eqtrd 
 |-  ( ph -> ( 1 .x. ( 0 .^ F ) ) = ( 1r ` S ) )
61 60 oveq1d 
 |-  ( ph -> ( ( 1 .x. ( 0 .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( 1r ` S ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
62 52 6 mulg1 
 |-  ( F e. B -> ( 1 .^ F ) = F )
63 9 62 syl 
 |-  ( ph -> ( 1 .^ F ) = F )
64 63 fveq2d 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( 1 .^ F ) ) = ( ( ( I mPSDer R ) ` X ) ` F ) )
65 51 61 64 3eqtr4rd 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( 1 .^ F ) ) = ( ( 1 .x. ( 0 .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
66 simpr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
67 66 oveq1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) .xb F ) = ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) .xb F ) )
68 46 adantr 
 |-  ( ( ph /\ m e. NN ) -> S e. CRing )
69 46 crnggrpd 
 |-  ( ph -> S e. Grp )
70 69 adantr 
 |-  ( ( ph /\ m e. NN ) -> S e. Grp )
71 simpr 
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
72 71 nnzd 
 |-  ( ( ph /\ m e. NN ) -> m e. ZZ )
73 47 adantr 
 |-  ( ( ph /\ m e. NN ) -> S e. Ring )
74 5 ringmgp 
 |-  ( S e. Ring -> M e. Mnd )
75 73 74 syl 
 |-  ( ( ph /\ m e. NN ) -> M e. Mnd )
76 nnm1nn0 
 |-  ( m e. NN -> ( m - 1 ) e. NN0 )
77 76 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( m - 1 ) e. NN0 )
78 9 adantr 
 |-  ( ( ph /\ m e. NN ) -> F e. B )
79 52 6 75 77 78 mulgnn0cld 
 |-  ( ( ph /\ m e. NN ) -> ( ( m - 1 ) .^ F ) e. B )
80 2 3 70 72 79 mulgcld 
 |-  ( ( ph /\ m e. NN ) -> ( m .x. ( ( m - 1 ) .^ F ) ) e. B )
81 50 adantr 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( I mPSDer R ) ` X ) ` F ) e. B )
82 2 4 68 80 81 78 crng32d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) .xb F ) = ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
83 82 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) .xb F ) = ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
84 2 3 4 mulgass2 
 |-  ( ( S e. Ring /\ ( m e. ZZ /\ ( ( m - 1 ) .^ F ) e. B /\ F e. B ) ) -> ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) = ( m .x. ( ( ( m - 1 ) .^ F ) .xb F ) ) )
85 73 72 79 78 84 syl13anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) = ( m .x. ( ( ( m - 1 ) .^ F ) .xb F ) ) )
86 5 4 mgpplusg 
 |-  .xb = ( +g ` M )
87 52 6 86 mulgnn0p1 
 |-  ( ( M e. Mnd /\ ( m - 1 ) e. NN0 /\ F e. B ) -> ( ( ( m - 1 ) + 1 ) .^ F ) = ( ( ( m - 1 ) .^ F ) .xb F ) )
88 75 77 78 87 syl3anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m - 1 ) + 1 ) .^ F ) = ( ( ( m - 1 ) .^ F ) .xb F ) )
89 71 nncnd 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
90 npcan1 
 |-  ( m e. CC -> ( ( m - 1 ) + 1 ) = m )
91 89 90 syl 
 |-  ( ( ph /\ m e. NN ) -> ( ( m - 1 ) + 1 ) = m )
92 91 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m - 1 ) + 1 ) .^ F ) = ( m .^ F ) )
93 88 92 eqtr3d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m - 1 ) .^ F ) .xb F ) = ( m .^ F ) )
94 93 oveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( m .x. ( ( ( m - 1 ) .^ F ) .xb F ) ) = ( m .x. ( m .^ F ) ) )
95 85 94 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) = ( m .x. ( m .^ F ) ) )
96 95 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
97 96 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
98 67 83 97 3eqtrd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) .xb F ) = ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
99 98 oveq1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) .xb F ) ( +g ` S ) ( ( m .^ F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) = ( ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ( +g ` S ) ( ( m .^ F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
100 eqid 
 |-  ( +g ` S ) = ( +g ` S )
101 7 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> R e. CRing )
102 8 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> X e. I )
103 47 74 syl 
 |-  ( ph -> M e. Mnd )
104 mndmgm 
 |-  ( M e. Mnd -> M e. Mgm )
105 103 104 syl 
 |-  ( ph -> M e. Mgm )
106 105 adantr 
 |-  ( ( ph /\ m e. NN ) -> M e. Mgm )
107 52 6 mulgnncl 
 |-  ( ( M e. Mgm /\ m e. NN /\ F e. B ) -> ( m .^ F ) e. B )
108 106 71 78 107 syl3anc 
 |-  ( ( ph /\ m e. NN ) -> ( m .^ F ) e. B )
109 108 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( m .^ F ) e. B )
110 9 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> F e. B )
111 1 2 100 4 101 102 109 110 psdmul 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( I mPSDer R ) ` X ) ` ( ( m .^ F ) .xb F ) ) = ( ( ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) .xb F ) ( +g ` S ) ( ( m .^ F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
112 2 3 100 mulgnnp1 
 |-  ( ( m e. NN /\ ( m .^ F ) e. B ) -> ( ( m + 1 ) .x. ( m .^ F ) ) = ( ( m .x. ( m .^ F ) ) ( +g ` S ) ( m .^ F ) ) )
113 71 108 112 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( m + 1 ) .x. ( m .^ F ) ) = ( ( m .x. ( m .^ F ) ) ( +g ` S ) ( m .^ F ) ) )
114 113 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m + 1 ) .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( m .x. ( m .^ F ) ) ( +g ` S ) ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
115 2 3 70 72 108 mulgcld 
 |-  ( ( ph /\ m e. NN ) -> ( m .x. ( m .^ F ) ) e. B )
116 2 100 4 73 115 108 81 ringdird 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m .x. ( m .^ F ) ) ( +g ` S ) ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ( +g ` S ) ( ( m .^ F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
117 114 116 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( m + 1 ) .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ( +g ` S ) ( ( m .^ F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
118 117 adantr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( m + 1 ) .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( m .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ( +g ` S ) ( ( m .^ F ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) )
119 99 111 118 3eqtr4d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( I mPSDer R ) ` X ) ` ( ( m .^ F ) .xb F ) ) = ( ( ( m + 1 ) .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
120 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> m e. NN )
121 52 6 86 mulgnnp1 
 |-  ( ( m e. NN /\ F e. B ) -> ( ( m + 1 ) .^ F ) = ( ( m .^ F ) .xb F ) )
122 120 110 121 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( m + 1 ) .^ F ) = ( ( m .^ F ) .xb F ) )
123 122 fveq2d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( I mPSDer R ) ` X ) ` ( ( m + 1 ) .^ F ) ) = ( ( ( I mPSDer R ) ` X ) ` ( ( m .^ F ) .xb F ) ) )
124 120 nncnd 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> m e. CC )
125 pncan1 
 |-  ( m e. CC -> ( ( m + 1 ) - 1 ) = m )
126 124 125 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( m + 1 ) - 1 ) = m )
127 126 oveq1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( m + 1 ) - 1 ) .^ F ) = ( m .^ F ) )
128 127 oveq2d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( m + 1 ) .x. ( ( ( m + 1 ) - 1 ) .^ F ) ) = ( ( m + 1 ) .x. ( m .^ F ) ) )
129 128 oveq1d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( m + 1 ) .x. ( ( ( m + 1 ) - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) = ( ( ( m + 1 ) .x. ( m .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
130 119 123 129 3eqtr4d 
 |-  ( ( ( ph /\ m e. NN ) /\ ( ( ( I mPSDer R ) ` X ) ` ( m .^ F ) ) = ( ( m .x. ( ( m - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) ) -> ( ( ( I mPSDer R ) ` X ) ` ( ( m + 1 ) .^ F ) ) = ( ( ( m + 1 ) .x. ( ( ( m + 1 ) - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
131 19 26 33 40 65 130 nnindd 
 |-  ( ( ph /\ N e. NN ) -> ( ( ( I mPSDer R ) ` X ) ` ( N .^ F ) ) = ( ( N .x. ( ( N - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )
132 10 131 mpdan 
 |-  ( ph -> ( ( ( I mPSDer R ) ` X ) ` ( N .^ F ) ) = ( ( N .x. ( ( N - 1 ) .^ F ) ) .xb ( ( ( I mPSDer R ) ` X ) ` F ) ) )