| Step | Hyp | Ref
| Expression |
| 1 | | ulmshft.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | | ulmshft.w |
. . 3
⊢ 𝑊 =
(ℤ≥‘(𝑀 + 𝐾)) |
| 3 | | ulmshft.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 4 | | ulmshft.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 5 | | ulmshft.f |
. . 3
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
| 6 | | ulmshft.h |
. . 3
⊢ (𝜑 → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) |
| 7 | 1, 2, 3, 4, 5, 6 | ulmshftlem 26432 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐻(⇝𝑢‘𝑆)𝐺)) |
| 8 | | eqid 2737 |
. . 3
⊢
(ℤ≥‘((𝑀 + 𝐾) + -𝐾)) = (ℤ≥‘((𝑀 + 𝐾) + -𝐾)) |
| 9 | 3, 4 | zaddcld 12726 |
. . 3
⊢ (𝜑 → (𝑀 + 𝐾) ∈ ℤ) |
| 10 | 4 | znegcld 12724 |
. . 3
⊢ (𝜑 → -𝐾 ∈ ℤ) |
| 11 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
| 12 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑀 ∈ ℤ) |
| 13 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝐾 ∈ ℤ) |
| 14 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑛 ∈ 𝑊) |
| 15 | 14, 2 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → 𝑛 ∈ (ℤ≥‘(𝑀 + 𝐾))) |
| 16 | | eluzsub 12908 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑀 + 𝐾))) → (𝑛 − 𝐾) ∈ (ℤ≥‘𝑀)) |
| 17 | 12, 13, 15, 16 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝑛 − 𝐾) ∈ (ℤ≥‘𝑀)) |
| 18 | 17, 1 | eleqtrrdi 2852 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝑛 − 𝐾) ∈ 𝑍) |
| 19 | 11, 18 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑊) → (𝐹‘(𝑛 − 𝐾)) ∈ (ℂ ↑m 𝑆)) |
| 20 | 6, 19 | fmpt3d 7136 |
. . 3
⊢ (𝜑 → 𝐻:𝑊⟶(ℂ ↑m 𝑆)) |
| 21 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 22 | 21, 1 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ (ℤ≥‘𝑀)) |
| 23 | | eluzelz 12888 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑚 ∈ ℤ) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ ℤ) |
| 25 | 24 | zcnd 12723 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ ℂ) |
| 26 | 4 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 27 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐾 ∈ ℂ) |
| 28 | 25, 27 | subnegd 11627 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑚 − -𝐾) = (𝑚 + 𝐾)) |
| 29 | 28 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐻‘(𝑚 − -𝐾)) = (𝐻‘(𝑚 + 𝐾))) |
| 30 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐻 = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))) |
| 31 | 30 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐻‘(𝑚 + 𝐾)) = ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘(𝑚 + 𝐾))) |
| 32 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐾 ∈ ℤ) |
| 33 | | eluzadd 12907 |
. . . . . . . . . 10
⊢ ((𝑚 ∈
(ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑚 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
| 34 | 22, 32, 33 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑚 + 𝐾) ∈
(ℤ≥‘(𝑀 + 𝐾))) |
| 35 | 34, 2 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑚 + 𝐾) ∈ 𝑊) |
| 36 | | fvoveq1 7454 |
. . . . . . . . 9
⊢ (𝑛 = (𝑚 + 𝐾) → (𝐹‘(𝑛 − 𝐾)) = (𝐹‘((𝑚 + 𝐾) − 𝐾))) |
| 37 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))) = (𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾))) |
| 38 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘((𝑚 + 𝐾) − 𝐾)) ∈ V |
| 39 | 36, 37, 38 | fvmpt 7016 |
. . . . . . . 8
⊢ ((𝑚 + 𝐾) ∈ 𝑊 → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘(𝑚 + 𝐾)) = (𝐹‘((𝑚 + 𝐾) − 𝐾))) |
| 40 | 35, 39 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘(𝑚 + 𝐾)) = (𝐹‘((𝑚 + 𝐾) − 𝐾))) |
| 41 | 25, 27 | pncand 11621 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 + 𝐾) − 𝐾) = 𝑚) |
| 42 | 41 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘((𝑚 + 𝐾) − 𝐾)) = (𝐹‘𝑚)) |
| 43 | 40, 42 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑛 ∈ 𝑊 ↦ (𝐹‘(𝑛 − 𝐾)))‘(𝑚 + 𝐾)) = (𝐹‘𝑚)) |
| 44 | 29, 31, 43 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐻‘(𝑚 − -𝐾)) = (𝐹‘𝑚)) |
| 45 | 44 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ (𝐻‘(𝑚 − -𝐾))) = (𝑚 ∈ 𝑍 ↦ (𝐹‘𝑚))) |
| 46 | 3 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 47 | 10 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝜑 → -𝐾 ∈ ℂ) |
| 48 | 46, 26, 47 | addassd 11283 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 + 𝐾) + -𝐾) = (𝑀 + (𝐾 + -𝐾))) |
| 49 | 26 | negidd 11610 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 + -𝐾) = 0) |
| 50 | 49 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 + (𝐾 + -𝐾)) = (𝑀 + 0)) |
| 51 | 46 | addridd 11461 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 + 0) = 𝑀) |
| 52 | 48, 50, 51 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 + 𝐾) + -𝐾) = 𝑀) |
| 53 | 52 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 →
(ℤ≥‘((𝑀 + 𝐾) + -𝐾)) = (ℤ≥‘𝑀)) |
| 54 | 53, 1 | eqtr4di 2795 |
. . . . 5
⊢ (𝜑 →
(ℤ≥‘((𝑀 + 𝐾) + -𝐾)) = 𝑍) |
| 55 | 54 | mpteq1d 5237 |
. . . 4
⊢ (𝜑 → (𝑚 ∈ (ℤ≥‘((𝑀 + 𝐾) + -𝐾)) ↦ (𝐻‘(𝑚 − -𝐾))) = (𝑚 ∈ 𝑍 ↦ (𝐻‘(𝑚 − -𝐾)))) |
| 56 | 5 | feqmptd 6977 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑚 ∈ 𝑍 ↦ (𝐹‘𝑚))) |
| 57 | 45, 55, 56 | 3eqtr4rd 2788 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑚 ∈ (ℤ≥‘((𝑀 + 𝐾) + -𝐾)) ↦ (𝐻‘(𝑚 − -𝐾)))) |
| 58 | 2, 8, 9, 10, 20, 57 | ulmshftlem 26432 |
. 2
⊢ (𝜑 → (𝐻(⇝𝑢‘𝑆)𝐺 → 𝐹(⇝𝑢‘𝑆)𝐺)) |
| 59 | 7, 58 | impbid 212 |
1
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ 𝐻(⇝𝑢‘𝑆)𝐺)) |