| 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 42207 | . . . 4
⊢ (𝜑 → 𝐶:(1...𝑀)⟶(1...𝑀)) | 
| 6 |  | metakunt33.5 | . . . . . . 7
⊢ 𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀 − 𝐼)), (𝑧 + (1 − 𝐼))))) | 
| 7 | 1, 2, 3, 6 | metakunt25 42230 | . . . . . 6
⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) | 
| 8 |  | f1of 6848 | . . . . . 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 42206 | . . . . 5
⊢ (𝜑 → 𝐴:(1...𝑀)⟶(1...𝑀)) | 
| 12 | 9, 11 | fcod 6761 | . . . 4
⊢ (𝜑 → (𝐵 ∘ 𝐴):(1...𝑀)⟶(1...𝑀)) | 
| 13 | 5, 12 | fcod 6761 | . . 3
⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)):(1...𝑀)⟶(1...𝑀)) | 
| 14 | 13 | ffnd 6737 | . 2
⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)) Fn (1...𝑀)) | 
| 15 |  | nfv 1914 | . . 3
⊢
Ⅎ𝑤𝜑 | 
| 16 |  | elfzelz 13564 | . . . . 5
⊢ (𝑤 ∈ (1...𝑀) → 𝑤 ∈ ℤ) | 
| 17 | 16 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 𝑤 ∈ ℤ) | 
| 18 | 1 | nnzd 12640 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 19 | 18 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 𝑀 ∈ ℤ) | 
| 20 | 2 | nnzd 12640 | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 21 | 20 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 𝐼 ∈ ℤ) | 
| 22 | 19, 21 | zsubcld 12727 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → (𝑀 − 𝐼) ∈ ℤ) | 
| 23 | 17, 22 | zaddcld 12726 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → (𝑤 + (𝑀 − 𝐼)) ∈ ℤ) | 
| 24 |  | 1zzd 12648 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 1 ∈ ℤ) | 
| 25 |  | 0zd 12625 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → 0 ∈ ℤ) | 
| 26 | 24, 25 | ifcld 4572 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ) | 
| 27 | 23, 26 | zaddcld 12726 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)) ∈ ℤ) | 
| 28 | 17, 21 | zsubcld 12727 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → (𝑤 − 𝐼) ∈ ℤ) | 
| 29 | 24, 25 | ifcld 4572 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝐼 ≤ (𝑤 − 𝐼), 1, 0) ∈ ℤ) | 
| 30 | 28, 29 | zaddcld 12726 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0)) ∈ ℤ) | 
| 31 | 27, 30 | ifcld 4572 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ (1...𝑀)) → if(𝑤 < 𝐼, ((𝑤 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀 − 𝐼)), 1, 0)), ((𝑤 − 𝐼) + if(𝐼 ≤ (𝑤 − 𝐼), 1, 0))) ∈ ℤ) | 
| 32 | 17, 31 | ifcld 4572 | . . 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 6709 | . 2
⊢ (𝜑 → 𝐷 Fn (1...𝑀)) | 
| 35 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐵 ∘ 𝐴):(1...𝑀)⟶(1...𝑀)) | 
| 36 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝑎 ∈ (1...𝑀)) | 
| 37 | 35, 36 | fvco3d 7009 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐶 ∘ (𝐵 ∘ 𝐴))‘𝑎) = (𝐶‘((𝐵 ∘ 𝐴)‘𝑎))) | 
| 38 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝐴:(1...𝑀)⟶(1...𝑀)) | 
| 39 | 38, 36 | fvco3d 7009 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐵 ∘ 𝐴)‘𝑎) = (𝐵‘(𝐴‘𝑎))) | 
| 40 | 39 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐶‘((𝐵 ∘ 𝐴)‘𝑎)) = (𝐶‘(𝐵‘(𝐴‘𝑎)))) | 
| 41 | 37, 40 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → ((𝐶 ∘ (𝐵 ∘ 𝐴))‘𝑎) = (𝐶‘(𝐵‘(𝐴‘𝑎)))) | 
| 42 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) | 
| 43 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → 𝐼 ∈ ℕ) | 
| 44 | 3 | adantr 480 | . . . . 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 42236 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (1...𝑀)) → (𝐶‘(𝐵‘(𝐴‘𝑎))) = if(𝑎 = 𝐼, 𝑎, if(𝑎 < 𝐼, ((𝑎 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑎 + (𝑀 − 𝐼)), 1, 0)), ((𝑎 − 𝐼) + if(𝐼 ≤ (𝑎 − 𝐼), 1, 0))))) | 
| 49 | 42, 43, 44, 36, 33, 45, 46, 47 | metakunt32 42237 | . . . . 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 7054 | 1
⊢ (𝜑 → (𝐶 ∘ (𝐵 ∘ 𝐴)) = 𝐷) |