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 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
15 14 5 mgpbas 
 |-  B = ( Base ` ( mulGrp ` P ) )
16 eqid 
 |-  ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) )
17 1 2 3 16 4 evlsrhm 
 |-  ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
18 6 7 8 17 syl3anc 
 |-  ( ph -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
19 rhmrcl1 
 |-  ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> P e. Ring )
20 14 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
21 18 19 20 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
22 10 simpld 
 |-  ( ph -> M e. B )
23 15 11 21 13 22 mulgnn0cld 
 |-  ( ph -> ( N .xb M ) e. B )
24 eqid 
 |-  ( mulGrp ` ( S ^s ( K ^m I ) ) ) = ( mulGrp ` ( S ^s ( K ^m I ) ) )
25 1 2 14 11 3 16 24 4 5 6 7 8 13 22 evlspw 
 |-  ( ph -> ( Q ` ( N .xb M ) ) = ( N ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( Q ` M ) ) )
26 25 fveq1d 
 |-  ( ph -> ( ( Q ` ( N .xb M ) ) ` A ) = ( ( N ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( Q ` M ) ) ` A ) )
27 eqid 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) )
28 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
29 eqid 
 |-  ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) = ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) )
30 7 crngringd 
 |-  ( ph -> S e. Ring )
31 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
32 5 27 rhmf 
 |-  ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) )
33 18 32 syl 
 |-  ( ph -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) )
34 33 22 ffvelcdmd 
 |-  ( ph -> ( Q ` M ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
35 16 27 24 28 29 12 30 31 13 34 9 pwsexpg 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` ( S ^s ( K ^m I ) ) ) ) ( Q ` M ) ) ` A ) = ( N .^ ( ( Q ` M ) ` A ) ) )
36 10 simprd 
 |-  ( ph -> ( ( Q ` M ) ` A ) = V )
37 36 oveq2d 
 |-  ( ph -> ( N .^ ( ( Q ` M ) ` A ) ) = ( N .^ V ) )
38 26 35 37 3eqtrd 
 |-  ( ph -> ( ( Q ` ( N .xb M ) ) ` A ) = ( N .^ V ) )
39 23 38 jca 
 |-  ( ph -> ( ( N .xb M ) e. B /\ ( ( Q ` ( N .xb M ) ) ` A ) = ( N .^ V ) ) )