evlmulval

Description: Polynomial evaluation builder for multiplication. (Contributed by SN, 18-Feb-2025)

	Ref	Expression
Hypotheses	evlmulval.q	$⊢ Q = I eval S$
	evlmulval.p	$⊢ P = I mPoly S$
	evlmulval.k	$⊢ K = {Base}_{S}$
	evlmulval.b	$⊢ B = {Base}_{P}$
	evlmulval.g	$⊢ \underset{˙}{∙} = \cdot_{P}$
	evlmulval.f	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	evlmulval.i	$⊢ φ \to I \in Z$
	evlmulval.s	$⊢ φ \to S \in CRing$
	evlmulval.a	$⊢ φ \to A \in (K^{I})$
	evlmulval.m	$⊢ φ \to (M \in B \land Q (M) (A) = V)$
	evlmulval.n	$⊢ φ \to (N \in B \land Q (N) (A) = W)$
Assertion	evlmulval	$⊢ φ \to (M \underset{˙}{∙} N \in B \land Q (M \underset{˙}{∙} N) (A) = V \underset{˙}{\cdot} W)$

Proof

Step	Hyp	Ref	Expression
1		evlmulval.q	$⊢ Q = I eval S$
2		evlmulval.p	$⊢ P = I mPoly S$
3		evlmulval.k	$⊢ K = {Base}_{S}$
4		evlmulval.b	$⊢ B = {Base}_{P}$
5		evlmulval.g	$⊢ \underset{˙}{∙} = \cdot_{P}$
6		evlmulval.f	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
7		evlmulval.i	$⊢ φ \to I \in Z$
8		evlmulval.s	$⊢ φ \to S \in CRing$
9		evlmulval.a	$⊢ φ \to A \in (K^{I})$
10		evlmulval.m	$⊢ φ \to (M \in B \land Q (M) (A) = V)$
11		evlmulval.n	$⊢ φ \to (N \in B \land Q (N) (A) = W)$
12		eqid	$⊢ S ↑_{𝑠} (K^{I}) = S ↑_{𝑠} (K^{I})$
13	1 3 2 12	evlrhm	$⊢ (I \in Z \land S \in CRing) \to Q \in (P RingHom (S ↑_{𝑠} (K^{I})))$
14	7 8 13	syl2anc	$⊢ φ \to Q \in (P RingHom (S ↑_{𝑠} (K^{I})))$
15		rhmrcl1	$⊢ Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \to P \in Ring$
16	14 15	syl	$⊢ φ \to P \in Ring$
17	10	simpld	$⊢ φ \to M \in B$
18	11	simpld	$⊢ φ \to N \in B$
19	4 5 16 17 18	ringcld	$⊢ φ \to M \underset{˙}{∙} N \in B$
20		eqid	$⊢ \cdot_{(S ↑_{𝑠} (K^{I}))} = \cdot_{(S ↑_{𝑠} (K^{I}))}$
21	4 5 20	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)$
22	14 17 18 21	syl3anc	$⊢ φ \to Q (M \underset{˙}{∙} N) = Q (M) \cdot_{(S ↑_{𝑠} (K^{I}))} Q (N)$
23		eqid	$⊢ {Base}_{(S ↑_{𝑠} (K^{I}))} = {Base}_{(S ↑_{𝑠} (K^{I}))}$
24		ovexd	$⊢ φ \to K^{I} \in V$
25	4 23	rhmf	$⊢ Q \in (P RingHom (S ↑_{𝑠} (K^{I}))) \to Q : B ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
26	14 25	syl	$⊢ φ \to Q : B ⟶ {Base}_{(S ↑_{𝑠} (K^{I}))}$
27	26 17	ffvelcdmd	$⊢ φ \to Q (M) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
28	26 18	ffvelcdmd	$⊢ φ \to Q (N) \in {Base}_{(S ↑_{𝑠} (K^{I}))}$
29	12 23 8 24 27 28 6 20	pwsmulrval	$⊢ φ \to Q (M) \cdot_{(S ↑_{𝑠} (K^{I}))} Q (N) = Q (M) {\underset{˙}{\cdot}}_{f} Q (N)$
30	22 29	eqtrd	$⊢ φ \to Q (M \underset{˙}{∙} N) = Q (M) {\underset{˙}{\cdot}}_{f} Q (N)$
31	30	fveq1d	$⊢ φ \to Q (M \underset{˙}{∙} N) (A) = (Q (M) {\underset{˙}{\cdot}}_{f} Q (N)) (A)$
32	12 3 23 8 24 27	pwselbas	$⊢ φ \to Q (M) : K^{I} ⟶ K$
33	32	ffnd	$⊢ φ \to Q (M) Fn (K^{I})$
34	12 3 23 8 24 28	pwselbas	$⊢ φ \to Q (N) : K^{I} ⟶ K$
35	34	ffnd	$⊢ φ \to Q (N) Fn (K^{I})$
36		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)$
37	33 35 24 9 36	syl22anc	$⊢ φ \to (Q (M) {\underset{˙}{\cdot}}_{f} Q (N)) (A) = Q (M) (A) \underset{˙}{\cdot} Q (N) (A)$
38	10	simprd	$⊢ φ \to Q (M) (A) = V$
39	11	simprd	$⊢ φ \to Q (N) (A) = W$
40	38 39	oveq12d	$⊢ φ \to Q (M) (A) \underset{˙}{\cdot} Q (N) (A) = V \underset{˙}{\cdot} W$
41	31 37 40	3eqtrd	$⊢ φ \to Q (M \underset{˙}{∙} N) (A) = V \underset{˙}{\cdot} W$
42	19 41	jca	$⊢ φ \to (M \underset{˙}{∙} N \in B \land Q (M \underset{˙}{∙} N) (A) = V \underset{˙}{\cdot} W)$

Metamath Proof Explorer

Theorem evlmulval

Proof