evlsaddval

Description: Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsaddval.q	$⊢ Q = (I evalSub S) (R)$
	evlsaddval.p	$⊢ P = I mPoly U$
	evlsaddval.u	$⊢ U = S ↾_{𝑠} R$
	evlsaddval.k	$⊢ K = {Base}_{S}$
	evlsaddval.b	$⊢ B = {Base}_{P}$
	evlsaddval.i	$⊢ φ \to I \in Z$
	evlsaddval.s	$⊢ φ \to S \in CRing$
	evlsaddval.r	$⊢ φ \to R \in SubRing (S)$
	evlsaddval.a	$⊢ φ \to A \in (K^{I})$
	evlsaddval.m	$⊢ φ \to (M \in B \land Q (M) (A) = V)$
	evlsaddval.n	$⊢ φ \to (N \in B \land Q (N) (A) = W)$
	evlsaddval.g	$⊢ \underset{˙}{✚} = +_{P}$
	evlsaddval.f	$⊢ \underset{˙}{+} = +_{S}$
Assertion	evlsaddval	$⊢ φ \to (M \underset{˙}{✚} N \in B \land Q (M \underset{˙}{✚} N) (A) = V \underset{˙}{+} W)$

Proof

Step	Hyp	Ref	Expression
1		evlsaddval.q	$⊢ Q = (I evalSub S) (R)$
2		evlsaddval.p	$⊢ P = I mPoly U$
3		evlsaddval.u	$⊢ U = S ↾_{𝑠} R$
4		evlsaddval.k	$⊢ K = {Base}_{S}$
5		evlsaddval.b	$⊢ B = {Base}_{P}$
6		evlsaddval.i	$⊢ φ \to I \in Z$
7		evlsaddval.s	$⊢ φ \to S \in CRing$
8		evlsaddval.r	$⊢ φ \to R \in SubRing (S)$
9		evlsaddval.a	$⊢ φ \to A \in (K^{I})$
10		evlsaddval.m	$⊢ φ \to (M \in B \land Q (M) (A) = V)$
11		evlsaddval.n	$⊢ φ \to (N \in B \land Q (N) (A) = W)$
12		evlsaddval.g	$⊢ \underset{˙}{✚} = +_{P}$
13		evlsaddval.f	$⊢ \underset{˙}{+} = +_{S}$
14		eqid	$⊢ S ↑_{𝑠} (K^{I}) = S ↑_{𝑠} (K^{I})$
15	1 2 3 14 4	evlsrhm	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to Q \in (P RingHom (S ↑_{𝑠} (K^{I})))$
16	6 7 8 15	syl3anc	$⊢ φ \to Q \in (P RingHom (S ↑_{𝑠} (K^{I})))$
17		rhmghm	$⊢ Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \to Q \in (P GrpHom (S ↑_{𝑠} (K^{I})))$
18	16 17	syl	$⊢ φ \to Q \in (P GrpHom (S ↑_{𝑠} (K^{I})))$
19		ghmgrp1	$⊢ Q \in (P GrpHom (S ↑_{𝑠} (K^{I}))) \to P \in Grp$
20	18 19	syl	$⊢ φ \to P \in Grp$
21	10	simpld	$⊢ φ \to M \in B$
22	11	simpld	$⊢ φ \to N \in B$
23	5 12	grpcl	$⊢ (P \in Grp \land M \in B \land N \in B) \to M \underset{˙}{✚} N \in B$
24	20 21 22 23	syl3anc	$⊢ φ \to M \underset{˙}{✚} N \in B$
25		eqid	$⊢ +_{(S ↑_{𝑠} (K^{I}))} = +_{(S ↑_{𝑠} (K^{I}))}$
26	5 12 25	ghmlin	$⊢ (Q \in (P GrpHom (S ↑_{𝑠} (K^{I}))) \land M \in B \land N \in B) \to Q (M \underset{˙}{✚} N) = Q (M) +_{(S ↑_{𝑠} (K^{I}))} Q (N)$
27	18 21 22 26	syl3anc	$⊢ φ \to Q (M \underset{˙}{✚} N) = Q (M) +_{(S ↑_{𝑠} (K^{I}))} Q (N)$
28		eqid	$⊢ {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} (K^{I}))}$
29		ovexd	$⊢ φ \to K^{I} \in V$
30	5 28	rhmf	$⊢ Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \to Q : B ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
31	16 30	syl	$⊢ φ \to Q : B ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
32	31 21	ffvelrnd	$⊢ φ \to Q (M) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
33	31 22	ffvelrnd	$⊢ φ \to Q (N) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
34	14 28 7 29 32 33 13 25	pwsplusgval	$⊢ φ \to Q (M) +_{(S ↑_{𝑠} (K^{I}))} Q (N) = Q (M) {\underset{˙}{+}}_{f} Q (N)$
35	27 34	eqtrd	$⊢ φ \to Q (M \underset{˙}{✚} N) = Q (M) {\underset{˙}{+}}_{f} Q (N)$
36	35	fveq1d	$⊢ φ \to Q (M \underset{˙}{✚} N) (A) = (Q (M) {\underset{˙}{+}}_{f} Q (N)) (A)$
37	14 4 28 7 29 32	pwselbas	$⊢ φ \to Q (M) : K^{I} ⟶ K$
38	37	ffnd	$⊢ φ \to Q (M) Fn (K^{I})$
39	14 4 28 7 29 33	pwselbas	$⊢ φ \to Q (N) : K^{I} ⟶ K$
40	39	ffnd	$⊢ φ \to Q (N) Fn (K^{I})$
41		fnfvof	$⊢ ((Q (M) Fn (K^{I}) \land Q (N) Fn (K^{I})) \land (K^{I} \in V \land A \in (K^{I}))) \to (Q (M) {\underset{˙}{+}}_{f} Q (N)) (A) = Q (M) (A) \underset{˙}{+} Q (N) (A)$
42	38 40 29 9 41	syl22anc	$⊢ φ \to (Q (M) {\underset{˙}{+}}_{f} Q (N)) (A) = Q (M) (A) \underset{˙}{+} Q (N) (A)$
43	10	simprd	$⊢ φ \to Q (M) (A) = V$
44	11	simprd	$⊢ φ \to Q (N) (A) = W$
45	43 44	oveq12d	$⊢ φ \to Q (M) (A) \underset{˙}{+} Q (N) (A) = V \underset{˙}{+} W$
46	36 42 45	3eqtrd	$⊢ φ \to Q (M \underset{˙}{✚} N) (A) = V \underset{˙}{+} W$
47	24 46	jca	$⊢ φ \to (M \underset{˙}{✚} N \in B \land Q (M \underset{˙}{✚} N) (A) = V \underset{˙}{+} W)$

Metamath Proof Explorer

Theorem evlsaddval

Proof