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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
r1p0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
r1p0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑁 )
r1p0.0 ⊢ 0 = ( 0g ‘ 𝑃 )
Assertion r1p0 ( 𝜑 → ( 0 𝐸 𝐷 ) = 0 )

Proof

Step Hyp Ref Expression
1 r1padd1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4 r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5 r1p0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 r1p0.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑁 )
7 r1p0.0 ⊢ 0 = ( 0g ‘ 𝑃 )
8 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
9 5 8 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
10 9 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
11 10 oveq1d ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 0 ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) 0 ) )
12 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
13 5 12 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
14 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15 2 7 ring0cl ⊢ ( 𝑃 ∈ Ring → 0 ∈ 𝑈 )
16 5 14 15 3syl ⊢ ( 𝜑 → 0 ∈ 𝑈 )
17 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
18 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
19 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
20 2 17 18 19 7 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ 0 ∈ 𝑈 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) 0 ) = 0 )
21 13 16 20 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) 0 ) = 0 )
22 11 21 eqtrd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 0 ) = 0 )
23 22 oveq1d ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 0 ) 𝐸 𝐷 ) = ( 0 𝐸 𝐷 ) )
24 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26 24 25 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27 5 26 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
28 1 2 3 4 5 16 6 18 24 27 r1pvsca ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 0 ) 𝐸 𝐷 ) = ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 𝐸 𝐷 ) ) )
29 10 oveq1d ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 𝐸 𝐷 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 𝐸 𝐷 ) ) )
30 4 1 2 3 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝑈 ∧ 𝐷 ∈ 𝑁 ) → ( 0 𝐸 𝐷 ) ∈ 𝑈 )
31 5 16 6 30 syl3anc ⊢ ( 𝜑 → ( 0 𝐸 𝐷 ) ∈ 𝑈 )
32 2 17 18 19 7 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 0 𝐸 𝐷 ) ∈ 𝑈 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 𝐸 𝐷 ) ) = 0 )
33 13 31 32 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 𝐸 𝐷 ) ) = 0 )
34 28 29 33 3eqtrd ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 0 ) 𝐸 𝐷 ) = 0 )
35 23 34 eqtr3d ⊢ ( 𝜑 → ( 0 𝐸 𝐷 ) = 0 )