| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evlsmhpvvval.q |
⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) |
| 2 |
|
evlsmhpvvval.p |
⊢ 𝐻 = ( 𝐼 mHomP 𝑈 ) |
| 3 |
|
evlsmhpvvval.u |
⊢ 𝑈 = ( 𝑆 ↾s 𝑅 ) |
| 4 |
|
evlsmhpvvval.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
| 5 |
|
evlsmhpvvval.g |
⊢ 𝐺 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } |
| 6 |
|
evlsmhpvvval.k |
⊢ 𝐾 = ( Base ‘ 𝑆 ) |
| 7 |
|
evlsmhpvvval.m |
⊢ 𝑀 = ( mulGrp ‘ 𝑆 ) |
| 8 |
|
evlsmhpvvval.w |
⊢ ↑ = ( .g ‘ 𝑀 ) |
| 9 |
|
evlsmhpvvval.x |
⊢ · = ( .r ‘ 𝑆 ) |
| 10 |
|
evlsmhpvvval.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
| 11 |
|
evlsmhpvvval.r |
⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) |
| 12 |
|
evlsmhpvvval.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 13 |
|
evlsmhpvvval.a |
⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) |
| 14 |
|
eqid |
⊢ ( 𝐼 mPoly 𝑈 ) = ( 𝐼 mPoly 𝑈 ) |
| 15 |
|
eqid |
⊢ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) |
| 16 |
|
reldmmhp |
⊢ Rel dom mHomP |
| 17 |
16 2 12
|
elfvov1 |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
| 18 |
2 14 15 12
|
mhpmpl |
⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ) |
| 19 |
1 14 15 3 4 6 7 8 9 17 10 11 18 13
|
evlsvvval |
⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) ) |
| 20 |
|
eqid |
⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) |
| 21 |
10
|
crngringd |
⊢ ( 𝜑 → 𝑆 ∈ Ring ) |
| 22 |
21
|
ringcmnd |
⊢ ( 𝜑 → 𝑆 ∈ CMnd ) |
| 23 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
| 24 |
4 23
|
rabex2 |
⊢ 𝐷 ∈ V |
| 25 |
24
|
a1i |
⊢ ( 𝜑 → 𝐷 ∈ V ) |
| 26 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ Ring ) |
| 27 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
| 28 |
14 27 15 4 18
|
mplelf |
⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ( Base ‘ 𝑈 ) ) |
| 29 |
3
|
subrgbas |
⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) ) |
| 30 |
6
|
subrgss |
⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 ) |
| 31 |
29 30
|
eqsstrrd |
⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( Base ‘ 𝑈 ) ⊆ 𝐾 ) |
| 32 |
11 31
|
syl |
⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ⊆ 𝐾 ) |
| 33 |
28 32
|
fssd |
⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐾 ) |
| 34 |
33
|
ffvelcdmda |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐾 ) |
| 35 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐼 ∈ V ) |
| 36 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑆 ∈ CRing ) |
| 37 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) |
| 38 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐷 ) |
| 39 |
4 6 7 8 35 36 37 38
|
evlsvvvallem |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ 𝐾 ) |
| 40 |
6 9 26 34 39
|
ringcld |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ∈ 𝐾 ) |
| 41 |
40
|
fmpttd |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) : 𝐷 ⟶ 𝐾 ) |
| 42 |
3 20
|
subrg0 |
⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) ) |
| 43 |
11 42
|
syl |
⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) ) |
| 44 |
43
|
oveq2d |
⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑆 ) ) = ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ) |
| 45 |
|
eqid |
⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 ) |
| 46 |
2 45 4 12
|
mhpdeg |
⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
| 47 |
46 5
|
sseqtrrdi |
⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑈 ) ) ⊆ 𝐺 ) |
| 48 |
44 47
|
eqsstrd |
⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑆 ) ) ⊆ 𝐺 ) |
| 49 |
|
fvexd |
⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V ) |
| 50 |
33 48 25 49
|
suppssr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 0g ‘ 𝑆 ) ) |
| 51 |
50
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) |
| 52 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → 𝑆 ∈ Ring ) |
| 53 |
|
eldifi |
⊢ ( 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) → 𝑏 ∈ 𝐷 ) |
| 54 |
53 39
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ 𝐾 ) |
| 55 |
6 9 20 52 54
|
ringlzd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( ( 0g ‘ 𝑆 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑆 ) ) |
| 56 |
51 55
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝐷 ∖ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( 0g ‘ 𝑆 ) ) |
| 57 |
56 25
|
suppss2 |
⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) supp ( 0g ‘ 𝑆 ) ) ⊆ 𝐺 ) |
| 58 |
4 14 3 15 6 7 8 9 17 10 11 18 13
|
evlsvvvallem2 |
⊢ ( 𝜑 → ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) finSupp ( 0g ‘ 𝑆 ) ) |
| 59 |
6 20 22 25 41 57 58
|
gsumres |
⊢ ( 𝜑 → ( 𝑆 Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ↾ 𝐺 ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) ) |
| 60 |
5
|
ssrab3 |
⊢ 𝐺 ⊆ 𝐷 |
| 61 |
60
|
a1i |
⊢ ( 𝜑 → 𝐺 ⊆ 𝐷 ) |
| 62 |
61
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ↾ 𝐺 ) = ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) |
| 63 |
62
|
oveq2d |
⊢ ( 𝜑 → ( 𝑆 Σg ( ( 𝑏 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ↾ 𝐺 ) ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) ) |
| 64 |
19 59 63
|
3eqtr2d |
⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝐴 ) = ( 𝑆 Σg ( 𝑏 ∈ 𝐺 ↦ ( ( 𝐹 ‘ 𝑏 ) · ( 𝑀 Σg ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑏 ‘ 𝑖 ) ↑ ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) ) ) |