Metamath Proof Explorer

Theorem evl1subd

Description: Polynomial evaluation builder for subtraction of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1addd.q ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1addd.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
evl1addd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evl1addd.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
evl1addd.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1addd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
evl1addd.3 ⊢ ( 𝜑 → ( 𝑀 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
evl1addd.4 ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) = 𝑊 ) )
evl1subd.s ⊢ − = ( -g ‘ 𝑃 )
evl1subd.d ⊢ 𝐷 = ( -g ‘ 𝑅 )
Assertion evl1subd ( 𝜑 → ( ( 𝑀 − 𝑁 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 𝐷 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 evl1addd.q ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2 evl1addd.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 evl1addd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 evl1addd.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
5 evl1addd.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 evl1addd.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 evl1addd.3 ⊢ ( 𝜑 → ( 𝑀 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
8 evl1addd.4 ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) = 𝑊 ) )
9 evl1subd.s ⊢ − = ( -g ‘ 𝑃 )
10 evl1subd.d ⊢ 𝐷 = ( -g ‘ 𝑅 )
11 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
12 1 2 11 3 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
13 5 12 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
14 rhmghm ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) )
15 13 14 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) )
16 ghmgrp1 ⊢ ( 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) → 𝑃 ∈ Grp )
17 15 16 syl ⊢ ( 𝜑 → 𝑃 ∈ Grp )
18 7 simpld ⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
19 8 simpld ⊢ ( 𝜑 → 𝑁 ∈ 𝑈 )
20 4 9 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑈 ) → ( 𝑀 − 𝑁 ) ∈ 𝑈 )
21 17 18 19 20 syl3anc ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ 𝑈 )
22 eqid ⊢ ( -g ‘ ( 𝑅 ↑s 𝐵 ) ) = ( -g ‘ ( 𝑅 ↑s 𝐵 ) )
23 4 9 22 ghmsub ⊢ ( ( 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) ∧ 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑈 ) → ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ( -g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) )
24 15 18 19 23 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ( -g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) )
25 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
26 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
27 5 25 26 3syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
28 3 fvexi ⊢ 𝐵 ∈ V
29 28 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
30 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
31 4 30 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
32 13 31 syl ⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
33 32 18 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
34 32 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑁 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
35 11 30 10 22 pwssub ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝐵 ∈ V ) ∧ ( ( 𝑂 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) ∧ ( 𝑂 ‘ 𝑁 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) ) ) → ( ( 𝑂 ‘ 𝑀 ) ( -g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ∘f 𝐷 ( 𝑂 ‘ 𝑁 ) ) )
36 27 29 33 34 35 syl22anc ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ( -g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ∘f 𝐷 ( 𝑂 ‘ 𝑁 ) ) )
37 24 36 eqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ∘f 𝐷 ( 𝑂 ‘ 𝑁 ) ) )
38 37 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ 𝑀 ) ∘f 𝐷 ( 𝑂 ‘ 𝑁 ) ) ‘ 𝑌 ) )
39 11 3 30 5 29 33 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) : 𝐵 ⟶ 𝐵 )
40 39 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) Fn 𝐵 )
41 11 3 30 5 29 34 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑁 ) : 𝐵 ⟶ 𝐵 )
42 41 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑁 ) Fn 𝐵 )
43 fnfvof ⊢ ( ( ( ( 𝑂 ‘ 𝑀 ) Fn 𝐵 ∧ ( 𝑂 ‘ 𝑁 ) Fn 𝐵 ) ∧ ( 𝐵 ∈ V ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑂 ‘ 𝑀 ) ∘f 𝐷 ( 𝑂 ‘ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) 𝐷 ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) ) )
44 40 42 29 6 43 syl22anc ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝑀 ) ∘f 𝐷 ( 𝑂 ‘ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) 𝐷 ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) ) )
45 7 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = 𝑉 )
46 8 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) = 𝑊 )
47 45 46 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) 𝐷 ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) ) = ( 𝑉 𝐷 𝑊 ) )
48 38 44 47 3eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 𝐷 𝑊 ) )
49 21 48 jca ⊢ ( 𝜑 → ( ( 𝑀 − 𝑁 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑀 − 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 𝐷 𝑊 ) ) )