evl1addd

Description: Polynomial evaluation builder for addition 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)$
	evl1addd.g	$⊢ \underset{˙}{✚} = +_{P}$
	evl1addd.a	$⊢ \underset{˙}{+} = +_{R}$
Assertion	evl1addd	$⊢ φ \to (M \underset{˙}{✚} N \in U \land O (M \underset{˙}{✚} N) (Y) = V \underset{˙}{+} 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		evl1addd.g	$⊢ \underset{˙}{✚} = +_{P}$
10		evl1addd.a	$⊢ \underset{˙}{+} = +_{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	grpcl	$⊢ (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	ghmlin	$⊢ (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		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
26	3	fvexi	$⊢ B \in V$
27	26	a1i	$⊢ φ \to B \in V$
28	4 25	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
29	13 28	syl	$⊢ φ \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
30	29 18	ffvelrnd	$⊢ φ \to O (M) \in {Base}_{(R ↑_{𝑠} B)}$
31	29 19	ffvelrnd	$⊢ φ \to O (N) \in {Base}_{(R ↑_{𝑠} B)}$
32	11 25 5 27 30 31 10 22	pwsplusgval	$⊢ φ \to O (M) +_{(R ↑_{𝑠} B)} O (N) = O (M) {\underset{˙}{+}}_{f} O (N)$
33	24 32	eqtrd	$⊢ φ \to O (M \underset{˙}{✚} N) = O (M) {\underset{˙}{+}}_{f} O (N)$
34	33	fveq1d	$⊢ φ \to O (M \underset{˙}{✚} N) (Y) = (O (M) {\underset{˙}{+}}_{f} O (N)) (Y)$
35	11 3 25 5 27 30	pwselbas	$⊢ φ \to O (M) : B ⟶ B$
36	35	ffnd	$⊢ φ \to O (M) Fn B$
37	11 3 25 5 27 31	pwselbas	$⊢ φ \to O (N) : B ⟶ B$
38	37	ffnd	$⊢ φ \to O (N) Fn B$
39		fnfvof	$⊢ ((O (M) Fn B \land O (N) Fn B) \land (B \in V \land Y \in B)) \to (O (M) {\underset{˙}{+}}_{f} O (N)) (Y) = O (M) (Y) \underset{˙}{+} O (N) (Y)$
40	36 38 27 6 39	syl22anc	$⊢ φ \to (O (M) {\underset{˙}{+}}_{f} O (N)) (Y) = O (M) (Y) \underset{˙}{+} O (N) (Y)$
41	7	simprd	$⊢ φ \to O (M) (Y) = V$
42	8	simprd	$⊢ φ \to O (N) (Y) = W$
43	41 42	oveq12d	$⊢ φ \to O (M) (Y) \underset{˙}{+} O (N) (Y) = V \underset{˙}{+} W$
44	34 40 43	3eqtrd	$⊢ φ \to O (M \underset{˙}{✚} N) (Y) = V \underset{˙}{+} W$
45	21 44	jca	$⊢ φ \to (M \underset{˙}{✚} N \in U \land O (M \underset{˙}{✚} N) (Y) = V \underset{˙}{+} W)$

Metamath Proof Explorer

Theorem evl1addd

Proof