Metamath Proof Explorer

Theorem r1p0

Description: Polynomial remainder operation of a division of the zero polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses r1padd1.p 
|- P = ( Poly1 ` R )
r1padd1.u 
|- U = ( Base ` P )
r1padd1.n 
|- N = ( Unic1p ` R )
r1padd1.e 
|- E = ( rem1p ` R )
r1p0.r 
|- ( ph -> R e. Ring )
r1p0.d 
|- ( ph -> D e. N )
r1p0.0 
|- .0. = ( 0g ` P )
Assertion r1p0 
|- ( ph -> ( .0. E D ) = .0. )

Proof

Step Hyp Ref Expression
1 r1padd1.p 
 |-  P = ( Poly1 ` R )
2 r1padd1.u 
 |-  U = ( Base ` P )
3 r1padd1.n 
 |-  N = ( Unic1p ` R )
4 r1padd1.e 
 |-  E = ( rem1p ` R )
5 r1p0.r 
 |-  ( ph -> R e. Ring )
6 r1p0.d 
 |-  ( ph -> D e. N )
7 r1p0.0 
 |-  .0. = ( 0g ` P )
8 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
9 5 8 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
10 9 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
11 10 oveq1d 
 |-  ( ph -> ( ( 0g ` R ) ( .s ` P ) .0. ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) .0. ) )
12 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
13 5 12 syl 
 |-  ( ph -> P e. LMod )
14 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 2 7 ring0cl 
 |-  ( P e. Ring -> .0. e. U )
16 5 14 15 3syl 
 |-  ( ph -> .0. e. U )
17 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
18 eqid 
 |-  ( .s ` P ) = ( .s ` P )
19 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
20 2 17 18 19 7 lmod0vs 
 |-  ( ( P e. LMod /\ .0. e. U ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) .0. ) = .0. )
21 13 16 20 syl2anc 
 |-  ( ph -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) .0. ) = .0. )
22 11 21 eqtrd 
 |-  ( ph -> ( ( 0g ` R ) ( .s ` P ) .0. ) = .0. )
23 22 oveq1d 
 |-  ( ph -> ( ( ( 0g ` R ) ( .s ` P ) .0. ) E D ) = ( .0. E D ) )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
26 24 25 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
27 5 26 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
28 1 2 3 4 5 16 6 18 24 27 r1pvsca 
 |-  ( ph -> ( ( ( 0g ` R ) ( .s ` P ) .0. ) E D ) = ( ( 0g ` R ) ( .s ` P ) ( .0. E D ) ) )
29 10 oveq1d 
 |-  ( ph -> ( ( 0g ` R ) ( .s ` P ) ( .0. E D ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( .0. E D ) ) )
30 4 1 2 3 r1pcl 
 |-  ( ( R e. Ring /\ .0. e. U /\ D e. N ) -> ( .0. E D ) e. U )
31 5 16 6 30 syl3anc 
 |-  ( ph -> ( .0. E D ) e. U )
32 2 17 18 19 7 lmod0vs 
 |-  ( ( P e. LMod /\ ( .0. E D ) e. U ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( .0. E D ) ) = .0. )
33 13 31 32 syl2anc 
 |-  ( ph -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( .0. E D ) ) = .0. )
34 28 29 33 3eqtrd 
 |-  ( ph -> ( ( ( 0g ` R ) ( .s ` P ) .0. ) E D ) = .0. )
35 23 34 eqtr3d 
 |-  ( ph -> ( .0. E D ) = .0. )