Step |
Hyp |
Ref |
Expression |
1 |
|
evl1varpw.q |
|- Q = ( eval1 ` R ) |
2 |
|
evl1varpw.w |
|- W = ( Poly1 ` R ) |
3 |
|
evl1varpw.g |
|- G = ( mulGrp ` W ) |
4 |
|
evl1varpw.x |
|- X = ( var1 ` R ) |
5 |
|
evl1varpw.b |
|- B = ( Base ` R ) |
6 |
|
evl1varpw.e |
|- .^ = ( .g ` G ) |
7 |
|
evl1varpw.r |
|- ( ph -> R e. CRing ) |
8 |
|
evl1varpw.n |
|- ( ph -> N e. NN0 ) |
9 |
1 5
|
evl1fval1 |
|- Q = ( R evalSub1 B ) |
10 |
9
|
a1i |
|- ( ph -> Q = ( R evalSub1 B ) ) |
11 |
2
|
fveq2i |
|- ( mulGrp ` W ) = ( mulGrp ` ( Poly1 ` R ) ) |
12 |
3 11
|
eqtri |
|- G = ( mulGrp ` ( Poly1 ` R ) ) |
13 |
12
|
fveq2i |
|- ( .g ` G ) = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) |
14 |
6 13
|
eqtri |
|- .^ = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) |
15 |
5
|
ressid |
|- ( R e. CRing -> ( R |`s B ) = R ) |
16 |
7 15
|
syl |
|- ( ph -> ( R |`s B ) = R ) |
17 |
16
|
eqcomd |
|- ( ph -> R = ( R |`s B ) ) |
18 |
17
|
fveq2d |
|- ( ph -> ( Poly1 ` R ) = ( Poly1 ` ( R |`s B ) ) ) |
19 |
18
|
fveq2d |
|- ( ph -> ( mulGrp ` ( Poly1 ` R ) ) = ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) |
20 |
19
|
fveq2d |
|- ( ph -> ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ) |
21 |
14 20
|
eqtrid |
|- ( ph -> .^ = ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ) |
22 |
|
eqidd |
|- ( ph -> N = N ) |
23 |
17
|
fveq2d |
|- ( ph -> ( var1 ` R ) = ( var1 ` ( R |`s B ) ) ) |
24 |
4 23
|
eqtrid |
|- ( ph -> X = ( var1 ` ( R |`s B ) ) ) |
25 |
21 22 24
|
oveq123d |
|- ( ph -> ( N .^ X ) = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ( var1 ` ( R |`s B ) ) ) ) |
26 |
10 25
|
fveq12d |
|- ( ph -> ( Q ` ( N .^ X ) ) = ( ( R evalSub1 B ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ( var1 ` ( R |`s B ) ) ) ) ) |
27 |
|
eqid |
|- ( R evalSub1 B ) = ( R evalSub1 B ) |
28 |
|
eqid |
|- ( R |`s B ) = ( R |`s B ) |
29 |
|
eqid |
|- ( Poly1 ` ( R |`s B ) ) = ( Poly1 ` ( R |`s B ) ) |
30 |
|
eqid |
|- ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) = ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) |
31 |
|
eqid |
|- ( var1 ` ( R |`s B ) ) = ( var1 ` ( R |`s B ) ) |
32 |
|
eqid |
|- ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) |
33 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
34 |
5
|
subrgid |
|- ( R e. Ring -> B e. ( SubRing ` R ) ) |
35 |
7 33 34
|
3syl |
|- ( ph -> B e. ( SubRing ` R ) ) |
36 |
27 28 29 30 31 5 32 7 35 8
|
evls1varpw |
|- ( ph -> ( ( R evalSub1 B ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ( var1 ` ( R |`s B ) ) ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( ( R evalSub1 B ) ` ( var1 ` ( R |`s B ) ) ) ) ) |
37 |
9
|
eqcomi |
|- ( R evalSub1 B ) = Q |
38 |
37
|
a1i |
|- ( ph -> ( R evalSub1 B ) = Q ) |
39 |
24
|
eqcomd |
|- ( ph -> ( var1 ` ( R |`s B ) ) = X ) |
40 |
38 39
|
fveq12d |
|- ( ph -> ( ( R evalSub1 B ) ` ( var1 ` ( R |`s B ) ) ) = ( Q ` X ) ) |
41 |
40
|
oveq2d |
|- ( ph -> ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( ( R evalSub1 B ) ` ( var1 ` ( R |`s B ) ) ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) ) |
42 |
26 36 41
|
3eqtrd |
|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) ) |