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