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 
|- P = ( I mPoly R )
mplcoe1.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplcoe1.z 
|- .0. = ( 0g ` R )
mplcoe1.o 
|- .1. = ( 1r ` R )
mplcoe1.i 
|- ( ph -> I e. W )
mplcoe2.g 
|- G = ( mulGrp ` P )
mplcoe2.m 
|- .^ = ( .g ` G )
mplcoe2.v 
|- V = ( I mVar R )
mplcoe3.r 
|- ( ph -> R e. Ring )
mplcoe3.x 
|- ( ph -> X e. I )
mplcoe3.n 
|- ( ph -> N e. NN0 )
Assertion mplcoe3 
|- ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) ) = ( N .^ ( V ` X ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p 
 |-  P = ( I mPoly R )
2 mplcoe1.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplcoe1.z 
 |-  .0. = ( 0g ` R )
4 mplcoe1.o 
 |-  .1. = ( 1r ` R )
5 mplcoe1.i 
 |-  ( ph -> I e. W )
6 mplcoe2.g 
 |-  G = ( mulGrp ` P )
7 mplcoe2.m 
 |-  .^ = ( .g ` G )
8 mplcoe2.v 
 |-  V = ( I mVar R )
9 mplcoe3.r 
 |-  ( ph -> R e. Ring )
10 mplcoe3.x 
 |-  ( ph -> X e. I )
11 mplcoe3.n 
 |-  ( ph -> N e. NN0 )
12 ifeq1 
 |-  ( x = 0 -> if ( k = X , x , 0 ) = if ( k = X , 0 , 0 ) )
13 ifid 
 |-  if ( k = X , 0 , 0 ) = 0
14 12 13 eqtrdi 
 |-  ( x = 0 -> if ( k = X , x , 0 ) = 0 )
15 14 mpteq2dv 
 |-  ( x = 0 -> ( k e. I |-> if ( k = X , x , 0 ) ) = ( k e. I |-> 0 ) )
16 fconstmpt 
 |-  ( I X. { 0 } ) = ( k e. I |-> 0 )
17 15 16 eqtr4di 
 |-  ( x = 0 -> ( k e. I |-> if ( k = X , x , 0 ) ) = ( I X. { 0 } ) )
18 17 eqeq2d 
 |-  ( x = 0 -> ( y = ( k e. I |-> if ( k = X , x , 0 ) ) <-> y = ( I X. { 0 } ) ) )
19 18 ifbid 
 |-  ( x = 0 -> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) = if ( y = ( I X. { 0 } ) , .1. , .0. ) )
20 19 mpteq2dv 
 |-  ( x = 0 -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) )
21 oveq1 
 |-  ( x = 0 -> ( x .^ ( V ` X ) ) = ( 0 .^ ( V ` X ) ) )
22 20 21 eqeq12d 
 |-  ( x = 0 -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) <-> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 0 .^ ( V ` X ) ) ) )
23 22 imbi2d 
 |-  ( x = 0 -> ( ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) ) <-> ( ph -> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 0 .^ ( V ` X ) ) ) ) )
24 ifeq1 
 |-  ( x = n -> if ( k = X , x , 0 ) = if ( k = X , n , 0 ) )
25 24 mpteq2dv 
 |-  ( x = n -> ( k e. I |-> if ( k = X , x , 0 ) ) = ( k e. I |-> if ( k = X , n , 0 ) ) )
26 25 eqeq2d 
 |-  ( x = n -> ( y = ( k e. I |-> if ( k = X , x , 0 ) ) <-> y = ( k e. I |-> if ( k = X , n , 0 ) ) ) )
27 26 ifbid 
 |-  ( x = n -> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) = if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) )
28 27 mpteq2dv 
 |-  ( x = n -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) )
29 oveq1 
 |-  ( x = n -> ( x .^ ( V ` X ) ) = ( n .^ ( V ` X ) ) )
30 28 29 eqeq12d 
 |-  ( x = n -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) <-> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) = ( n .^ ( V ` X ) ) ) )
31 30 imbi2d 
 |-  ( x = n -> ( ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) ) <-> ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) = ( n .^ ( V ` X ) ) ) ) )
32 ifeq1 
 |-  ( x = ( n + 1 ) -> if ( k = X , x , 0 ) = if ( k = X , ( n + 1 ) , 0 ) )
33 32 mpteq2dv 
 |-  ( x = ( n + 1 ) -> ( k e. I |-> if ( k = X , x , 0 ) ) = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) )
34 33 eqeq2d 
 |-  ( x = ( n + 1 ) -> ( y = ( k e. I |-> if ( k = X , x , 0 ) ) <-> y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) ) )
35 34 ifbid 
 |-  ( x = ( n + 1 ) -> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) = if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) )
36 35 mpteq2dv 
 |-  ( x = ( n + 1 ) -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) )
37 oveq1 
 |-  ( x = ( n + 1 ) -> ( x .^ ( V ` X ) ) = ( ( n + 1 ) .^ ( V ` X ) ) )
38 36 37 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) <-> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( n + 1 ) .^ ( V ` X ) ) ) )
39 38 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) ) <-> ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( n + 1 ) .^ ( V ` X ) ) ) ) )
40 ifeq1 
 |-  ( x = N -> if ( k = X , x , 0 ) = if ( k = X , N , 0 ) )
41 40 mpteq2dv 
 |-  ( x = N -> ( k e. I |-> if ( k = X , x , 0 ) ) = ( k e. I |-> if ( k = X , N , 0 ) ) )
42 41 eqeq2d 
 |-  ( x = N -> ( y = ( k e. I |-> if ( k = X , x , 0 ) ) <-> y = ( k e. I |-> if ( k = X , N , 0 ) ) ) )
43 42 ifbid 
 |-  ( x = N -> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) = if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) )
44 43 mpteq2dv 
 |-  ( x = N -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) ) )
45 oveq1 
 |-  ( x = N -> ( x .^ ( V ` X ) ) = ( N .^ ( V ` X ) ) )
46 44 45 eqeq12d 
 |-  ( x = N -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) <-> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) ) = ( N .^ ( V ` X ) ) ) )
47 46 imbi2d 
 |-  ( x = N -> ( ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , x , 0 ) ) , .1. , .0. ) ) = ( x .^ ( V ` X ) ) ) <-> ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) ) = ( N .^ ( V ` X ) ) ) ) )
48 eqid 
 |-  ( Base ` P ) = ( Base ` P )
49 1 8 48 5 9 10 mvrcl 
 |-  ( ph -> ( V ` X ) e. ( Base ` P ) )
50 6 48 mgpbas 
 |-  ( Base ` P ) = ( Base ` G )
51 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
52 6 51 ringidval 
 |-  ( 1r ` P ) = ( 0g ` G )
53 50 52 7 mulg0 
 |-  ( ( V ` X ) e. ( Base ` P ) -> ( 0 .^ ( V ` X ) ) = ( 1r ` P ) )
54 49 53 syl 
 |-  ( ph -> ( 0 .^ ( V ` X ) ) = ( 1r ` P ) )
55 1 2 3 4 51 5 9 mpl1 
 |-  ( ph -> ( 1r ` P ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) )
56 54 55 eqtr2d 
 |-  ( ph -> ( y e. D |-> if ( y = ( I X. { 0 } ) , .1. , .0. ) ) = ( 0 .^ ( V ` X ) ) )
57 oveq1 
 |-  ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) = ( n .^ ( V ` X ) ) -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( V ` X ) ) = ( ( n .^ ( V ` X ) ) ( .r ` P ) ( V ` X ) ) )
58 5 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> I e. W )
59 9 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> R e. Ring )
60 2 snifpsrbag 
 |-  ( ( I e. W /\ n e. NN0 ) -> ( k e. I |-> if ( k = X , n , 0 ) ) e. D )
61 5 60 sylan 
 |-  ( ( ph /\ n e. NN0 ) -> ( k e. I |-> if ( k = X , n , 0 ) ) e. D )
62 eqid 
 |-  ( .r ` P ) = ( .r ` P )
63 1nn0 
 |-  1 e. NN0
64 63 a1i 
 |-  ( n e. NN0 -> 1 e. NN0 )
65 2 snifpsrbag 
 |-  ( ( I e. W /\ 1 e. NN0 ) -> ( k e. I |-> if ( k = X , 1 , 0 ) ) e. D )
66 5 64 65 syl2an 
 |-  ( ( ph /\ n e. NN0 ) -> ( k e. I |-> if ( k = X , 1 , 0 ) ) e. D )
67 1 48 3 4 2 58 59 61 62 66 mplmonmul 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , 1 , 0 ) ) , .1. , .0. ) ) ) = ( y e. D |-> if ( y = ( ( k e. I |-> if ( k = X , n , 0 ) ) oF + ( k e. I |-> if ( k = X , 1 , 0 ) ) ) , .1. , .0. ) ) )
68 10 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> X e. I )
69 8 2 3 4 58 59 68 mvrval 
 |-  ( ( ph /\ n e. NN0 ) -> ( V ` X ) = ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , 1 , 0 ) ) , .1. , .0. ) ) )
70 69 eqcomd 
 |-  ( ( ph /\ n e. NN0 ) -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , 1 , 0 ) ) , .1. , .0. ) ) = ( V ` X ) )
71 70 oveq2d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , 1 , 0 ) ) , .1. , .0. ) ) ) = ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( V ` X ) ) )
72 simplr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. I ) -> n e. NN0 )
73 0nn0 
 |-  0 e. NN0
74 ifcl 
 |-  ( ( n e. NN0 /\ 0 e. NN0 ) -> if ( k = X , n , 0 ) e. NN0 )
75 72 73 74 sylancl 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. I ) -> if ( k = X , n , 0 ) e. NN0 )
76 63 73 ifcli 
 |-  if ( k = X , 1 , 0 ) e. NN0
77 76 a1i 
 |-  ( ( ( ph /\ n e. NN0 ) /\ k e. I ) -> if ( k = X , 1 , 0 ) e. NN0 )
78 eqidd 
 |-  ( ( ph /\ n e. NN0 ) -> ( k e. I |-> if ( k = X , n , 0 ) ) = ( k e. I |-> if ( k = X , n , 0 ) ) )
79 eqidd 
 |-  ( ( ph /\ n e. NN0 ) -> ( k e. I |-> if ( k = X , 1 , 0 ) ) = ( k e. I |-> if ( k = X , 1 , 0 ) ) )
80 58 75 77 78 79 offval2 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( k e. I |-> if ( k = X , n , 0 ) ) oF + ( k e. I |-> if ( k = X , 1 , 0 ) ) ) = ( k e. I |-> ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) ) )
81 iftrue 
 |-  ( k = X -> if ( k = X , n , 0 ) = n )
82 iftrue 
 |-  ( k = X -> if ( k = X , 1 , 0 ) = 1 )
83 81 82 oveq12d 
 |-  ( k = X -> ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) = ( n + 1 ) )
84 iftrue 
 |-  ( k = X -> if ( k = X , ( n + 1 ) , 0 ) = ( n + 1 ) )
85 83 84 eqtr4d 
 |-  ( k = X -> ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) = if ( k = X , ( n + 1 ) , 0 ) )
86 00id 
 |-  ( 0 + 0 ) = 0
87 iffalse 
 |-  ( -. k = X -> if ( k = X , n , 0 ) = 0 )
88 iffalse 
 |-  ( -. k = X -> if ( k = X , 1 , 0 ) = 0 )
89 87 88 oveq12d 
 |-  ( -. k = X -> ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) = ( 0 + 0 ) )
90 iffalse 
 |-  ( -. k = X -> if ( k = X , ( n + 1 ) , 0 ) = 0 )
91 86 89 90 3eqtr4a 
 |-  ( -. k = X -> ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) = if ( k = X , ( n + 1 ) , 0 ) )
92 85 91 pm2.61i 
 |-  ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) = if ( k = X , ( n + 1 ) , 0 )
93 92 mpteq2i 
 |-  ( k e. I |-> ( if ( k = X , n , 0 ) + if ( k = X , 1 , 0 ) ) ) = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) )
94 80 93 eqtrdi 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( k e. I |-> if ( k = X , n , 0 ) ) oF + ( k e. I |-> if ( k = X , 1 , 0 ) ) ) = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) )
95 94 eqeq2d 
 |-  ( ( ph /\ n e. NN0 ) -> ( y = ( ( k e. I |-> if ( k = X , n , 0 ) ) oF + ( k e. I |-> if ( k = X , 1 , 0 ) ) ) <-> y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) ) )
96 95 ifbid 
 |-  ( ( ph /\ n e. NN0 ) -> if ( y = ( ( k e. I |-> if ( k = X , n , 0 ) ) oF + ( k e. I |-> if ( k = X , 1 , 0 ) ) ) , .1. , .0. ) = if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) )
97 96 mpteq2dv 
 |-  ( ( ph /\ n e. NN0 ) -> ( y e. D |-> if ( y = ( ( k e. I |-> if ( k = X , n , 0 ) ) oF + ( k e. I |-> if ( k = X , 1 , 0 ) ) ) , .1. , .0. ) ) = ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) )
98 67 71 97 3eqtr3rd 
 |-  ( ( ph /\ n e. NN0 ) -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( V ` X ) ) )
99 1 5 9 mplringd 
 |-  ( ph -> P e. Ring )
100 6 ringmgp 
 |-  ( P e. Ring -> G e. Mnd )
101 99 100 syl 
 |-  ( ph -> G e. Mnd )
102 101 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> G e. Mnd )
103 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
104 49 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( V ` X ) e. ( Base ` P ) )
105 6 62 mgpplusg 
 |-  ( .r ` P ) = ( +g ` G )
106 50 7 105 mulgnn0p1 
 |-  ( ( G e. Mnd /\ n e. NN0 /\ ( V ` X ) e. ( Base ` P ) ) -> ( ( n + 1 ) .^ ( V ` X ) ) = ( ( n .^ ( V ` X ) ) ( .r ` P ) ( V ` X ) ) )
107 102 103 104 106 syl3anc 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n + 1 ) .^ ( V ` X ) ) = ( ( n .^ ( V ` X ) ) ( .r ` P ) ( V ` X ) ) )
108 98 107 eqeq12d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( n + 1 ) .^ ( V ` X ) ) <-> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) ( .r ` P ) ( V ` X ) ) = ( ( n .^ ( V ` X ) ) ( .r ` P ) ( V ` X ) ) ) )
109 57 108 imbitrrid 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) = ( n .^ ( V ` X ) ) -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( n + 1 ) .^ ( V ` X ) ) ) )
110 109 expcom 
 |-  ( n e. NN0 -> ( ph -> ( ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) = ( n .^ ( V ` X ) ) -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( n + 1 ) .^ ( V ` X ) ) ) ) )
111 110 a2d 
 |-  ( n e. NN0 -> ( ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , n , 0 ) ) , .1. , .0. ) ) = ( n .^ ( V ` X ) ) ) -> ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , ( n + 1 ) , 0 ) ) , .1. , .0. ) ) = ( ( n + 1 ) .^ ( V ` X ) ) ) ) )
112 23 31 39 47 56 111 nn0ind 
 |-  ( N e. NN0 -> ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) ) = ( N .^ ( V ` X ) ) ) )
113 11 112 mpcom 
 |-  ( ph -> ( y e. D |-> if ( y = ( k e. I |-> if ( k = X , N , 0 ) ) , .1. , .0. ) ) = ( N .^ ( V ` X ) ) )