Metamath Proof Explorer

Theorem mplcoe3

Description: Decompose a monomial in one variable into a power of a variable. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 18-Jul-2019)

Ref Expression
Hypotheses mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplcoe2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
mplcoe2.m ⊢ ↑ = ( .g ‘ 𝐺 )
mplcoe2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mplcoe3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplcoe3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
mplcoe3.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion mplcoe3 ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ↑ ( 𝑉 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3 mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplcoe2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
7 mplcoe2.m ⊢ ↑ = ( .g ‘ 𝐺 )
8 mplcoe2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
9 mplcoe3.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 mplcoe3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
11 mplcoe3.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 ifeq1 ⊢ ( 𝑥 = 0 → if ( 𝑘 = 𝑋 , 𝑥 , 0 ) = if ( 𝑘 = 𝑋 , 0 , 0 ) )
13 ifid ⊢ if ( 𝑘 = 𝑋 , 0 , 0 ) = 0
14 12 13 eqtrdi ⊢ ( 𝑥 = 0 → if ( 𝑘 = 𝑋 , 𝑥 , 0 ) = 0 )
15 14 mpteq2dv ⊢ ( 𝑥 = 0 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ 0 ) )
16 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑘 ∈ 𝐼 ↦ 0 )
17 15 16 eqtr4di ⊢ ( 𝑥 = 0 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) = ( 𝐼 × { 0 } ) )
18 17 eqeq2d ⊢ ( 𝑥 = 0 → ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) ↔ 𝑦 = ( 𝐼 × { 0 } ) ) )
19 18 ifbid ⊢ ( 𝑥 = 0 → if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
20 19 mpteq2dv ⊢ ( 𝑥 = 0 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
21 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) = ( 0 ↑ ( 𝑉 ‘ 𝑋 ) ) )
22 20 21 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 0 ↑ ( 𝑉 ‘ 𝑋 ) ) ) )
23 22 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 0 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ) )
24 ifeq1 ⊢ ( 𝑥 = 𝑛 → if ( 𝑘 = 𝑋 , 𝑥 , 0 ) = if ( 𝑘 = 𝑋 , 𝑛 , 0 ) )
25 24 mpteq2dv ⊢ ( 𝑥 = 𝑛 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) )
26 25 eqeq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) ↔ 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ) )
27 26 ifbid ⊢ ( 𝑥 = 𝑛 → if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) )
28 27 mpteq2dv ⊢ ( 𝑥 = 𝑛 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) )
29 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) )
30 28 29 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ) )
31 30 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ) )
32 ifeq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → if ( 𝑘 = 𝑋 , 𝑥 , 0 ) = if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) )
33 32 mpteq2dv ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) )
34 33 eqeq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) ↔ 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) ) )
35 34 ifbid ⊢ ( 𝑥 = ( 𝑛 + 1 ) → if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) )
36 35 mpteq2dv ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) )
37 oveq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) )
38 36 37 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) ) )
39 38 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) ) ) )
40 ifeq1 ⊢ ( 𝑥 = 𝑁 → if ( 𝑘 = 𝑋 , 𝑥 , 0 ) = if ( 𝑘 = 𝑋 , 𝑁 , 0 ) )
41 40 mpteq2dv ⊢ ( 𝑥 = 𝑁 → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) )
42 41 eqeq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) ↔ 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) ) )
43 42 ifbid ⊢ ( 𝑥 = 𝑁 → if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) )
44 43 mpteq2dv ⊢ ( 𝑥 = 𝑁 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) )
45 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑁 ↑ ( 𝑉 ‘ 𝑋 ) ) )
46 44 45 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ↑ ( 𝑉 ‘ 𝑋 ) ) ) )
47 46 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑥 , 0 ) ) , 1 , 0 ) ) = ( 𝑥 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ↑ ( 𝑉 ‘ 𝑋 ) ) ) ) )
48 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
49 1 8 48 5 9 10 mvrcl ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
50 6 48 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
51 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
52 6 51 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝐺 )
53 50 52 7 mulg0 ⊢ ( ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ ( 𝑉 ‘ 𝑋 ) ) = ( 1r ‘ 𝑃 ) )
54 49 53 syl ⊢ ( 𝜑 → ( 0 ↑ ( 𝑉 ‘ 𝑋 ) ) = ( 1r ‘ 𝑃 ) )
55 1 2 3 4 51 5 9 mpl1 ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
56 54 55 eqtr2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 0 ↑ ( 𝑉 ‘ 𝑋 ) ) )
57 oveq1 ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) = ( ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) )
58 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐼 ∈ 𝑊 )
59 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
60 2 snifpsrbag ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∈ 𝐷 )
61 5 60 sylan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∈ 𝐷 )
62 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
63 1nn0 ⊢ 1 ∈ ℕ0
64 63 a1i ⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℕ0 )
65 2 snifpsrbag ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 1 ∈ ℕ0 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ∈ 𝐷 )
66 5 64 65 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ∈ 𝐷 )
67 1 48 3 4 2 58 59 61 62 66 mplmonmul ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∘f + ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) , 1 , 0 ) ) )
68 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐼 )
69 8 2 3 4 58 59 68 mvrval ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑉 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) )
70 69 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) = ( 𝑉 ‘ 𝑋 ) )
71 70 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) )
72 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑛 ∈ ℕ0 )
73 0nn0 ⊢ 0 ∈ ℕ0
74 ifcl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ∈ ℕ0 )
75 72 73 74 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ 𝐼 ) → if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ∈ ℕ0 )
76 63 73 ifcli ⊢ if ( 𝑘 = 𝑋 , 1 , 0 ) ∈ ℕ0
77 76 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑘 ∈ 𝐼 ) → if ( 𝑘 = 𝑋 , 1 , 0 ) ∈ ℕ0 )
78 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) )
79 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) )
80 58 75 77 78 79 offval2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∘f + ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) )
81 iftrue ⊢ ( 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , 𝑛 , 0 ) = 𝑛 )
82 iftrue ⊢ ( 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , 1 , 0 ) = 1 )
83 81 82 oveq12d ⊢ ( 𝑘 = 𝑋 → ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) = ( 𝑛 + 1 ) )
84 iftrue ⊢ ( 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) = ( 𝑛 + 1 ) )
85 83 84 eqtr4d ⊢ ( 𝑘 = 𝑋 → ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) = if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) )
86 00id ⊢ ( 0 + 0 ) = 0
87 iffalse ⊢ ( ¬ 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , 𝑛 , 0 ) = 0 )
88 iffalse ⊢ ( ¬ 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , 1 , 0 ) = 0 )
89 87 88 oveq12d ⊢ ( ¬ 𝑘 = 𝑋 → ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) = ( 0 + 0 ) )
90 iffalse ⊢ ( ¬ 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) = 0 )
91 86 89 90 3eqtr4a ⊢ ( ¬ 𝑘 = 𝑋 → ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) = if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) )
92 85 91 pm2.61i ⊢ ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) = if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 )
93 92 mpteq2i ⊢ ( 𝑘 ∈ 𝐼 ↦ ( if ( 𝑘 = 𝑋 , 𝑛 , 0 ) + if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) )
94 80 93 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∘f + ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) )
95 94 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑦 = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∘f + ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) ↔ 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) ) )
96 95 ifbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑦 = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∘f + ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) )
97 96 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) ∘f + ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 1 , 0 ) ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) )
98 67 71 97 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) )
99 1 5 9 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
100 6 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
101 99 100 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
103 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
104 49 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
105 6 62 mgpplusg ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝐺 )
106 50 7 105 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ ( 𝑉 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) = ( ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) )
107 102 103 104 106 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) = ( ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) )
108 98 107 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) = ( ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ( .r ‘ 𝑃 ) ( 𝑉 ‘ 𝑋 ) ) ) )
109 57 108 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) ) )
110 109 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) ) ) )
111 110 a2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ↑ ( 𝑉 ‘ 𝑋 ) ) ) → ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ↑ ( 𝑉 ‘ 𝑋 ) ) ) ) )
112 23 31 39 47 56 111 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ↑ ( 𝑉 ‘ 𝑋 ) ) ) )
113 11 112 mpcom ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑘 ∈ 𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ↑ ( 𝑉 ‘ 𝑋 ) ) )