| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
| 2 | | evl1addd.u |
. . . 4
⊢ 𝑈 = (Base‘𝑃) |
| 3 | 1, 2 | mgpbas 20142 |
. . 3
⊢ 𝑈 =
(Base‘(mulGrp‘𝑃)) |
| 4 | | evl1expd.f |
. . 3
⊢ ∙ =
(.g‘(mulGrp‘𝑃)) |
| 5 | | evl1addd.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 6 | | crngring 20242 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 8 | | evl1addd.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
| 9 | 8 | ply1ring 22249 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 10 | 1 | ringmgp 20236 |
. . . 4
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
| 11 | 7, 9, 10 | 3syl 18 |
. . 3
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) |
| 12 | | evl1expd.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 13 | | evl1addd.3 |
. . . 4
⊢ (𝜑 → (𝑀 ∈ 𝑈 ∧ ((𝑂‘𝑀)‘𝑌) = 𝑉)) |
| 14 | 13 | simpld 494 |
. . 3
⊢ (𝜑 → 𝑀 ∈ 𝑈) |
| 15 | 3, 4, 11, 12, 14 | mulgnn0cld 19113 |
. 2
⊢ (𝜑 → (𝑁 ∙ 𝑀) ∈ 𝑈) |
| 16 | | evl1addd.q |
. . . . . . . . 9
⊢ 𝑂 = (eval1‘𝑅) |
| 17 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
| 18 | | evl1addd.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
| 19 | 16, 8, 17, 18 | evl1rhm 22336 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐵))) |
| 20 | 5, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐵))) |
| 21 | | eqid 2737 |
. . . . . . . 8
⊢
(mulGrp‘(𝑅
↑s 𝐵)) = (mulGrp‘(𝑅 ↑s 𝐵)) |
| 22 | 1, 21 | rhmmhm 20479 |
. . . . . . 7
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐵)) → 𝑂 ∈ ((mulGrp‘𝑃) MndHom (mulGrp‘(𝑅 ↑s 𝐵)))) |
| 23 | 20, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑂 ∈ ((mulGrp‘𝑃) MndHom (mulGrp‘(𝑅 ↑s 𝐵)))) |
| 24 | | eqid 2737 |
. . . . . . 7
⊢
(.g‘(mulGrp‘(𝑅 ↑s 𝐵))) =
(.g‘(mulGrp‘(𝑅 ↑s 𝐵))) |
| 25 | 3, 4, 24 | mhmmulg 19133 |
. . . . . 6
⊢ ((𝑂 ∈ ((mulGrp‘𝑃) MndHom (mulGrp‘(𝑅 ↑s 𝐵))) ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ 𝑈) → (𝑂‘(𝑁 ∙ 𝑀)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑂‘𝑀))) |
| 26 | 23, 12, 14, 25 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑂‘(𝑁 ∙ 𝑀)) = (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑂‘𝑀))) |
| 27 | | eqid 2737 |
. . . . . . 7
⊢
(.g‘((mulGrp‘𝑅) ↑s 𝐵)) =
(.g‘((mulGrp‘𝑅) ↑s 𝐵)) |
| 28 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(mulGrp‘(𝑅 ↑s 𝐵))) = (Base‘(mulGrp‘(𝑅 ↑s 𝐵)))) |
| 29 | 18 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
| 30 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 31 | | eqid 2737 |
. . . . . . . . . 10
⊢
((mulGrp‘𝑅)
↑s 𝐵) = ((mulGrp‘𝑅) ↑s 𝐵) |
| 32 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(mulGrp‘(𝑅 ↑s 𝐵))) = (Base‘(mulGrp‘(𝑅 ↑s 𝐵))) |
| 33 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘((mulGrp‘𝑅) ↑s 𝐵)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐵)) |
| 34 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘(mulGrp‘(𝑅 ↑s 𝐵))) =
(+g‘(mulGrp‘(𝑅 ↑s 𝐵))) |
| 35 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘((mulGrp‘𝑅) ↑s 𝐵)) =
(+g‘((mulGrp‘𝑅) ↑s 𝐵)) |
| 36 | 17, 30, 31, 21, 32, 33, 34, 35 | pwsmgp 20324 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝐵 ∈ V) →
((Base‘(mulGrp‘(𝑅 ↑s 𝐵))) = (Base‘((mulGrp‘𝑅) ↑s
𝐵)) ∧
(+g‘(mulGrp‘(𝑅 ↑s 𝐵))) =
(+g‘((mulGrp‘𝑅) ↑s 𝐵)))) |
| 37 | 5, 29, 36 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 →
((Base‘(mulGrp‘(𝑅 ↑s 𝐵))) = (Base‘((mulGrp‘𝑅) ↑s
𝐵)) ∧
(+g‘(mulGrp‘(𝑅 ↑s 𝐵))) =
(+g‘((mulGrp‘𝑅) ↑s 𝐵)))) |
| 38 | 37 | simpld 494 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(mulGrp‘(𝑅 ↑s 𝐵))) = (Base‘((mulGrp‘𝑅) ↑s
𝐵))) |
| 39 | | ssv 4008 |
. . . . . . . 8
⊢
(Base‘(mulGrp‘(𝑅 ↑s 𝐵))) ⊆ V |
| 40 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
(Base‘(mulGrp‘(𝑅 ↑s 𝐵))) ⊆ V) |
| 41 | | ovexd 7466 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘(mulGrp‘(𝑅 ↑s 𝐵)))𝑦) ∈ V) |
| 42 | 37 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 →
(+g‘(mulGrp‘(𝑅 ↑s 𝐵))) =
(+g‘((mulGrp‘𝑅) ↑s 𝐵))) |
| 43 | 42 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘(mulGrp‘(𝑅 ↑s 𝐵)))𝑦) = (𝑥(+g‘((mulGrp‘𝑅) ↑s
𝐵))𝑦)) |
| 44 | 24, 27, 28, 38, 40, 41, 43 | mulgpropd 19134 |
. . . . . 6
⊢ (𝜑 →
(.g‘(mulGrp‘(𝑅 ↑s 𝐵))) =
(.g‘((mulGrp‘𝑅) ↑s 𝐵))) |
| 45 | 44 | oveqd 7448 |
. . . . 5
⊢ (𝜑 → (𝑁(.g‘(mulGrp‘(𝑅 ↑s 𝐵)))(𝑂‘𝑀)) = (𝑁(.g‘((mulGrp‘𝑅) ↑s
𝐵))(𝑂‘𝑀))) |
| 46 | 26, 45 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝑂‘(𝑁 ∙ 𝑀)) = (𝑁(.g‘((mulGrp‘𝑅) ↑s
𝐵))(𝑂‘𝑀))) |
| 47 | 46 | fveq1d 6908 |
. . 3
⊢ (𝜑 → ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = ((𝑁(.g‘((mulGrp‘𝑅) ↑s
𝐵))(𝑂‘𝑀))‘𝑌)) |
| 48 | 30 | ringmgp 20236 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
| 49 | 7, 48 | syl 17 |
. . . . 5
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
| 50 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
| 51 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
| 52 | 2, 51 | rhmf 20485 |
. . . . . . . 8
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐵)) → 𝑂:𝑈⟶(Base‘(𝑅 ↑s 𝐵))) |
| 53 | 20, 52 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑂:𝑈⟶(Base‘(𝑅 ↑s 𝐵))) |
| 54 | 53, 14 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝑂‘𝑀) ∈ (Base‘(𝑅 ↑s 𝐵))) |
| 55 | 21, 51 | mgpbas 20142 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(mulGrp‘(𝑅 ↑s 𝐵))) |
| 56 | 55, 38 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (Base‘(𝑅 ↑s 𝐵)) =
(Base‘((mulGrp‘𝑅) ↑s 𝐵))) |
| 57 | 54, 56 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → (𝑂‘𝑀) ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐵))) |
| 58 | | evl1addd.2 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 59 | | evl1expd.e |
. . . . . 6
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
| 60 | 31, 33, 27, 59 | pwsmulg 19137 |
. . . . 5
⊢
((((mulGrp‘𝑅)
∈ Mnd ∧ 𝐵 ∈
V) ∧ (𝑁 ∈
ℕ0 ∧ (𝑂‘𝑀) ∈ (Base‘((mulGrp‘𝑅) ↑s
𝐵)) ∧ 𝑌 ∈ 𝐵)) → ((𝑁(.g‘((mulGrp‘𝑅) ↑s
𝐵))(𝑂‘𝑀))‘𝑌) = (𝑁 ↑ ((𝑂‘𝑀)‘𝑌))) |
| 61 | 49, 50, 12, 57, 58, 60 | syl23anc 1379 |
. . . 4
⊢ (𝜑 → ((𝑁(.g‘((mulGrp‘𝑅) ↑s
𝐵))(𝑂‘𝑀))‘𝑌) = (𝑁 ↑ ((𝑂‘𝑀)‘𝑌))) |
| 62 | 13 | simprd 495 |
. . . . 5
⊢ (𝜑 → ((𝑂‘𝑀)‘𝑌) = 𝑉) |
| 63 | 62 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝑁 ↑ ((𝑂‘𝑀)‘𝑌)) = (𝑁 ↑ 𝑉)) |
| 64 | 61, 63 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((𝑁(.g‘((mulGrp‘𝑅) ↑s
𝐵))(𝑂‘𝑀))‘𝑌) = (𝑁 ↑ 𝑉)) |
| 65 | 47, 64 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 ↑ 𝑉)) |
| 66 | 15, 65 | jca 511 |
1
⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝑈 ∧ ((𝑂‘(𝑁 ∙ 𝑀))‘𝑌) = (𝑁 ↑ 𝑉))) |