Metamath Proof Explorer

Theorem metakunt33

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024)

Ref Expression
Hypotheses metakunt33.1 ⊢ φ → M ∈ ℕ
metakunt33.2 ⊢ φ → I ∈ ℕ
metakunt33.3 ⊢ φ → I ≤ M
metakunt33.4 ⊢ A = x ∈ 1 … M ⟼ if x = I M if x < I x x − 1
metakunt33.5 ⊢ B = z ∈ 1 … M ⟼ if z = M M if z < I z + M - I z + 1 - I
metakunt33.6 ⊢ C = y ∈ 1 … M ⟼ if y = M I if y < I y y + 1
metakunt33.7 ⊢ D = w ∈ 1 … M ⟼ if w = I w if w < I w + M − I + if I ≤ w + M - I 1 0 w - I + if I ≤ w − I 1 0
Assertion metakunt33 ⊢ φ → C ∘ B ∘ A = D

Proof

Step Hyp Ref Expression
1 metakunt33.1 ⊢ φ → M ∈ ℕ
2 metakunt33.2 ⊢ φ → I ∈ ℕ
3 metakunt33.3 ⊢ φ → I ≤ M
4 metakunt33.4 ⊢ A = x ∈ 1 … M ⟼ if x = I M if x < I x x − 1
5 metakunt33.5 ⊢ B = z ∈ 1 … M ⟼ if z = M M if z < I z + M - I z + 1 - I
6 metakunt33.6 ⊢ C = y ∈ 1 … M ⟼ if y = M I if y < I y y + 1
7 metakunt33.7 ⊢ D = w ∈ 1 … M ⟼ if w = I w if w < I w + M − I + if I ≤ w + M - I 1 0 w - I + if I ≤ w − I 1 0
8 1 2 3 6 metakunt2 ⊢ φ → C : 1 … M ⟶ 1 … M
9 1 2 3 5 metakunt25 ⊢ φ → B : 1 … M ⟶ 1-1 onto 1 … M
10 f1of ⊢ B : 1 … M ⟶ 1-1 onto 1 … M → B : 1 … M ⟶ 1 … M
11 9 10 syl ⊢ φ → B : 1 … M ⟶ 1 … M
12 1 2 3 4 metakunt1 ⊢ φ → A : 1 … M ⟶ 1 … M
13 11 12 fcod ⊢ φ → B ∘ A : 1 … M ⟶ 1 … M
14 8 13 fcod ⊢ φ → C ∘ B ∘ A : 1 … M ⟶ 1 … M
15 14 ffnd ⊢ φ → C ∘ B ∘ A Fn 1 … M
16 nfv ⊢ Ⅎ w φ
17 elfzelz ⊢ w ∈ 1 … M → w ∈ ℤ
18 17 adantl ⊢ φ ∧ w ∈ 1 … M → w ∈ ℤ
19 1 nnzd ⊢ φ → M ∈ ℤ
20 19 adantr ⊢ φ ∧ w ∈ 1 … M → M ∈ ℤ
21 2 nnzd ⊢ φ → I ∈ ℤ
22 21 adantr ⊢ φ ∧ w ∈ 1 … M → I ∈ ℤ
23 20 22 zsubcld ⊢ φ ∧ w ∈ 1 … M → M − I ∈ ℤ
24 18 23 zaddcld ⊢ φ ∧ w ∈ 1 … M → w + M - I ∈ ℤ
25 1zzd ⊢ φ ∧ w ∈ 1 … M → 1 ∈ ℤ
26 0zd ⊢ φ ∧ w ∈ 1 … M → 0 ∈ ℤ
27 25 26 ifcld ⊢ φ ∧ w ∈ 1 … M → if I ≤ w + M - I 1 0 ∈ ℤ
28 24 27 zaddcld ⊢ φ ∧ w ∈ 1 … M → w + M − I + if I ≤ w + M - I 1 0 ∈ ℤ
29 18 22 zsubcld ⊢ φ ∧ w ∈ 1 … M → w − I ∈ ℤ
30 25 26 ifcld ⊢ φ ∧ w ∈ 1 … M → if I ≤ w − I 1 0 ∈ ℤ
31 29 30 zaddcld ⊢ φ ∧ w ∈ 1 … M → w - I + if I ≤ w − I 1 0 ∈ ℤ
32 28 31 ifcld ⊢ φ ∧ w ∈ 1 … M → if w < I w + M − I + if I ≤ w + M - I 1 0 w - I + if I ≤ w − I 1 0 ∈ ℤ
33 18 32 ifcld ⊢ φ ∧ w ∈ 1 … M → if w = I w if w < I w + M − I + if I ≤ w + M - I 1 0 w - I + if I ≤ w − I 1 0 ∈ ℤ
34 16 33 7 fnmptd ⊢ φ → D Fn 1 … M
35 13 adantr ⊢ φ ∧ a ∈ 1 … M → B ∘ A : 1 … M ⟶ 1 … M
36 simpr ⊢ φ ∧ a ∈ 1 … M → a ∈ 1 … M
37 35 36 fvco3d ⊢ φ ∧ a ∈ 1 … M → C ∘ B ∘ A ⁡ a = C ⁡ B ∘ A ⁡ a
38 12 adantr ⊢ φ ∧ a ∈ 1 … M → A : 1 … M ⟶ 1 … M
39 38 36 fvco3d ⊢ φ ∧ a ∈ 1 … M → B ∘ A ⁡ a = B ⁡ A ⁡ a
40 39 fveq2d ⊢ φ ∧ a ∈ 1 … M → C ⁡ B ∘ A ⁡ a = C ⁡ B ⁡ A ⁡ a
41 37 40 eqtrd ⊢ φ ∧ a ∈ 1 … M → C ∘ B ∘ A ⁡ a = C ⁡ B ⁡ A ⁡ a
42 1 adantr ⊢ φ ∧ a ∈ 1 … M → M ∈ ℕ
43 2 adantr ⊢ φ ∧ a ∈ 1 … M → I ∈ ℕ
44 3 adantr ⊢ φ ∧ a ∈ 1 … M → I ≤ M
45 eqid ⊢ if I ≤ a + M - I 1 0 = if I ≤ a + M - I 1 0
46 eqid ⊢ if I ≤ a − I 1 0 = if I ≤ a − I 1 0
47 eqid ⊢ if a = I a if a < I a + M − I + if I ≤ a + M - I 1 0 a - I + if I ≤ a − I 1 0 = if a = I a if a < I a + M − I + if I ≤ a + M - I 1 0 a - I + if I ≤ a − I 1 0
48 42 43 44 36 4 5 6 45 46 47 metakunt31 ⊢ φ ∧ a ∈ 1 … M → C ⁡ B ⁡ A ⁡ a = if a = I a if a < I a + M − I + if I ≤ a + M - I 1 0 a - I + if I ≤ a − I 1 0
49 42 43 44 36 7 45 46 47 metakunt32 ⊢ φ ∧ a ∈ 1 … M → D ⁡ a = if a = I a if a < I a + M − I + if I ≤ a + M - I 1 0 a - I + if I ≤ a − I 1 0
50 49 eqcomd ⊢ φ ∧ a ∈ 1 … M → if a = I a if a < I a + M − I + if I ≤ a + M - I 1 0 a - I + if I ≤ a − I 1 0 = D ⁡ a
51 48 50 eqtrd ⊢ φ ∧ a ∈ 1 … M → C ⁡ B ⁡ A ⁡ a = D ⁡ a
52 41 51 eqtrd ⊢ φ ∧ a ∈ 1 … M → C ∘ B ∘ A ⁡ a = D ⁡ a
53 15 34 52 eqfnfvd ⊢ φ → C ∘ B ∘ A = D