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 eqtrid ⊢ ( 𝜑 → ( 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 ⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 ↑ 𝑉 ) ) )