This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1expd

Description: Univariate polynomial evaluation builder for an exponential. See also evl1expd . (Contributed by Thierry Arnoux, 24-Jan-2025)

Ref Expression
Hypotheses evls1expd.q 
|- Q = ( S evalSub1 R )
evls1expd.k 
|- K = ( Base ` S )
evls1expd.w 
|- W = ( Poly1 ` U )
evls1expd.u 
|- U = ( S |`s R )
evls1expd.b 
|- B = ( Base ` W )
evls1expd.s 
|- ( ph -> S e. CRing )
evls1expd.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1expd.1 
|- ./\ = ( .g ` ( mulGrp ` W ) )
evls1expd.2 
|- .^ = ( .g ` ( mulGrp ` S ) )
evls1expd.n 
|- ( ph -> N e. NN0 )
evls1expd.m 
|- ( ph -> M e. B )
evls1expd.c 
|- ( ph -> C e. K )
Assertion evls1expd 
|- ( ph -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) )

Proof

Step Hyp Ref Expression
1 evls1expd.q 
 |-  Q = ( S evalSub1 R )
2 evls1expd.k 
 |-  K = ( Base ` S )
3 evls1expd.w 
 |-  W = ( Poly1 ` U )
4 evls1expd.u 
 |-  U = ( S |`s R )
5 evls1expd.b 
 |-  B = ( Base ` W )
6 evls1expd.s 
 |-  ( ph -> S e. CRing )
7 evls1expd.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
8 evls1expd.1 
 |-  ./\ = ( .g ` ( mulGrp ` W ) )
9 evls1expd.2 
 |-  .^ = ( .g ` ( mulGrp ` S ) )
10 evls1expd.n 
 |-  ( ph -> N e. NN0 )
11 evls1expd.m 
 |-  ( ph -> M e. B )
12 evls1expd.c 
 |-  ( ph -> C e. K )
13 eqid 
 |-  ( mulGrp ` W ) = ( mulGrp ` W )
14 1 4 3 13 2 5 8 6 7 10 11 evls1pw 
 |-  ( ph -> ( Q ` ( N ./\ M ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` M ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` M ) ) ` C ) )
16 eqid 
 |-  ( S ^s K ) = ( S ^s K )
17 eqid 
 |-  ( Base ` ( S ^s K ) ) = ( Base ` ( S ^s K ) )
18 eqid 
 |-  ( mulGrp ` ( S ^s K ) ) = ( mulGrp ` ( S ^s K ) )
19 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
20 eqid 
 |-  ( .g ` ( mulGrp ` ( S ^s K ) ) ) = ( .g ` ( mulGrp ` ( S ^s K ) ) )
21 6 crngringd 
 |-  ( ph -> S e. Ring )
22 2 fvexi 
 |-  K e. _V
23 22 a1i 
 |-  ( ph -> K e. _V )
24 1 2 16 4 3 evls1rhm 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) )
25 6 7 24 syl2anc 
 |-  ( ph -> Q e. ( W RingHom ( S ^s K ) ) )
26 5 17 rhmf 
 |-  ( Q e. ( W RingHom ( S ^s K ) ) -> Q : B --> ( Base ` ( S ^s K ) ) )
27 25 26 syl 
 |-  ( ph -> Q : B --> ( Base ` ( S ^s K ) ) )
28 27 11 ffvelcdmd 
 |-  ( ph -> ( Q ` M ) e. ( Base ` ( S ^s K ) ) )
29 16 17 18 19 20 9 21 23 10 28 12 pwsexpg 
 |-  ( ph -> ( ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) )
30 15 29 eqtrd 
 |-  ( ph -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) )