Step |
Hyp |
Ref |
Expression |
1 |
|
eqcoe1ply1eq.p |
|- P = ( Poly1 ` R ) |
2 |
|
eqcoe1ply1eq.b |
|- B = ( Base ` P ) |
3 |
|
eqcoe1ply1eq.a |
|- A = ( coe1 ` K ) |
4 |
|
eqcoe1ply1eq.c |
|- C = ( coe1 ` L ) |
5 |
|
fveq2 |
|- ( k = n -> ( A ` k ) = ( A ` n ) ) |
6 |
|
fveq2 |
|- ( k = n -> ( C ` k ) = ( C ` n ) ) |
7 |
5 6
|
eqeq12d |
|- ( k = n -> ( ( A ` k ) = ( C ` k ) <-> ( A ` n ) = ( C ` n ) ) ) |
8 |
7
|
rspccv |
|- ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> ( n e. NN0 -> ( A ` n ) = ( C ` n ) ) ) |
9 |
8
|
adantl |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( n e. NN0 -> ( A ` n ) = ( C ` n ) ) ) |
10 |
9
|
imp |
|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) /\ n e. NN0 ) -> ( A ` n ) = ( C ` n ) ) |
11 |
3
|
fveq1i |
|- ( A ` n ) = ( ( coe1 ` K ) ` n ) |
12 |
4
|
fveq1i |
|- ( C ` n ) = ( ( coe1 ` L ) ` n ) |
13 |
10 11 12
|
3eqtr3g |
|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) /\ n e. NN0 ) -> ( ( coe1 ` K ) ` n ) = ( ( coe1 ` L ) ` n ) ) |
14 |
13
|
oveq1d |
|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) |
15 |
14
|
mpteq2dva |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) |
16 |
15
|
oveq2d |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
17 |
|
eqid |
|- ( var1 ` R ) = ( var1 ` R ) |
18 |
|
eqid |
|- ( .s ` P ) = ( .s ` P ) |
19 |
|
eqid |
|- ( mulGrp ` P ) = ( mulGrp ` P ) |
20 |
|
eqid |
|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) ) |
21 |
|
eqid |
|- ( coe1 ` K ) = ( coe1 ` K ) |
22 |
1 17 2 18 19 20 21
|
ply1coe |
|- ( ( R e. Ring /\ K e. B ) -> K = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
23 |
22
|
3adant3 |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> K = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
24 |
|
eqid |
|- ( coe1 ` L ) = ( coe1 ` L ) |
25 |
1 17 2 18 19 20 24
|
ply1coe |
|- ( ( R e. Ring /\ L e. B ) -> L = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
26 |
25
|
3adant2 |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> L = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) |
27 |
23 26
|
eqeq12d |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K = L <-> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) |
28 |
27
|
adantr |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> ( K = L <-> ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) = ( P gsum ( n e. NN0 |-> ( ( ( coe1 ` L ) ` n ) ( .s ` P ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) ) ) ) |
29 |
16 28
|
mpbird |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ A. k e. NN0 ( A ` k ) = ( C ` k ) ) -> K = L ) |
30 |
29
|
ex |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> K = L ) ) |