Metamath Proof Explorer

Theorem deg1pow

Description: Exact degree of a power of a polynomial in an integral domain. (Contributed by metakunt, 6-May-2025)

Ref Expression
Hypotheses deg1pow.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
deg1pow.2 ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
deg1pow.3 ⊢ ( 𝜑 → 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
deg1pow.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
deg1pow.5 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
deg1pow.6 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
Assertion deg1pow ( 𝜑 → ( 𝐷 ‘ ( 𝐴 ↑ 𝐹 ) ) = ( 𝐴 · ( 𝐷 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 deg1pow.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2 deg1pow.2 ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
3 deg1pow.3 ⊢ ( 𝜑 → 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
4 deg1pow.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
5 deg1pow.5 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
6 deg1pow.6 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
7 fvoveq1 ⊢ ( 𝑥 = 0 → ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝐷 ‘ ( 0 ↑ 𝐹 ) ) )
8 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) = ( 0 · ( 𝐷 ‘ 𝐹 ) ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 0 ↑ 𝐹 ) ) = ( 0 · ( 𝐷 ‘ 𝐹 ) ) ) )
10 fvoveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) )
11 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) )
13 fvoveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝐷 ‘ ( ( 𝑦 + 1 ) ↑ 𝐹 ) ) )
14 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( ( 𝑦 + 1 ) ↑ 𝐹 ) ) = ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) ) )
16 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝐷 ‘ ( 𝐴 ↑ 𝐹 ) ) )
17 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) = ( 𝐴 · ( 𝐷 ‘ 𝐹 ) ) )
18 16 17 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐷 ‘ ( 𝑥 ↑ 𝐹 ) ) = ( 𝑥 · ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐷 ‘ ( 𝐴 ↑ 𝐹 ) ) = ( 𝐴 · ( 𝐷 ‘ 𝐹 ) ) ) )
19 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) )
20 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
21 19 20 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
22 eqid ⊢ ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) = ( 1r ‘ ( Poly1 ‘ 𝑅 ) )
23 19 22 ringidval ⊢ ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
24 21 23 5 mulg0 ⊢ ( 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) → ( 0 ↑ 𝐹 ) = ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) )
25 2 24 syl ⊢ ( 𝜑 → ( 0 ↑ 𝐹 ) = ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) )
26 25 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0 ↑ 𝐹 ) ) = ( 𝐷 ‘ ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) ) )
27 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
28 27 simprbi ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
29 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
30 28 29 syl ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Ring )
31 1 30 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
32 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
33 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
34 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
35 32 33 34 22 ply1scl1 ⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) )
36 31 35 syl ⊢ ( 𝜑 → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) )
37 36 eqcomd ⊢ ( 𝜑 → ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 1r ‘ 𝑅 ) ) )
38 37 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) ) = ( 𝐷 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 1r ‘ 𝑅 ) ) ) )
39 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
40 39 34 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
41 31 40 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
42 1 28 syl ⊢ ( 𝜑 → 𝑅 ∈ Domn )
43 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
44 42 43 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
45 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
46 34 45 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
47 44 46 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
48 6 32 39 33 45 deg1scl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐷 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 1r ‘ 𝑅 ) ) ) = 0 )
49 31 41 47 48 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ ( 1r ‘ 𝑅 ) ) ) = 0 )
50 38 49 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ ( Poly1 ‘ 𝑅 ) ) ) = 0 )
51 26 50 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0 ↑ 𝐹 ) ) = 0 )
52 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
53 6 32 52 20 deg1nn0cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
54 31 2 3 53 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
55 54 nn0cnd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℂ )
56 55 mul02d ⊢ ( 𝜑 → ( 0 · ( 𝐷 ‘ 𝐹 ) ) = 0 )
57 56 eqcomd ⊢ ( 𝜑 → 0 = ( 0 · ( 𝐷 ‘ 𝐹 ) ) )
58 51 57 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0 ↑ 𝐹 ) ) = ( 0 · ( 𝐷 ‘ 𝐹 ) ) )
59 32 ply1idom ⊢ ( 𝑅 ∈ IDomn → ( Poly1 ‘ 𝑅 ) ∈ IDomn )
60 1 59 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) ∈ IDomn )
61 60 idomringd ⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) ∈ Ring )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( Poly1 ‘ 𝑅 ) ∈ Ring )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( Poly1 ‘ 𝑅 ) ∈ Ring )
64 19 ringmgp ⊢ ( ( Poly1 ‘ 𝑅 ) ∈ Ring → ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ∈ Mnd )
65 63 64 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ∈ Mnd )
66 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → 𝑦 ∈ ℕ0 )
67 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
68 eqid ⊢ ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) = ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
69 21 5 68 mulgnn0p1 ⊢ ( ( ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( 𝑦 + 1 ) ↑ 𝐹 ) = ( ( 𝑦 ↑ 𝐹 ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) 𝐹 ) )
70 65 66 67 69 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( 𝑦 + 1 ) ↑ 𝐹 ) = ( ( 𝑦 ↑ 𝐹 ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) 𝐹 ) )
71 70 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( ( 𝑦 + 1 ) ↑ 𝐹 ) ) = ( 𝐷 ‘ ( ( 𝑦 ↑ 𝐹 ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) 𝐹 ) ) )
72 eqid ⊢ ( .r ‘ ( Poly1 ‘ 𝑅 ) ) = ( .r ‘ ( Poly1 ‘ 𝑅 ) )
73 19 72 mgpplusg ⊢ ( .r ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
74 73 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) = ( .r ‘ ( Poly1 ‘ 𝑅 ) )
75 1 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝑅 ∈ Domn )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → 𝑅 ∈ Domn )
78 21 5 65 66 67 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝑦 ↑ 𝐹 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
79 60 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( Poly1 ‘ 𝑅 ) ∈ IDomn )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( Poly1 ‘ 𝑅 ) ∈ IDomn )
81 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
82 80 67 81 66 5 idomnnzpownz ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝑦 ↑ 𝐹 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
83 6 32 20 74 52 77 78 82 67 81 deg1mul ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( ( 𝑦 ↑ 𝐹 ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) 𝐹 ) ) = ( ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) + ( 𝐷 ‘ 𝐹 ) ) )
84 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) )
85 84 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) + ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) + ( 𝐷 ‘ 𝐹 ) ) )
86 66 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → 𝑦 ∈ ℂ )
87 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℂ )
88 86 87 adddirp1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) + ( 𝐷 ‘ 𝐹 ) ) )
89 88 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) + ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) )
90 85 89 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) + ( 𝐷 ‘ 𝐹 ) ) = ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) )
91 83 90 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( ( 𝑦 ↑ 𝐹 ) ( +g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) 𝐹 ) ) = ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) )
92 71 91 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝐷 ‘ ( 𝑦 ↑ 𝐹 ) ) = ( 𝑦 · ( 𝐷 ‘ 𝐹 ) ) ) → ( 𝐷 ‘ ( ( 𝑦 + 1 ) ↑ 𝐹 ) ) = ( ( 𝑦 + 1 ) · ( 𝐷 ‘ 𝐹 ) ) )
93 9 12 15 18 58 92 nn0indd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝐴 ↑ 𝐹 ) ) = ( 𝐴 · ( 𝐷 ‘ 𝐹 ) ) )
94 93 ex ⊢ ( 𝜑 → ( 𝐴 ∈ ℕ0 → ( 𝐷 ‘ ( 𝐴 ↑ 𝐹 ) ) = ( 𝐴 · ( 𝐷 ‘ 𝐹 ) ) ) )
95 4 94 mpd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐴 ↑ 𝐹 ) ) = ( 𝐴 · ( 𝐷 ‘ 𝐹 ) ) )