Metamath Proof Explorer

Theorem evlsexpval

Description: Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses evlsaddval.q 
|- Q = ( ( I evalSub S ) ` R )
evlsaddval.p 
|- P = ( I mPoly U )
evlsaddval.u 
|- U = ( S |`s R )
evlsaddval.k 
|- K = ( Base ` S )
evlsaddval.b 
|- B = ( Base ` P )
evlsaddval.i 
|- ( ph -> I e. Z )
evlsaddval.s 
|- ( ph -> S e. CRing )
evlsaddval.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsaddval.a 
|- ( ph -> A e. ( K ^m I ) )
evlsaddval.m 
|- ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) )
evlsexpval.g 
|- .xb = ( .g ` ( mulGrp ` P ) )
evlsexpval.f 
|- .^ = ( .g ` ( mulGrp ` S ) )
evlsexpval.n 
|- ( ph -> N e. NN0 )
Assertion evlsexpval 
|- ( ph -> ( ( N .xb M ) e. B /\ ( ( Q ` ( N .xb M ) ) ` A ) = ( N .^ V ) ) )

Proof

Step Hyp Ref Expression
1 evlsaddval.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsaddval.p 
 |-  P = ( I mPoly U )
3 evlsaddval.u 
 |-  U = ( S |`s R )
4 evlsaddval.k 
 |-  K = ( Base ` S )
5 evlsaddval.b 
 |-  B = ( Base ` P )
6 evlsaddval.i 
 |-  ( ph -> I e. Z )
7 evlsaddval.s 
 |-  ( ph -> S e. CRing )
8 evlsaddval.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
9 evlsaddval.a 
 |-  ( ph -> A e. ( K ^m I ) )
10 evlsaddval.m 
 |-  ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) )
11 evlsexpval.g 
 |-  .xb = ( .g ` ( mulGrp ` P ) )
12 evlsexpval.f 
 |-  .^ = ( .g ` ( mulGrp ` S ) )
13 evlsexpval.n 
 |-  ( ph -> N e. NN0 )
14 eqid 
 |-  ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) )
15 1 2 3 14 4 evlsrhm 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
16 6 7 8 15 syl3anc 
 |-  ( ph -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
17 rhmrcl1 
 |-  ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> P e. Ring )
18 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
19 18 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
20 16 17 19 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
21 10 simpld 
 |-  ( ph -> M e. B )
22 18 5 mgpbas 
 |-  B = ( Base ` ( mulGrp ` P ) )
23 22 11 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ N e. NN0 /\ M e. B ) -> ( N .xb M ) e. B )
24 20 13 21 23 syl3anc 
 |-  ( ph -> ( N .xb M ) e. B )
25 eqid 
 |-  ( mulGrp ` ( S ^s ( K ^m I ) ) ) = ( mulGrp ` ( S ^s ( K ^m I ) ) )
26 1 2 18 11 3 14 25 4 5 6 7 8 13 21 evlspw 
 |-  ( ph -> ( Q ` ( N .xb M ) ) = ( N ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( Q ` M ) ) )
27 26 fveq1d 
 |-  ( ph -> ( ( Q ` ( N .xb M ) ) ` A ) = ( ( N ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( Q ` M ) ) ` A ) )
28 eqid 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) )
29 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
30 eqid 
 |-  ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) = ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) )
31 7 crngringd 
 |-  ( ph -> S e. Ring )
32 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
33 5 28 rhmf 
 |-  ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) )
34 16 33 syl 
 |-  ( ph -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) )
35 34 21 ffvelrnd 
 |-  ( ph -> ( Q ` M ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
36 14 28 25 29 30 12 31 32 13 35 9 pwsexpg 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( Q ` M ) ) ` A ) = ( N .^ ( ( Q ` M ) ` A ) ) )
37 10 simprd 
 |-  ( ph -> ( ( Q ` M ) ` A ) = V )
38 37 oveq2d 
 |-  ( ph -> ( N .^ ( ( Q ` M ) ` A ) ) = ( N .^ V ) )
39 27 36 38 3eqtrd 
 |-  ( ph -> ( ( Q ` ( N .xb M ) ) ` A ) = ( N .^ V ) )
40 24 39 jca 
 |-  ( ph -> ( ( N .xb M ) e. B /\ ( ( Q ` ( N .xb M ) ) ` A ) = ( N .^ V ) ) )