Step | Hyp | Ref
| Expression |
1 | | metakunt33.1 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | | metakunt33.2 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℕ) |
3 | | metakunt33.3 |
. . . . 5
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
4 | | metakunt33.6 |
. . . . 5
⊢ 𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1)))) |
5 | 1, 2, 3, 4 | metakunt2 39848 |
. . . 4
⊢ (𝜑 → 𝐶:(1...𝑀)⟶(1...𝑀)) |
6 | | metakunt33.5 |
. . . . . . 7
⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) |
7 | 1, 2, 3, 6 | metakunt25 39871 |
. . . . . 6
⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) |
8 | | f1of 6661 |
. . . . . 6
⊢ (𝐵:(1...𝑀)–1-1-onto→(1...𝑀) → 𝐵:(1...𝑀)⟶(1...𝑀)) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵:(1...𝑀)⟶(1...𝑀)) |
10 | | metakunt33.4 |
. . . . . 6
⊢ 𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1)))) |
11 | 1, 2, 3, 10 | metakunt1 39847 |
. . . . 5
⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) |
12 | 9, 11 | fcod 6571 |
. . . 4
⊢ (𝜑 → (𝐵 ∘ 𝐴):(1...𝑀)⟶(1...𝑀)) |
13 | 5, 12 | fcod 6571 |
. . 3
⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)):(1...𝑀)⟶(1...𝑀)) |
14 | 13 | ffnd 6546 |
. 2
⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)) Fn (1...𝑀)) |
15 | | nfv 1922 |
. . 3
⊢
Ⅎ𝑤𝜑 |
16 | | elfzelz 13112 |
. . . . 5
⊢ (𝑤 ∈ (1...𝑀) → 𝑤 ∈ ℤ) |
17 | 16 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 𝑤 ∈ ℤ) |
18 | 1 | nnzd 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
19 | 18 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 𝑀 ∈ ℤ) |
20 | 2 | nnzd 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℤ) |
21 | 20 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 𝐼 ∈ ℤ) |
22 | 19, 21 | zsubcld 12287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → (𝑀 − 𝐼) ∈ ℤ) |
23 | 17, 22 | zaddcld 12286 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → (𝑤 + (𝑀 − 𝐼)) ∈ ℤ) |
24 | | 1zzd 12208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 1 ∈ ℤ) |
25 | | 0zd 12188 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 0 ∈ ℤ) |
26 | 24, 25 | ifcld 4485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ) |
27 | 23, 26 | zaddcld 12286 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)) ∈ ℤ) |
28 | 17, 21 | zsubcld 12287 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → (𝑤 − 𝐼) ∈ ℤ) |
29 | 24, 25 | ifcld 4485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝐼 ≤ (𝑤 − 𝐼), 1, 0) ∈ ℤ) |
30 | 28, 29 | zaddcld 12286 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0)) ∈ ℤ) |
31 | 27, 30 | ifcld 4485 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0))) ∈ ℤ) |
32 | 17, 31 | ifcld 4485 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0)))) ∈ ℤ) |
33 | | metakunt33.7 |
. . 3
⊢ 𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0))))) |
34 | 15, 32, 33 | fnmptd 6519 |
. 2
⊢ (𝜑 → 𝐷 Fn (1...𝑀)) |
35 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐵 ∘ 𝐴):(1...𝑀)⟶(1...𝑀)) |
36 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝑎 ∈ (1...𝑀)) |
37 | 35, 36 | fvco3d 6811 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐶 ∘ (𝐵 ∘ 𝐴))‘𝑎) = (𝐶‘((𝐵 ∘ 𝐴)‘𝑎))) |
38 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝐴:(1...𝑀)⟶(1...𝑀)) |
39 | 38, 36 | fvco3d 6811 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐵 ∘ 𝐴)‘𝑎) = (𝐵‘(𝐴‘𝑎))) |
40 | 39 | fveq2d 6721 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐶‘((𝐵 ∘ 𝐴)‘𝑎)) = (𝐶‘(𝐵‘(𝐴‘𝑎)))) |
41 | 37, 40 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐶 ∘ (𝐵 ∘ 𝐴))‘𝑎) = (𝐶‘(𝐵‘(𝐴‘𝑎)))) |
42 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) |
43 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝐼 ∈ ℕ) |
44 | 3 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝐼 ≤ 𝑀) |
45 | | eqid 2737 |
. . . . 5
⊢ if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0) = if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0) |
46 | | eqid 2737 |
. . . . 5
⊢ if(𝐼 ≤ (𝑎 − 𝐼), 1, 0) = if(𝐼 ≤ (𝑎 − 𝐼), 1, 0) |
47 | | eqid 2737 |
. . . . 5
⊢ if(𝑎 = 𝐼, 𝑎, if(𝑎 < 𝐼, ((𝑎 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0)), ((𝑎 − 𝐼) + if(𝐼 ≤ (𝑎 − 𝐼), 1, 0)))) = if(𝑎 = 𝐼, 𝑎, if(𝑎 < 𝐼, ((𝑎 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0)), ((𝑎 − 𝐼) + if(𝐼 ≤ (𝑎 − 𝐼), 1, 0)))) |
48 | 42, 43, 44, 36, 10, 6, 4, 45, 46, 47 | metakunt31 39877 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐶‘(𝐵‘(𝐴‘𝑎))) = if(𝑎 = 𝐼, 𝑎, if(𝑎 < 𝐼, ((𝑎 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0)), ((𝑎 − 𝐼) + if(𝐼 ≤ (𝑎 − 𝐼), 1, 0))))) |
49 | 42, 43, 44, 36, 33, 45, 46, 47 | metakunt32 39878 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐷‘𝑎) = if(𝑎 = 𝐼, 𝑎, if(𝑎 < 𝐼, ((𝑎 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0)), ((𝑎 − 𝐼) + if(𝐼 ≤ (𝑎 − 𝐼), 1, 0))))) |
50 | 49 | eqcomd 2743 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → if(𝑎 = 𝐼, 𝑎, if(𝑎 < 𝐼, ((𝑎 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0)), ((𝑎 − 𝐼) + if(𝐼 ≤ (𝑎 − 𝐼), 1, 0)))) = (𝐷‘𝑎)) |
51 | 48, 50 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐶‘(𝐵‘(𝐴‘𝑎))) = (𝐷‘𝑎)) |
52 | 41, 51 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐶 ∘ (𝐵 ∘ 𝐴))‘𝑎) = (𝐷‘𝑎)) |
53 | 14, 34, 52 | eqfnfvd 6855 |
1
⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)) = 𝐷) |