Theorem evlmulval

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

	Ref	Expression
Hypotheses	evlmulval.q	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
	evlmulval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
	evlmulval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlmulval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlmulval.g	⊢ ∙ = ( .r ‘ 𝑃 )
	evlmulval.f	⊢ · = ( .r ‘ 𝑆 )
	evlmulval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
	evlmulval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlmulval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
	evlmulval.m	⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
	evlmulval.n	⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
Assertion	evlmulval	⊢ ( 𝜑 → ( ( 𝑀 ∙ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 · 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlmulval.q	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2		evlmulval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
3		evlmulval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
4		evlmulval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		evlmulval.g	⊢ ∙ = ( .r ‘ 𝑃 )
6		evlmulval.f	⊢ · = ( .r ‘ 𝑆 )
7		evlmulval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
8		evlmulval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evlmulval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
10		evlmulval.m	⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
11		evlmulval.n	⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
12		eqid	⊢ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
13	1 3 2 12	evlrhm	⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ) → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
14	7 8 13	syl2anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
15		rhmrcl1	⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑃 ∈ Ring )
16	14 15	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
17	10	simpld	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
18	11	simpld	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
19	4 5 16 17 18	ringcld	⊢ ( 𝜑 → ( 𝑀 ∙ 𝑁 ) ∈ 𝐵 )
20		eqid	⊢ ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
21	4 5 20	rhmmul	⊢ ( ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) )
22	14 17 18 21	syl3anc	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) )
23		eqid	⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
24		ovexd	⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
25	4 23	rhmf	⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
26	14 25	syl	⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
27	26 17	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
28	26 18	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
29	12 23 8 24 27 28 6 20	pwsmulrval	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ( .r ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ∘f · ( 𝑄 ‘ 𝑁 ) ) )
30	22 29	eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ∘f · ( 𝑄 ‘ 𝑁 ) ) )
31	30	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ∘f · ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) )
32	12 3 23 8 24 27	pwselbas	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
33	32	ffnd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) Fn ( 𝐾 ↑m 𝐼 ) )
34	12 3 23 8 24 28	pwselbas	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
35	34	ffnd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) Fn ( 𝐾 ↑m 𝐼 ) )
36		fnfvof	⊢ ( ( ( ( 𝑄 ‘ 𝑀 ) Fn ( 𝐾 ↑m 𝐼 ) ∧ ( 𝑄 ‘ 𝑁 ) Fn ( 𝐾 ↑m 𝐼 ) ) ∧ ( ( 𝐾 ↑m 𝐼 ) ∈ V ∧ 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) ) → ( ( ( 𝑄 ‘ 𝑀 ) ∘f · ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) )
37	33 35 24 9 36	syl22anc	⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝑀 ) ∘f · ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) )
38	10	simprd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 )
39	11	simprd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 )
40	38 39	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) = ( 𝑉 · 𝑊 ) )
41	31 37 40	3eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 · 𝑊 ) )
42	19 41	jca	⊢ ( 𝜑 → ( ( 𝑀 ∙ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 ∙ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 · 𝑊 ) ) )