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

Metamath Proof Explorer

Theorem evls1vsca

Description: Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses ressply1evl2.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
ressply1evl2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
ressply1evl2.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
ressply1evl2.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
ressply1evl2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evls1vsca.1 ⊢ × = ( ·𝑠 ‘ 𝑊 )
evls1vsca.2 ⊢ · = ( .r ‘ 𝑆 )
evls1vsca.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1vsca.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1vsca.m ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
evls1vsca.n ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
evls1vsca.y ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion evls1vsca ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ressply1evl2.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 ressply1evl2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 ressply1evl2.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 ressply1evl2.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 ressply1evl2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
6 evls1vsca.1 ⊢ × = ( ·𝑠 ‘ 𝑊 )
7 evls1vsca.2 ⊢ · = ( .r ‘ 𝑆 )
8 evls1vsca.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 evls1vsca.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 evls1vsca.m ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
11 evls1vsca.n ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
12 evls1vsca.y ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13 id ⊢ ( 𝜑 → 𝜑 )
14 eqid ⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
15 eqid ⊢ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) = ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 )
16 14 4 3 5 9 15 ressply1vsca ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝑁 ∈ 𝐵 ) ) → ( 𝐴 ( ·𝑠 ‘ 𝑊 ) 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
17 13 10 11 16 syl12anc ⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑊 ) 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
18 6 oveqi ⊢ ( 𝐴 × 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ 𝑊 ) 𝑁 )
19 5 fvexi ⊢ 𝐵 ∈ V
20 eqid ⊢ ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) = ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) )
21 15 20 ressvsca ⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) = ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) )
22 19 21 ax-mp ⊢ ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) = ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) )
23 22 oveqi ⊢ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 )
24 17 18 23 3eqtr4g ⊢ ( 𝜑 → ( 𝐴 × 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) )
25 24 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) )
26 25 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) )
27 eqid ⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
28 1 2 3 4 5 27 8 9 ressply1evl ⊢ ( 𝜑 → 𝑄 = ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) )
29 28 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝐴 × 𝑁 ) ) )
30 4 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
31 8 9 30 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
32 crngring ⊢ ( 𝑈 ∈ CRing → 𝑈 ∈ Ring )
33 3 ply1lmod ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
34 31 32 33 3syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
35 2 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
36 9 35 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
37 4 2 ressbas2 ⊢ ( 𝑅 ⊆ 𝐾 → 𝑅 = ( Base ‘ 𝑈 ) )
38 36 37 syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
39 4 ovexi ⊢ 𝑈 ∈ V
40 3 ply1sca ⊢ ( 𝑈 ∈ V → 𝑈 = ( Scalar ‘ 𝑊 ) )
41 39 40 mp1i ⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
42 41 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
43 38 42 eqtrd ⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
44 10 43 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
45 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
46 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
47 5 45 6 46 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑁 ∈ 𝐵 ) → ( 𝐴 × 𝑁 ) ∈ 𝐵 )
48 34 44 11 47 syl3anc ⊢ ( 𝜑 → ( 𝐴 × 𝑁 ) ∈ 𝐵 )
49 48 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝐴 × 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) )
50 29 49 eqtr2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) = ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) )
51 50 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) )
52 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
53 eqid ⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
54 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
55 14 4 3 5 9 53 54 52 ressply1bas2 ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
56 inss2 ⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
57 55 56 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
58 57 11 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
59 28 fveq1d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) )
60 11 fvresd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) )
61 59 60 eqtr2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) = ( 𝑄 ‘ 𝑁 ) )
62 61 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) )
63 58 62 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
64 36 10 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
65 27 14 2 52 8 12 63 64 20 7 evl1vsd ⊢ ( 𝜑 → ( ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
66 65 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
67 26 51 66 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )