Step |
Hyp |
Ref |
Expression |
1 |
|
evlspw.q |
⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) |
2 |
|
evlspw.w |
⊢ 𝑊 = ( 𝐼 mPoly 𝑈 ) |
3 |
|
evlspw.g |
⊢ 𝐺 = ( mulGrp ‘ 𝑊 ) |
4 |
|
evlspw.e |
⊢ ↑ = ( .g ‘ 𝐺 ) |
5 |
|
evlspw.u |
⊢ 𝑈 = ( 𝑆 ↾s 𝑅 ) |
6 |
|
evlspw.p |
⊢ 𝑃 = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) |
7 |
|
evlspw.h |
⊢ 𝐻 = ( mulGrp ‘ 𝑃 ) |
8 |
|
evlspw.k |
⊢ 𝐾 = ( Base ‘ 𝑆 ) |
9 |
|
evlspw.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
10 |
|
evlspw.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
11 |
|
evlspw.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
12 |
|
evlspw.r |
⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) |
13 |
|
evlspw.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
14 |
|
evlspw.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
15 |
1 2 5 6 8
|
evlsrhm |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) ) |
16 |
10 11 12 15
|
syl3anc |
⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) ) |
17 |
3 7
|
rhmmhm |
⊢ ( 𝑄 ∈ ( 𝑊 RingHom 𝑃 ) → 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) ) |
18 |
16 17
|
syl |
⊢ ( 𝜑 → 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) ) |
19 |
3 9
|
mgpbas |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
20 |
|
eqid |
⊢ ( .g ‘ 𝐻 ) = ( .g ‘ 𝐻 ) |
21 |
19 4 20
|
mhmmulg |
⊢ ( ( 𝑄 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ 𝐻 ) ( 𝑄 ‘ 𝑋 ) ) ) |
22 |
18 13 14 21
|
syl3anc |
⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ 𝐻 ) ( 𝑄 ‘ 𝑋 ) ) ) |