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