evl1subd

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

	Ref	Expression
Hypotheses	evl1addd.q	$⊢ O = {eval}_{1} (R)$
	evl1addd.p	$⊢ P = {Poly}_{1} (R)$
	evl1addd.b	$⊢ B = {Base}_{R}$
	evl1addd.u	$⊢ U = {Base}_{P}$
	evl1addd.1	$⊢ φ \to R \in CRing$
	evl1addd.2	$⊢ φ \to Y \in B$
	evl1addd.3	$⊢ φ \to (M \in U \land O (M) (Y) = V)$
	evl1addd.4	$⊢ φ \to (N \in U \land O (N) (Y) = W)$
	evl1subd.s	$⊢ \underset{˙}{-} = -_{P}$
	evl1subd.d	$⊢ D = -_{R}$
Assertion	evl1subd	$⊢ φ \to (M \underset{˙}{-} N \in U \land O (M \underset{˙}{-} N) (Y) = V D W)$

Proof

Step	Hyp	Ref	Expression
1		evl1addd.q	$⊢ O = {eval}_{1} (R)$
2		evl1addd.p	$⊢ P = {Poly}_{1} (R)$
3		evl1addd.b	$⊢ B = {Base}_{R}$
4		evl1addd.u	$⊢ U = {Base}_{P}$
5		evl1addd.1	$⊢ φ \to R \in CRing$
6		evl1addd.2	$⊢ φ \to Y \in B$
7		evl1addd.3	$⊢ φ \to (M \in U \land O (M) (Y) = V)$
8		evl1addd.4	$⊢ φ \to (N \in U \land O (N) (Y) = W)$
9		evl1subd.s	$⊢ \underset{˙}{-} = -_{P}$
10		evl1subd.d	$⊢ D = -_{R}$
11		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
12	1 2 11 3	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} B))$
13	5 12	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} B))$
14		rhmghm	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O \in (P GrpHom (R ↑_{𝑠} B))$
15	13 14	syl	$⊢ φ \to O \in (P GrpHom (R ↑_{𝑠} B))$
16		ghmgrp1	$⊢ O \in (P GrpHom (R ↑_{𝑠} B)) \to P \in Grp$
17	15 16	syl	$⊢ φ \to P \in Grp$
18	7	simpld	$⊢ φ \to M \in U$
19	8	simpld	$⊢ φ \to N \in U$
20	4 9	grpsubcl	$⊢ (P \in Grp \land M \in U \land N \in U) \to M \underset{˙}{-} N \in U$
21	17 18 19 20	syl3anc	$⊢ φ \to M \underset{˙}{-} N \in U$
22		eqid	$⊢ -_{(R ↑_{𝑠} B)} = -_{(R ↑_{𝑠} B)}$
23	4 9 22	ghmsub	$⊢ (O \in (P GrpHom (R ↑_{𝑠} B)) \land M \in U \land N \in U) \to O (M \underset{˙}{-} N) = O (M) -_{(R ↑_{𝑠} B)} O (N)$
24	15 18 19 23	syl3anc	$⊢ φ \to O (M \underset{˙}{-} N) = O (M) -_{(R ↑_{𝑠} B)} O (N)$
25		crngring	$⊢ R \in CRing \to R \in Ring$
26		ringgrp	$⊢ R \in Ring \to R \in Grp$
27	5 25 26	3syl	$⊢ φ \to R \in Grp$
28	3	fvexi	$⊢ B \in V$
29	28	a1i	$⊢ φ \to B \in V$
30		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
31	4 30	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
32	13 31	syl	$⊢ φ \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
33	32 18	ffvelcdmd	$⊢ φ \to O (M) \in {Base}_{(R ↑_{𝑠} B)}$
34	32 19	ffvelcdmd	$⊢ φ \to O (N) \in {Base}_{(R ↑_{𝑠} B)}$
35	11 30 10 22	pwssub	$⊢ ((R \in Grp \land B \in V) \land (O (M) \in {Base}_{(R ↑_{𝑠} B)} \land O (N) \in {Base}_{(R ↑_{𝑠} B)})) \to O (M) -_{(R ↑_{𝑠} B)} O (N) = O (M) D_{f} O (N)$
36	27 29 33 34 35	syl22anc	$⊢ φ \to O (M) -_{(R ↑_{𝑠} B)} O (N) = O (M) D_{f} O (N)$
37	24 36	eqtrd	$⊢ φ \to O (M \underset{˙}{-} N) = O (M) D_{f} O (N)$
38	37	fveq1d	$⊢ φ \to O (M \underset{˙}{-} N) (Y) = (O (M) D_{f} O (N)) (Y)$
39	11 3 30 5 29 33	pwselbas	$⊢ φ \to O (M) : B ⟶ B$
40	39	ffnd	$⊢ φ \to O (M) Fn B$
41	11 3 30 5 29 34	pwselbas	$⊢ φ \to O (N) : B ⟶ B$
42	41	ffnd	$⊢ φ \to O (N) Fn B$
43		fnfvof	$⊢ ((O (M) Fn B \land O (N) Fn B) \land (B \in V \land Y \in B)) \to (O (M) D_{f} O (N)) (Y) = O (M) (Y) D O (N) (Y)$
44	40 42 29 6 43	syl22anc	$⊢ φ \to (O (M) D_{f} O (N)) (Y) = O (M) (Y) D O (N) (Y)$
45	7	simprd	$⊢ φ \to O (M) (Y) = V$
46	8	simprd	$⊢ φ \to O (N) (Y) = W$
47	45 46	oveq12d	$⊢ φ \to O (M) (Y) D O (N) (Y) = V D W$
48	38 44 47	3eqtrd	$⊢ φ \to O (M \underset{˙}{-} N) (Y) = V D W$
49	21 48	jca	$⊢ φ \to (M \underset{˙}{-} N \in U \land O (M \underset{˙}{-} N) (Y) = V D W)$

Metamath Proof Explorer

Theorem evl1subd

Proof