Theorem metakunt9

Description: C is the left inverse for A. (Contributed by metakunt, 24-May-2024)

	Ref	Expression
Hypotheses	metakunt9.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	metakunt9.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
	metakunt9.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
	metakunt9.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
	metakunt9.5	⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
	metakunt9.6	⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
Assertion	metakunt9	⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		metakunt9.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		metakunt9.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3		metakunt9.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4		metakunt9.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5		metakunt9.5	⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6		metakunt9.6	⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7	1 2 3 4 5 6	metakunt8	⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )
8		elfznn	⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
9	6 8	syl	⊢ ( 𝜑 → 𝑋 ∈ ℕ )
10	9	nnred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
11	2	nnred	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
12	10 11	leloed	⊢ ( 𝜑 → ( 𝑋 ≤ 𝐼 ↔ ( 𝑋 < 𝐼 ∨ 𝑋 = 𝐼 ) ) )
13	1 2 3 4 5 6	metakunt6	⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )
14	1 2 3 4 5 6	metakunt5	⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )
15	13 14	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑋 < 𝐼 ∨ 𝑋 = 𝐼 ) ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )
16	15	ex	⊢ ( 𝜑 → ( ( 𝑋 < 𝐼 ∨ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 ) )
17	12 16	sylbid	⊢ ( 𝜑 → ( 𝑋 ≤ 𝐼 → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 ) )
18	17	imp	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝐼 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )
19	7 18 11 10	ltlecasei	⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )