Metamath Proof Explorer

Theorem evl1expd

Description: Polynomial evaluation builder for an exponential. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1addd.q 
|- O = ( eval1 ` R )
evl1addd.p 
|- P = ( Poly1 ` R )
evl1addd.b 
|- B = ( Base ` R )
evl1addd.u 
|- U = ( Base ` P )
evl1addd.1 
|- ( ph -> R e. CRing )
evl1addd.2 
|- ( ph -> Y e. B )
evl1addd.3 
|- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )
evl1expd.f 
|- .xb = ( .g ` ( mulGrp ` P ) )
evl1expd.e 
|- .^ = ( .g ` ( mulGrp ` R ) )
evl1expd.4 
|- ( ph -> N e. NN0 )
Assertion evl1expd 
|- ( ph -> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .^ V ) ) )

Proof

Step Hyp Ref Expression
1 evl1addd.q 
 |-  O = ( eval1 ` R )
2 evl1addd.p 
 |-  P = ( Poly1 ` R )
3 evl1addd.b 
 |-  B = ( Base ` R )
4 evl1addd.u 
 |-  U = ( Base ` P )
5 evl1addd.1 
 |-  ( ph -> R e. CRing )
6 evl1addd.2 
 |-  ( ph -> Y e. B )
7 evl1addd.3 
 |-  ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )
8 evl1expd.f 
 |-  .xb = ( .g ` ( mulGrp ` P ) )
9 evl1expd.e 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
10 evl1expd.4 
 |-  ( ph -> N e. NN0 )
11 crngring 
 |-  ( R e. CRing -> R e. Ring )
12 5 11 syl 
 |-  ( ph -> R e. Ring )
13 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
14 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
15 14 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
16 12 13 15 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
17 7 simpld 
 |-  ( ph -> M e. U )
18 14 4 mgpbas 
 |-  U = ( Base ` ( mulGrp ` P ) )
19 18 8 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ N e. NN0 /\ M e. U ) -> ( N .xb M ) e. U )
20 16 10 17 19 syl3anc 
 |-  ( ph -> ( N .xb M ) e. U )
21 eqid 
 |-  ( R ^s B ) = ( R ^s B )
22 1 2 21 3 evl1rhm 
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s B ) ) )
23 5 22 syl 
 |-  ( ph -> O e. ( P RingHom ( R ^s B ) ) )
24 eqid 
 |-  ( mulGrp ` ( R ^s B ) ) = ( mulGrp ` ( R ^s B ) )
25 14 24 rhmmhm 
 |-  ( O e. ( P RingHom ( R ^s B ) ) -> O e. ( ( mulGrp ` P ) MndHom ( mulGrp ` ( R ^s B ) ) ) )
26 23 25 syl 
 |-  ( ph -> O e. ( ( mulGrp ` P ) MndHom ( mulGrp ` ( R ^s B ) ) ) )
27 eqid 
 |-  ( .g ` ( mulGrp ` ( R ^s B ) ) ) = ( .g ` ( mulGrp ` ( R ^s B ) ) )
28 18 8 27 mhmmulg 
 |-  ( ( O e. ( ( mulGrp ` P ) MndHom ( mulGrp ` ( R ^s B ) ) ) /\ N e. NN0 /\ M e. U ) -> ( O ` ( N .xb M ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( O ` M ) ) )
29 26 10 17 28 syl3anc 
 |-  ( ph -> ( O ` ( N .xb M ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( O ` M ) ) )
30 eqid 
 |-  ( .g ` ( ( mulGrp ` R ) ^s B ) ) = ( .g ` ( ( mulGrp ` R ) ^s B ) )
31 eqidd 
 |-  ( ph -> ( Base ` ( mulGrp ` ( R ^s B ) ) ) = ( Base ` ( mulGrp ` ( R ^s B ) ) ) )
32 3 fvexi 
 |-  B e. _V
33 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
34 eqid 
 |-  ( ( mulGrp ` R ) ^s B ) = ( ( mulGrp ` R ) ^s B )
35 eqid 
 |-  ( Base ` ( mulGrp ` ( R ^s B ) ) ) = ( Base ` ( mulGrp ` ( R ^s B ) ) )
36 eqid 
 |-  ( Base ` ( ( mulGrp ` R ) ^s B ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) )
37 eqid 
 |-  ( +g ` ( mulGrp ` ( R ^s B ) ) ) = ( +g ` ( mulGrp ` ( R ^s B ) ) )
38 eqid 
 |-  ( +g ` ( ( mulGrp ` R ) ^s B ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) )
39 21 33 34 24 35 36 37 38 pwsmgp 
 |-  ( ( R e. CRing /\ B e. _V ) -> ( ( Base ` ( mulGrp ` ( R ^s B ) ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) /\ ( +g ` ( mulGrp ` ( R ^s B ) ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) ) )
40 5 32 39 sylancl 
 |-  ( ph -> ( ( Base ` ( mulGrp ` ( R ^s B ) ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) /\ ( +g ` ( mulGrp ` ( R ^s B ) ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) ) )
41 40 simpld 
 |-  ( ph -> ( Base ` ( mulGrp ` ( R ^s B ) ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) )
42 ssv 
 |-  ( Base ` ( mulGrp ` ( R ^s B ) ) ) C_ _V
43 42 a1i 
 |-  ( ph -> ( Base ` ( mulGrp ` ( R ^s B ) ) ) C_ _V )
44 ovexd 
 |-  ( ( ph /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` ( mulGrp ` ( R ^s B ) ) ) y ) e. _V )
45 40 simprd 
 |-  ( ph -> ( +g ` ( mulGrp ` ( R ^s B ) ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) )
46 45 oveqdr 
 |-  ( ( ph /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` ( mulGrp ` ( R ^s B ) ) ) y ) = ( x ( +g ` ( ( mulGrp ` R ) ^s B ) ) y ) )
47 27 30 31 41 43 44 46 mulgpropd 
 |-  ( ph -> ( .g ` ( mulGrp ` ( R ^s B ) ) ) = ( .g ` ( ( mulGrp ` R ) ^s B ) ) )
48 47 oveqd 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( O ` M ) ) = ( N ( .g ` ( ( mulGrp ` R ) ^s B ) ) ( O ` M ) ) )
49 29 48 eqtrd 
 |-  ( ph -> ( O ` ( N .xb M ) ) = ( N ( .g ` ( ( mulGrp ` R ) ^s B ) ) ( O ` M ) ) )
50 49 fveq1d 
 |-  ( ph -> ( ( O ` ( N .xb M ) ) ` Y ) = ( ( N ( .g ` ( ( mulGrp ` R ) ^s B ) ) ( O ` M ) ) ` Y ) )
51 33 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
52 12 51 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
53 32 a1i 
 |-  ( ph -> B e. _V )
54 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
55 4 54 rhmf 
 |-  ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )
56 23 55 syl 
 |-  ( ph -> O : U --> ( Base ` ( R ^s B ) ) )
57 56 17 ffvelrnd 
 |-  ( ph -> ( O ` M ) e. ( Base ` ( R ^s B ) ) )
58 24 54 mgpbas 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( mulGrp ` ( R ^s B ) ) )
59 58 41 eqtrid 
 |-  ( ph -> ( Base ` ( R ^s B ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) )
60 57 59 eleqtrd 
 |-  ( ph -> ( O ` M ) e. ( Base ` ( ( mulGrp ` R ) ^s B ) ) )
61 34 36 30 9 pwsmulg 
 |-  ( ( ( ( mulGrp ` R ) e. Mnd /\ B e. _V ) /\ ( N e. NN0 /\ ( O ` M ) e. ( Base ` ( ( mulGrp ` R ) ^s B ) ) /\ Y e. B ) ) -> ( ( N ( .g ` ( ( mulGrp ` R ) ^s B ) ) ( O ` M ) ) ` Y ) = ( N .^ ( ( O ` M ) ` Y ) ) )
62 52 53 10 60 6 61 syl23anc 
 |-  ( ph -> ( ( N ( .g ` ( ( mulGrp ` R ) ^s B ) ) ( O ` M ) ) ` Y ) = ( N .^ ( ( O ` M ) ` Y ) ) )
63 7 simprd 
 |-  ( ph -> ( ( O ` M ) ` Y ) = V )
64 63 oveq2d 
 |-  ( ph -> ( N .^ ( ( O ` M ) ` Y ) ) = ( N .^ V ) )
65 62 64 eqtrd 
 |-  ( ph -> ( ( N ( .g ` ( ( mulGrp ` R ) ^s B ) ) ( O ` M ) ) ` Y ) = ( N .^ V ) )
66 50 65 eqtrd 
 |-  ( ph -> ( ( O ` ( N .xb M ) ) ` Y ) = ( N .^ V ) )
67 20 66 jca 
 |-  ( ph -> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .^ V ) ) )