This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1scleq

Description: Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses ply1scleq.p 
|- P = ( Poly1 ` R )
ply1scleq.b 
|- B = ( Base ` R )
ply1scleq.a 
|- A = ( algSc ` P )
ply1scleq.r 
|- ( ph -> R e. Ring )
ply1scleq.e 
|- ( ph -> E e. B )
ply1scleq.f 
|- ( ph -> F e. B )
Assertion ply1scleq 
|- ( ph -> ( ( A ` E ) = ( A ` F ) <-> E = F ) )

Proof

Step Hyp Ref Expression
1 ply1scleq.p 
 |-  P = ( Poly1 ` R )
2 ply1scleq.b 
 |-  B = ( Base ` R )
3 ply1scleq.a 
 |-  A = ( algSc ` P )
4 ply1scleq.r 
 |-  ( ph -> R e. Ring )
5 ply1scleq.e 
 |-  ( ph -> E e. B )
6 ply1scleq.f 
 |-  ( ph -> F e. B )
7 fveq2 
 |-  ( d = 0 -> ( ( coe1 ` ( A ` E ) ) ` d ) = ( ( coe1 ` ( A ` E ) ) ` 0 ) )
8 fveq2 
 |-  ( d = 0 -> ( ( coe1 ` ( A ` F ) ) ` d ) = ( ( coe1 ` ( A ` F ) ) ` 0 ) )
9 7 8 eqeq12d 
 |-  ( d = 0 -> ( ( ( coe1 ` ( A ` E ) ) ` d ) = ( ( coe1 ` ( A ` F ) ) ` d ) <-> ( ( coe1 ` ( A ` E ) ) ` 0 ) = ( ( coe1 ` ( A ` F ) ) ` 0 ) ) )
10 eqid 
 |-  ( Base ` P ) = ( Base ` P )
11 1 3 2 10 ply1sclcl 
 |-  ( ( R e. Ring /\ E e. B ) -> ( A ` E ) e. ( Base ` P ) )
12 4 5 11 syl2anc 
 |-  ( ph -> ( A ` E ) e. ( Base ` P ) )
13 1 3 2 10 ply1sclcl 
 |-  ( ( R e. Ring /\ F e. B ) -> ( A ` F ) e. ( Base ` P ) )
14 4 6 13 syl2anc 
 |-  ( ph -> ( A ` F ) e. ( Base ` P ) )
15 eqid 
 |-  ( coe1 ` ( A ` E ) ) = ( coe1 ` ( A ` E ) )
16 eqid 
 |-  ( coe1 ` ( A ` F ) ) = ( coe1 ` ( A ` F ) )
17 1 10 15 16 ply1coe1eq 
 |-  ( ( R e. Ring /\ ( A ` E ) e. ( Base ` P ) /\ ( A ` F ) e. ( Base ` P ) ) -> ( A. d e. NN0 ( ( coe1 ` ( A ` E ) ) ` d ) = ( ( coe1 ` ( A ` F ) ) ` d ) <-> ( A ` E ) = ( A ` F ) ) )
18 4 12 14 17 syl3anc 
 |-  ( ph -> ( A. d e. NN0 ( ( coe1 ` ( A ` E ) ) ` d ) = ( ( coe1 ` ( A ` F ) ) ` d ) <-> ( A ` E ) = ( A ` F ) ) )
19 18 biimpar 
 |-  ( ( ph /\ ( A ` E ) = ( A ` F ) ) -> A. d e. NN0 ( ( coe1 ` ( A ` E ) ) ` d ) = ( ( coe1 ` ( A ` F ) ) ` d ) )
20 0nn0 
 |-  0 e. NN0
21 20 a1i 
 |-  ( ( ph /\ ( A ` E ) = ( A ` F ) ) -> 0 e. NN0 )
22 9 19 21 rspcdva 
 |-  ( ( ph /\ ( A ` E ) = ( A ` F ) ) -> ( ( coe1 ` ( A ` E ) ) ` 0 ) = ( ( coe1 ` ( A ` F ) ) ` 0 ) )
23 1 3 2 ply1sclid 
 |-  ( ( R e. Ring /\ E e. B ) -> E = ( ( coe1 ` ( A ` E ) ) ` 0 ) )
24 4 5 23 syl2anc 
 |-  ( ph -> E = ( ( coe1 ` ( A ` E ) ) ` 0 ) )
25 24 adantr 
 |-  ( ( ph /\ ( A ` E ) = ( A ` F ) ) -> E = ( ( coe1 ` ( A ` E ) ) ` 0 ) )
26 1 3 2 ply1sclid 
 |-  ( ( R e. Ring /\ F e. B ) -> F = ( ( coe1 ` ( A ` F ) ) ` 0 ) )
27 4 6 26 syl2anc 
 |-  ( ph -> F = ( ( coe1 ` ( A ` F ) ) ` 0 ) )
28 27 adantr 
 |-  ( ( ph /\ ( A ` E ) = ( A ` F ) ) -> F = ( ( coe1 ` ( A ` F ) ) ` 0 ) )
29 22 25 28 3eqtr4d 
 |-  ( ( ph /\ ( A ` E ) = ( A ` F ) ) -> E = F )
30 fveq2 
 |-  ( E = F -> ( A ` E ) = ( A ` F ) )
31 30 adantl 
 |-  ( ( ph /\ E = F ) -> ( A ` E ) = ( A ` F ) )
32 29 31 impbida 
 |-  ( ph -> ( ( A ` E ) = ( A ` F ) <-> E = F ) )