Theorem metakunt33

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

	Ref	Expression
Hypotheses	metakunt33.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	metakunt33.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
	metakunt33.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
	metakunt33.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
	metakunt33.5	⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
	metakunt33.6	⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
	metakunt33.7	⊢ 𝐷 = ( 𝑤 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑤 = 𝐼 , 𝑤 , if ( 𝑤 < 𝐼 , ( ( 𝑤 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑤 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑤 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑤 − 𝐼 ) , 1 , 0 ) ) ) ) )
Assertion	metakunt33	⊢ ( 𝜑 → ( 𝐶 ∘ ( 𝐵 ∘ 𝐴 ) ) = 𝐷 )

Proof

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