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 |
1 2 3 4
|
eqcoe1ply1eq |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) -> K = L ) ) |
6 |
|
fveq2 |
|- ( K = L -> ( coe1 ` K ) = ( coe1 ` L ) ) |
7 |
6
|
adantl |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) -> ( coe1 ` K ) = ( coe1 ` L ) ) |
8 |
7 3 4
|
3eqtr4g |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) -> A = C ) |
9 |
8
|
adantr |
|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) /\ k e. NN0 ) -> A = C ) |
10 |
9
|
fveq1d |
|- ( ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) /\ k e. NN0 ) -> ( A ` k ) = ( C ` k ) ) |
11 |
10
|
ralrimiva |
|- ( ( ( R e. Ring /\ K e. B /\ L e. B ) /\ K = L ) -> A. k e. NN0 ( A ` k ) = ( C ` k ) ) |
12 |
11
|
ex |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( K = L -> A. k e. NN0 ( A ` k ) = ( C ` k ) ) ) |
13 |
5 12
|
impbid |
|- ( ( R e. Ring /\ K e. B /\ L e. B ) -> ( A. k e. NN0 ( A ` k ) = ( C ` k ) <-> K = L ) ) |