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

Metamath Proof Explorer

Theorem evls1subd

Description: Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-2025)

Ref Expression
Hypotheses ressply1evl.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
ressply1evl.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
ressply1evl.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
ressply1evl.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
ressply1evl.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evls1subd.1 ⊢ 𝐷 = ( -g ‘ 𝑊 )
evls1subd.2 ⊢ − = ( -g ‘ 𝑆 )
evls1subd.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1subd.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1subd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
evls1subd.n ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
evls1subd.y ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion evls1subd ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ressply1evl.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 ressply1evl.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 ressply1evl.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 ressply1evl.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 ressply1evl.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
6 evls1subd.1 ⊢ 𝐷 = ( -g ‘ 𝑊 )
7 evls1subd.2 ⊢ − = ( -g ‘ 𝑆 )
8 evls1subd.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 evls1subd.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 evls1subd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
11 evls1subd.n ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
12 evls1subd.y ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13 6 oveqi ⊢ ( 𝑀 𝐷 𝑁 ) = ( 𝑀 ( -g ‘ 𝑊 ) 𝑁 )
14 eqid ⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
15 eqid ⊢ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) = ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 )
16 14 4 3 5 9 15 10 11 ressply1sub ⊢ ( 𝜑 → ( 𝑀 ( -g ‘ 𝑊 ) 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
17 13 16 eqtrid ⊢ ( 𝜑 → ( 𝑀 𝐷 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
18 14 4 3 5 subrgply1 ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubRing ‘ ( Poly1 ‘ 𝑆 ) ) )
19 subrgsubg ⊢ ( 𝐵 ∈ ( SubRing ‘ ( Poly1 ‘ 𝑆 ) ) → 𝐵 ∈ ( SubGrp ‘ ( Poly1 ‘ 𝑆 ) ) )
20 9 18 19 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ ( Poly1 ‘ 𝑆 ) ) )
21 eqid ⊢ ( -g ‘ ( Poly1 ‘ 𝑆 ) ) = ( -g ‘ ( Poly1 ‘ 𝑆 ) )
22 eqid ⊢ ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) = ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) )
23 21 15 22 subgsub ⊢ ( ( 𝐵 ∈ ( SubGrp ‘ ( Poly1 ‘ 𝑆 ) ) ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
24 20 10 11 23 syl3anc ⊢ ( 𝜑 → ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
25 17 24 eqtr4d ⊢ ( 𝜑 → ( 𝑀 𝐷 𝑁 ) = ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) )
26 25 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) )
27 26 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) )
28 eqid ⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
29 1 2 3 4 5 28 8 9 ressply1evl ⊢ ( 𝜑 → 𝑄 = ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) )
30 29 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝑀 𝐷 𝑁 ) ) )
31 4 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
32 3 ply1ring ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
33 9 31 32 3syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
34 33 ringgrpd ⊢ ( 𝜑 → 𝑊 ∈ Grp )
35 5 6 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑀 𝐷 𝑁 ) ∈ 𝐵 )
36 34 10 11 35 syl3anc ⊢ ( 𝜑 → ( 𝑀 𝐷 𝑁 ) ∈ 𝐵 )
37 36 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝑀 𝐷 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) )
38 30 37 eqtr2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) = ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) )
39 38 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) )
40 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
41 eqid ⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
42 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
43 14 4 3 5 9 41 42 40 ressply1bas2 ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
44 inss2 ⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
45 43 44 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
46 45 10 sseldd ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
47 29 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑀 ) )
48 10 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑀 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) )
49 47 48 eqtr2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) = ( 𝑄 ‘ 𝑀 ) )
50 49 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) )
51 46 50 jca ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )
52 45 11 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
53 29 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) )
54 11 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) )
55 53 54 eqtr2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) = ( 𝑄 ‘ 𝑁 ) )
56 55 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) )
57 52 56 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
58 28 14 2 40 8 12 51 57 21 7 evl1subd ⊢ ( 𝜑 → ( ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
59 58 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
60 27 39 59 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )