Step |
Hyp |
Ref |
Expression |
1 |
|
evls1pw.q |
|- Q = ( S evalSub1 R ) |
2 |
|
evls1pw.u |
|- U = ( S |`s R ) |
3 |
|
evls1pw.w |
|- W = ( Poly1 ` U ) |
4 |
|
evls1pw.g |
|- G = ( mulGrp ` W ) |
5 |
|
evls1pw.k |
|- K = ( Base ` S ) |
6 |
|
evls1pw.b |
|- B = ( Base ` W ) |
7 |
|
evls1pw.e |
|- .^ = ( .g ` G ) |
8 |
|
evls1pw.s |
|- ( ph -> S e. CRing ) |
9 |
|
evls1pw.r |
|- ( ph -> R e. ( SubRing ` S ) ) |
10 |
|
evls1pw.n |
|- ( ph -> N e. NN0 ) |
11 |
|
evls1pw.x |
|- ( ph -> X e. B ) |
12 |
|
eqid |
|- ( S ^s K ) = ( S ^s K ) |
13 |
1 5 12 2 3
|
evls1rhm |
|- ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) ) |
14 |
8 9 13
|
syl2anc |
|- ( ph -> Q e. ( W RingHom ( S ^s K ) ) ) |
15 |
|
eqid |
|- ( mulGrp ` ( S ^s K ) ) = ( mulGrp ` ( S ^s K ) ) |
16 |
4 15
|
rhmmhm |
|- ( Q e. ( W RingHom ( S ^s K ) ) -> Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) ) |
17 |
14 16
|
syl |
|- ( ph -> Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) ) |
18 |
4 6
|
mgpbas |
|- B = ( Base ` G ) |
19 |
|
eqid |
|- ( .g ` ( mulGrp ` ( S ^s K ) ) ) = ( .g ` ( mulGrp ` ( S ^s K ) ) ) |
20 |
18 7 19
|
mhmmulg |
|- ( ( Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) /\ N e. NN0 /\ X e. B ) -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) ) |
21 |
17 10 11 20
|
syl3anc |
|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) ) |