| Step | Hyp | Ref
| Expression |
| 1 | | rhmply1vsca.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝐾) |
| 2 | | fconst6g 6797 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝐾 → ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}):{ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
| 3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}):{ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
| 4 | | psr1baslem 22186 |
. . . . . . . 8
⊢
(ℕ0 ↑m 1o) = {ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} |
| 5 | 4 | feq2i 6728 |
. . . . . . 7
⊢ (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}):(ℕ0
↑m 1o)⟶𝐾 ↔ ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}):{ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
| 6 | 3, 5 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}):(ℕ0
↑m 1o)⟶𝐾) |
| 7 | | rhmply1vsca.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 8 | | rhmply1vsca.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
| 9 | | rhmply1vsca.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑃) |
| 10 | | rhmply1vsca.k |
. . . . . . . 8
⊢ 𝐾 = (Base‘𝑅) |
| 11 | 8, 9, 10 | ply1basf 22204 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋:(ℕ0 ↑m
1o)⟶𝐾) |
| 12 | 7, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋:(ℕ0 ↑m
1o)⟶𝐾) |
| 13 | | rhmply1vsca.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ (𝑅 RingHom 𝑆)) |
| 14 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 15 | 10, 14 | rhmf 20485 |
. . . . . . . 8
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝐻:𝐾⟶(Base‘𝑆)) |
| 16 | 13, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐻:𝐾⟶(Base‘𝑆)) |
| 17 | 16 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → 𝐻 Fn 𝐾) |
| 18 | | ovexd 7466 |
. . . . . 6
⊢ (𝜑 → (ℕ0
↑m 1o) ∈ V) |
| 19 | | rhmrcl1 20476 |
. . . . . . . . 9
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝑅 ∈ Ring) |
| 20 | 13, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 21 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 22 | 10, 21 | ringcl 20247 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎(.r‘𝑅)𝑏) ∈ 𝐾) |
| 23 | 20, 22 | syl3an1 1164 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝑎(.r‘𝑅)𝑏) ∈ 𝐾) |
| 24 | 23 | 3expb 1121 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾)) → (𝑎(.r‘𝑅)𝑏) ∈ 𝐾) |
| 25 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑆) = (.r‘𝑆) |
| 26 | 10, 21, 25 | rhmmul 20486 |
. . . . . . . 8
⊢ ((𝐻 ∈ (𝑅 RingHom 𝑆) ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝐻‘(𝑎(.r‘𝑅)𝑏)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑏))) |
| 27 | 13, 26 | syl3an1 1164 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (𝐻‘(𝑎(.r‘𝑅)𝑏)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑏))) |
| 28 | 27 | 3expb 1121 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾)) → (𝐻‘(𝑎(.r‘𝑅)𝑏)) = ((𝐻‘𝑎)(.r‘𝑆)(𝐻‘𝑏))) |
| 29 | 6, 12, 17, 18, 24, 28 | coof 7721 |
. . . . 5
⊢ (𝜑 → (𝐻 ∘ (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}) ∘f
(.r‘𝑅)𝑋)) = ((𝐻 ∘ ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶})) ∘f
(.r‘𝑆)(𝐻 ∘ 𝑋))) |
| 30 | | fcoconst 7154 |
. . . . . . 7
⊢ ((𝐻 Fn 𝐾 ∧ 𝐶 ∈ 𝐾) → (𝐻 ∘ ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶})) = ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(𝐻‘𝐶)})) |
| 31 | 17, 1, 30 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∘ ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶})) = ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(𝐻‘𝐶)})) |
| 32 | 31 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((𝐻 ∘ ({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶})) ∘f
(.r‘𝑆)(𝐻 ∘ 𝑋)) = (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(𝐻‘𝐶)}) ∘f
(.r‘𝑆)(𝐻 ∘ 𝑋))) |
| 33 | 29, 32 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}) ∘f
(.r‘𝑅)𝑋)) = (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(𝐻‘𝐶)}) ∘f
(.r‘𝑆)(𝐻 ∘ 𝑋))) |
| 34 | | eqid 2737 |
. . . . . 6
⊢
(1o mPoly 𝑅) = (1o mPoly 𝑅) |
| 35 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘(1o mPoly 𝑅)) = (
·𝑠 ‘(1o mPoly 𝑅)) |
| 36 | 8, 9 | ply1bas 22196 |
. . . . . 6
⊢ 𝐵 = (Base‘(1o
mPoly 𝑅)) |
| 37 | | eqid 2737 |
. . . . . 6
⊢ {ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} |
| 38 | 34, 35, 10, 36, 21, 37, 1, 7 | mplvsca 22035 |
. . . . 5
⊢ (𝜑 → (𝐶( ·𝑠
‘(1o mPoly 𝑅))𝑋) = (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}) ∘f
(.r‘𝑅)𝑋)) |
| 39 | 38 | coeq2d 5873 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ (𝐶( ·𝑠
‘(1o mPoly 𝑅))𝑋)) = (𝐻 ∘ (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {𝐶}) ∘f
(.r‘𝑅)𝑋))) |
| 40 | | eqid 2737 |
. . . . 5
⊢
(1o mPoly 𝑆) = (1o mPoly 𝑆) |
| 41 | | eqid 2737 |
. . . . 5
⊢ (
·𝑠 ‘(1o mPoly 𝑆)) = (
·𝑠 ‘(1o mPoly 𝑆)) |
| 42 | | rhmply1vsca.q |
. . . . . 6
⊢ 𝑄 = (Poly1‘𝑆) |
| 43 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑄) =
(Base‘𝑄) |
| 44 | 42, 43 | ply1bas 22196 |
. . . . 5
⊢
(Base‘𝑄) =
(Base‘(1o mPoly 𝑆)) |
| 45 | 16, 1 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝐶) ∈ (Base‘𝑆)) |
| 46 | | rhmghm 20484 |
. . . . . . 7
⊢ (𝐻 ∈ (𝑅 RingHom 𝑆) → 𝐻 ∈ (𝑅 GrpHom 𝑆)) |
| 47 | | ghmmhm 19244 |
. . . . . . 7
⊢ (𝐻 ∈ (𝑅 GrpHom 𝑆) → 𝐻 ∈ (𝑅 MndHom 𝑆)) |
| 48 | 13, 46, 47 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ (𝑅 MndHom 𝑆)) |
| 49 | 8, 42, 9, 43, 48, 7 | mhmcoply1 22389 |
. . . . 5
⊢ (𝜑 → (𝐻 ∘ 𝑋) ∈ (Base‘𝑄)) |
| 50 | 40, 41, 14, 44, 25, 37, 45, 49 | mplvsca 22035 |
. . . 4
⊢ (𝜑 → ((𝐻‘𝐶)( ·𝑠
‘(1o mPoly 𝑆))(𝐻 ∘ 𝑋)) = (({ℎ ∈ (ℕ0
↑m 1o) ∣ (◡ℎ “ ℕ) ∈ Fin} × {(𝐻‘𝐶)}) ∘f
(.r‘𝑆)(𝐻 ∘ 𝑋))) |
| 51 | 33, 39, 50 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → (𝐻 ∘ (𝐶( ·𝑠
‘(1o mPoly 𝑅))𝑋)) = ((𝐻‘𝐶)( ·𝑠
‘(1o mPoly 𝑆))(𝐻 ∘ 𝑋))) |
| 52 | | rhmply1vsca.t |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑃) |
| 53 | 8, 34, 52 | ply1vsca 22226 |
. . . . 5
⊢ · = (
·𝑠 ‘(1o mPoly 𝑅)) |
| 54 | 53 | oveqi 7444 |
. . . 4
⊢ (𝐶 · 𝑋) = (𝐶( ·𝑠
‘(1o mPoly 𝑅))𝑋) |
| 55 | 54 | coeq2i 5871 |
. . 3
⊢ (𝐻 ∘ (𝐶 · 𝑋)) = (𝐻 ∘ (𝐶( ·𝑠
‘(1o mPoly 𝑅))𝑋)) |
| 56 | | rhmply1vsca.u |
. . . . 5
⊢ ∙ = (
·𝑠 ‘𝑄) |
| 57 | 42, 40, 56 | ply1vsca 22226 |
. . . 4
⊢ ∙ = (
·𝑠 ‘(1o mPoly 𝑆)) |
| 58 | 57 | oveqi 7444 |
. . 3
⊢ ((𝐻‘𝐶) ∙ (𝐻 ∘ 𝑋)) = ((𝐻‘𝐶)( ·𝑠
‘(1o mPoly 𝑆))(𝐻 ∘ 𝑋)) |
| 59 | 51, 55, 58 | 3eqtr4g 2802 |
. 2
⊢ (𝜑 → (𝐻 ∘ (𝐶 · 𝑋)) = ((𝐻‘𝐶) ∙ (𝐻 ∘ 𝑋))) |
| 60 | | rhmply1vsca.f |
. . 3
⊢ 𝐹 = (𝑝 ∈ 𝐵 ↦ (𝐻 ∘ 𝑝)) |
| 61 | | coeq2 5869 |
. . 3
⊢ (𝑝 = (𝐶 · 𝑋) → (𝐻 ∘ 𝑝) = (𝐻 ∘ (𝐶 · 𝑋))) |
| 62 | 8, 9, 10, 52, 20, 1, 7 | ply1vscl 22388 |
. . 3
⊢ (𝜑 → (𝐶 · 𝑋) ∈ 𝐵) |
| 63 | 13, 62 | coexd 7953 |
. . 3
⊢ (𝜑 → (𝐻 ∘ (𝐶 · 𝑋)) ∈ V) |
| 64 | 60, 61, 62, 63 | fvmptd3 7039 |
. 2
⊢ (𝜑 → (𝐹‘(𝐶 · 𝑋)) = (𝐻 ∘ (𝐶 · 𝑋))) |
| 65 | | coeq2 5869 |
. . . 4
⊢ (𝑝 = 𝑋 → (𝐻 ∘ 𝑝) = (𝐻 ∘ 𝑋)) |
| 66 | 13, 7 | coexd 7953 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ 𝑋) ∈ V) |
| 67 | 60, 65, 7, 66 | fvmptd3 7039 |
. . 3
⊢ (𝜑 → (𝐹‘𝑋) = (𝐻 ∘ 𝑋)) |
| 68 | 67 | oveq2d 7447 |
. 2
⊢ (𝜑 → ((𝐻‘𝐶) ∙ (𝐹‘𝑋)) = ((𝐻‘𝐶) ∙ (𝐻 ∘ 𝑋))) |
| 69 | 59, 64, 68 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐹‘(𝐶 · 𝑋)) = ((𝐻‘𝐶) ∙ (𝐹‘𝑋))) |