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