Metamath Proof Explorer

Theorem ply1moneq

Description: Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1moneq.p 
|- P = ( Poly1 ` R )
ply1moneq.x 
|- X = ( var1 ` R )
ply1moneq.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
ply1moneq.r 
|- ( ph -> R e. NzRing )
ply1moneq.m 
|- ( ph -> M e. NN0 )
ply1moneq.n 
|- ( ph -> N e. NN0 )
Assertion ply1moneq 
|- ( ph -> ( ( M .^ X ) = ( N .^ X ) <-> M = N ) )

Proof

Step Hyp Ref Expression
1 ply1moneq.p 
 |-  P = ( Poly1 ` R )
2 ply1moneq.x 
 |-  X = ( var1 ` R )
3 ply1moneq.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
4 ply1moneq.r 
 |-  ( ph -> R e. NzRing )
5 ply1moneq.m 
 |-  ( ph -> M e. NN0 )
6 ply1moneq.n 
 |-  ( ph -> N e. NN0 )
7 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
8 4 7 syl 
 |-  ( ph -> R e. Ring )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
11 1 2 3 8 5 9 10 coe1mon 
 |-  ( ph -> ( coe1 ` ( M .^ X ) ) = ( k e. NN0 |-> if ( k = M , ( 1r ` R ) , ( 0g ` R ) ) ) )
12 fvexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1r ` R ) e. _V )
13 fvexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( 0g ` R ) e. _V )
14 12 13 ifcld 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k = M , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
15 11 14 fvmpt2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` ( M .^ X ) ) ` k ) = if ( k = M , ( 1r ` R ) , ( 0g ` R ) ) )
16 1 2 3 8 6 9 10 coe1mon 
 |-  ( ph -> ( coe1 ` ( N .^ X ) ) = ( k e. NN0 |-> if ( k = N , ( 1r ` R ) , ( 0g ` R ) ) ) )
17 12 13 ifcld 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k = N , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
18 16 17 fvmpt2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( coe1 ` ( N .^ X ) ) ` k ) = if ( k = N , ( 1r ` R ) , ( 0g ` R ) ) )
19 15 18 eqeq12d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( coe1 ` ( M .^ X ) ) ` k ) = ( ( coe1 ` ( N .^ X ) ) ` k ) <-> if ( k = M , ( 1r ` R ) , ( 0g ` R ) ) = if ( k = N , ( 1r ` R ) , ( 0g ` R ) ) ) )
20 10 9 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
21 4 20 syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
22 21 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( 1r ` R ) =/= ( 0g ` R ) )
23 ifnebib 
 |-  ( ( 1r ` R ) =/= ( 0g ` R ) -> ( if ( k = M , ( 1r ` R ) , ( 0g ` R ) ) = if ( k = N , ( 1r ` R ) , ( 0g ` R ) ) <-> ( k = M <-> k = N ) ) )
24 22 23 syl 
 |-  ( ( ph /\ k e. NN0 ) -> ( if ( k = M , ( 1r ` R ) , ( 0g ` R ) ) = if ( k = N , ( 1r ` R ) , ( 0g ` R ) ) <-> ( k = M <-> k = N ) ) )
25 19 24 bitrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( coe1 ` ( M .^ X ) ) ` k ) = ( ( coe1 ` ( N .^ X ) ) ` k ) <-> ( k = M <-> k = N ) ) )
26 25 ralbidva 
 |-  ( ph -> ( A. k e. NN0 ( ( coe1 ` ( M .^ X ) ) ` k ) = ( ( coe1 ` ( N .^ X ) ) ` k ) <-> A. k e. NN0 ( k = M <-> k = N ) ) )
27 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
28 eqid 
 |-  ( Base ` P ) = ( Base ` P )
29 1 2 27 3 28 ply1moncl 
 |-  ( ( R e. Ring /\ M e. NN0 ) -> ( M .^ X ) e. ( Base ` P ) )
30 8 5 29 syl2anc 
 |-  ( ph -> ( M .^ X ) e. ( Base ` P ) )
31 1 2 27 3 28 ply1moncl 
 |-  ( ( R e. Ring /\ N e. NN0 ) -> ( N .^ X ) e. ( Base ` P ) )
32 8 6 31 syl2anc 
 |-  ( ph -> ( N .^ X ) e. ( Base ` P ) )
33 eqid 
 |-  ( coe1 ` ( M .^ X ) ) = ( coe1 ` ( M .^ X ) )
34 eqid 
 |-  ( coe1 ` ( N .^ X ) ) = ( coe1 ` ( N .^ X ) )
35 1 28 33 34 ply1coe1eq 
 |-  ( ( R e. Ring /\ ( M .^ X ) e. ( Base ` P ) /\ ( N .^ X ) e. ( Base ` P ) ) -> ( A. k e. NN0 ( ( coe1 ` ( M .^ X ) ) ` k ) = ( ( coe1 ` ( N .^ X ) ) ` k ) <-> ( M .^ X ) = ( N .^ X ) ) )
36 8 30 32 35 syl3anc 
 |-  ( ph -> ( A. k e. NN0 ( ( coe1 ` ( M .^ X ) ) ` k ) = ( ( coe1 ` ( N .^ X ) ) ` k ) <-> ( M .^ X ) = ( N .^ X ) ) )
37 5 6 eqelbid 
 |-  ( ph -> ( A. k e. NN0 ( k = M <-> k = N ) <-> M = N ) )
38 26 36 37 3bitr3d 
 |-  ( ph -> ( ( M .^ X ) = ( N .^ X ) <-> M = N ) )