evlsmulval

Description: Polynomial evaluation builder for multiplication. (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)$
	evlsmulval.g	$⊢ \underset{˙}{∙} = \cdot_{P}$
	evlsmulval.f	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
Assertion	evlsmulval	$⊢ φ \to (M \underset{˙}{∙} N \in B \land Q (M \underset{˙}{∙} N) (A) = V \underset{˙}{\cdot} 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		evlsmulval.g	$⊢ \underset{˙}{∙} = \cdot_{P}$
13		evlsmulval.f	$⊢ \underset{˙}{\cdot} = \cdot_{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		rhmrcl1	$⊢ Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \to P \in Ring$
18	16 17	syl	$⊢ φ \to P \in Ring$
19	10	simpld	$⊢ φ \to M \in B$
20	11	simpld	$⊢ φ \to N \in B$
21	5 12	ringcl	$⊢ (P \in Ring \land M \in B \land N \in B) \to M \underset{˙}{∙} N \in B$
22	18 19 20 21	syl3anc	$⊢ φ \to M \underset{˙}{∙} N \in B$
23		eqid	$⊢ \cdot_{(S ↑_{𝑠} (K^{I}))} = \cdot_{(S ↑_{𝑠} (K^{I}))}$
24	5 12 23	rhmmul	$⊢ (Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \land M \in B \land N \in B) \to Q (M \underset{˙}{∙} N) = Q (M) \cdot_{(S ↑_{𝑠} (K^{I}))} Q (N)$
25	16 19 20 24	syl3anc	$⊢ φ \to Q (M \underset{˙}{∙} N) = Q (M) \cdot_{(S ↑_{𝑠} (K^{I}))} Q (N)$
26		eqid	$⊢ {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} (K^{I}))}$
27		ovexd	$⊢ φ \to K^{I} \in V$
28	5 26	rhmf	$⊢ Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \to Q : B ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
29	16 28	syl	$⊢ φ \to Q : B ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
30	29 19	ffvelrnd	$⊢ φ \to Q (M) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
31	29 20	ffvelrnd	$⊢ φ \to Q (N) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
32	14 26 7 27 30 31 13 23	pwsmulrval	$⊢ φ \to Q (M) \cdot_{(S ↑_{𝑠} (K^{I}))} Q (N) = Q (M) {\underset{˙}{\cdot}}_{f} Q (N)$
33	25 32	eqtrd	$⊢ φ \to Q (M \underset{˙}{∙} N) = Q (M) {\underset{˙}{\cdot}}_{f} Q (N)$
34	33	fveq1d	$⊢ φ \to Q (M \underset{˙}{∙} N) (A) = (Q (M) {\underset{˙}{\cdot}}_{f} Q (N)) (A)$
35	14 4 26 7 27 30	pwselbas	$⊢ φ \to Q (M) : K^{I} ⟶ K$
36	35	ffnd	$⊢ φ \to Q (M) Fn (K^{I})$
37	14 4 26 7 27 31	pwselbas	$⊢ φ \to Q (N) : K^{I} ⟶ K$
38	37	ffnd	$⊢ φ \to Q (N) Fn (K^{I})$
39		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{˙}{\cdot}}_{f} Q (N)) (A) = Q (M) (A) \underset{˙}{\cdot} Q (N) (A)$
40	36 38 27 9 39	syl22anc	$⊢ φ \to (Q (M) {\underset{˙}{\cdot}}_{f} Q (N)) (A) = Q (M) (A) \underset{˙}{\cdot} Q (N) (A)$
41	10	simprd	$⊢ φ \to Q (M) (A) = V$
42	11	simprd	$⊢ φ \to Q (N) (A) = W$
43	41 42	oveq12d	$⊢ φ \to Q (M) (A) \underset{˙}{\cdot} Q (N) (A) = V \underset{˙}{\cdot} W$
44	34 40 43	3eqtrd	$⊢ φ \to Q (M \underset{˙}{∙} N) (A) = V \underset{˙}{\cdot} W$
45	22 44	jca	$⊢ φ \to (M \underset{˙}{∙} N \in B \land Q (M \underset{˙}{∙} N) (A) = V \underset{˙}{\cdot} W)$

Metamath Proof Explorer

Theorem evlsmulval

Proof