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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 mplring ( ( 𝐼𝑊𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
100 5 9 99 syl2anc ( 𝜑𝑃 ∈ Ring )
101 6 ringmgp ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
102 100 101 syl ( 𝜑𝐺 ∈ Mnd )
103 102 adantr ( ( 𝜑𝑛 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
104 simpr ( ( 𝜑𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
105 49 adantr ( ( 𝜑𝑛 ∈ ℕ0 ) → ( 𝑉𝑋 ) ∈ ( Base ‘ 𝑃 ) )
106 6 62 mgpplusg ( .r𝑃 ) = ( +g𝐺 )
107 50 7 106 mulgnn0p1 ( ( 𝐺 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ ( 𝑉𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑛 + 1 ) ( 𝑉𝑋 ) ) = ( ( 𝑛 ( 𝑉𝑋 ) ) ( .r𝑃 ) ( 𝑉𝑋 ) ) )
108 103 104 105 107 syl3anc ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ( 𝑉𝑋 ) ) = ( ( 𝑛 ( 𝑉𝑋 ) ) ( .r𝑃 ) ( 𝑉𝑋 ) ) )
109 98 108 eqeq12d ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ( 𝑉𝑋 ) ) ↔ ( ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) ( .r𝑃 ) ( 𝑉𝑋 ) ) = ( ( 𝑛 ( 𝑉𝑋 ) ) ( .r𝑃 ) ( 𝑉𝑋 ) ) ) )
110 57 109 syl5ibr ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ( 𝑉𝑋 ) ) → ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ( 𝑉𝑋 ) ) ) )
111 110 expcom ( 𝑛 ∈ ℕ0 → ( 𝜑 → ( ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ( 𝑉𝑋 ) ) → ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ( 𝑉𝑋 ) ) ) ) )
112 111 a2d ( 𝑛 ∈ ℕ0 → ( ( 𝜑 → ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑛 , 0 ) ) , 1 , 0 ) ) = ( 𝑛 ( 𝑉𝑋 ) ) ) → ( 𝜑 → ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , ( 𝑛 + 1 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑛 + 1 ) ( 𝑉𝑋 ) ) ) ) )
113 23 31 39 47 56 112 nn0ind ( 𝑁 ∈ ℕ0 → ( 𝜑 → ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ( 𝑉𝑋 ) ) ) )
114 11 113 mpcom ( 𝜑 → ( 𝑦𝐷 ↦ if ( 𝑦 = ( 𝑘𝐼 ↦ if ( 𝑘 = 𝑋 , 𝑁 , 0 ) ) , 1 , 0 ) ) = ( 𝑁 ( 𝑉𝑋 ) ) )