Metamath Proof Explorer


Theorem evl1expd

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

Ref Expression
Hypotheses evl1addd.q 𝑂 = ( eval1𝑅 )
evl1addd.p 𝑃 = ( Poly1𝑅 )
evl1addd.b 𝐵 = ( Base ‘ 𝑅 )
evl1addd.u 𝑈 = ( Base ‘ 𝑃 )
evl1addd.1 ( 𝜑𝑅 ∈ CRing )
evl1addd.2 ( 𝜑𝑌𝐵 )
evl1addd.3 ( 𝜑 → ( 𝑀𝑈 ∧ ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
evl1expd.f = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
evl1expd.e = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
evl1expd.4 ( 𝜑𝑁 ∈ ℕ0 )
Assertion evl1expd ( 𝜑 → ( ( 𝑁 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 evl1addd.q 𝑂 = ( eval1𝑅 )
2 evl1addd.p 𝑃 = ( Poly1𝑅 )
3 evl1addd.b 𝐵 = ( Base ‘ 𝑅 )
4 evl1addd.u 𝑈 = ( Base ‘ 𝑃 )
5 evl1addd.1 ( 𝜑𝑅 ∈ CRing )
6 evl1addd.2 ( 𝜑𝑌𝐵 )
7 evl1addd.3 ( 𝜑 → ( 𝑀𝑈 ∧ ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
8 evl1expd.f = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
9 evl1expd.e = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
10 evl1expd.4 ( 𝜑𝑁 ∈ ℕ0 )
11 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12 5 11 syl ( 𝜑𝑅 ∈ Ring )
13 2 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
14 eqid ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
15 14 ringmgp ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
16 12 13 15 3syl ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
17 7 simpld ( 𝜑𝑀𝑈 )
18 14 4 mgpbas 𝑈 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
19 18 8 mulgnn0cl ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑁 ∈ ℕ0𝑀𝑈 ) → ( 𝑁 𝑀 ) ∈ 𝑈 )
20 16 10 17 19 syl3anc ( 𝜑 → ( 𝑁 𝑀 ) ∈ 𝑈 )
21 eqid ( 𝑅s 𝐵 ) = ( 𝑅s 𝐵 )
22 1 2 21 3 evl1rhm ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅s 𝐵 ) ) )
23 5 22 syl ( 𝜑𝑂 ∈ ( 𝑃 RingHom ( 𝑅s 𝐵 ) ) )
24 eqid ( mulGrp ‘ ( 𝑅s 𝐵 ) ) = ( mulGrp ‘ ( 𝑅s 𝐵 ) )
25 14 24 rhmmhm ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅s 𝐵 ) ) → 𝑂 ∈ ( ( mulGrp ‘ 𝑃 ) MndHom ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) )
26 23 25 syl ( 𝜑𝑂 ∈ ( ( mulGrp ‘ 𝑃 ) MndHom ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) )
27 eqid ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
28 18 8 27 mhmmulg ( ( 𝑂 ∈ ( ( mulGrp ‘ 𝑃 ) MndHom ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ∧ 𝑁 ∈ ℕ0𝑀𝑈 ) → ( 𝑂 ‘ ( 𝑁 𝑀 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑂𝑀 ) ) )
29 26 10 17 28 syl3anc ( 𝜑 → ( 𝑂 ‘ ( 𝑁 𝑀 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑂𝑀 ) ) )
30 eqid ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) = ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) )
31 eqidd ( 𝜑 → ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) )
32 3 fvexi 𝐵 ∈ V
33 eqid ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
34 eqid ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) = ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 )
35 eqid ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
36 eqid ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) )
37 eqid ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
38 eqid ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) )
39 21 33 34 24 35 36 37 38 pwsmgp ( ( 𝑅 ∈ CRing ∧ 𝐵 ∈ V ) → ( ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ∧ ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ) )
40 5 32 39 sylancl ( 𝜑 → ( ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ∧ ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ) )
41 40 simpld ( 𝜑 → ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) )
42 ssv ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ⊆ V
43 42 a1i ( 𝜑 → ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ⊆ V )
44 ovexd ( ( 𝜑 ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) 𝑦 ) ∈ V )
45 40 simprd ( 𝜑 → ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) )
46 45 oveqdr ( ( 𝜑 ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) 𝑦 ) )
47 27 30 31 41 43 44 46 mulgpropd ( 𝜑 → ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) )
48 47 oveqd ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑂𝑀 ) ) = ( 𝑁 ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ( 𝑂𝑀 ) ) )
49 29 48 eqtrd ( 𝜑 → ( 𝑂 ‘ ( 𝑁 𝑀 ) ) = ( 𝑁 ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ( 𝑂𝑀 ) ) )
50 49 fveq1d ( 𝜑 → ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( ( 𝑁 ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ( 𝑂𝑀 ) ) ‘ 𝑌 ) )
51 33 ringmgp ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
52 12 51 syl ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
53 32 a1i ( 𝜑𝐵 ∈ V )
54 eqid ( Base ‘ ( 𝑅s 𝐵 ) ) = ( Base ‘ ( 𝑅s 𝐵 ) )
55 4 54 rhmf ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅s 𝐵 ) ) )
56 23 55 syl ( 𝜑𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅s 𝐵 ) ) )
57 56 17 ffvelrnd ( 𝜑 → ( 𝑂𝑀 ) ∈ ( Base ‘ ( 𝑅s 𝐵 ) ) )
58 24 54 mgpbas ( Base ‘ ( 𝑅s 𝐵 ) ) = ( Base ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
59 58 41 syl5eq ( 𝜑 → ( Base ‘ ( 𝑅s 𝐵 ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) )
60 57 59 eleqtrd ( 𝜑 → ( 𝑂𝑀 ) ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) )
61 34 36 30 9 pwsmulg ( ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐵 ∈ V ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑂𝑀 ) ∈ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ∧ 𝑌𝐵 ) ) → ( ( 𝑁 ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ( 𝑂𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
62 52 53 10 60 6 61 syl23anc ( 𝜑 → ( ( 𝑁 ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ( 𝑂𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
63 7 simprd ( 𝜑 → ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑉 )
64 63 oveq2d ( 𝜑 → ( 𝑁 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑁 𝑉 ) )
65 62 64 eqtrd ( 𝜑 → ( ( 𝑁 ( .g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐵 ) ) ( 𝑂𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 𝑉 ) )
66 50 65 eqtrd ( 𝜑 → ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 𝑉 ) )
67 20 66 jca ( 𝜑 → ( ( 𝑁 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 𝑉 ) ) )