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 ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psdpw.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psdpw.g ⊢ · = ( .g ‘ 𝑆 )
psdpw.t ⊢ ∙ = ( .r ‘ 𝑆 )
psdpw.m ⊢ 𝑀 = ( mulGrp ‘ 𝑆 )
psdpw.e ⊢ ↑ = ( .g ‘ 𝑀 )
psdpw.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
psdpw.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
psdpw.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
psdpw.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion psdpw ( 𝜑 → ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ ( 𝑁 ↑ 𝐹 ) ) = ( ( 𝑁 · ( ( 𝑁 − 1 ) ↑ 𝐹 ) ) ∙ ( ( ( 𝐼 mPSDer 𝑅 ) ‘ 𝑋 ) ‘ 𝐹 ) ) )

Proof

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