Metamath Proof Explorer

Theorem metakunt10

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

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

Proof

Step Hyp Ref Expression
1 metakunt10.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt10.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt10.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt10.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt10.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt10.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 4 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
8 eqeq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 = 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) = 𝐼 ) )
9 breq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 < 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) < 𝐼 ) )
10 id ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → 𝑥 = ( 𝐶 ‘ 𝑋 ) )
11 oveq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 − 1 ) = ( ( 𝐶 ‘ 𝑋 ) − 1 ) )
12 9 10 11 ifbieq12d ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
13 8 12 ifbieq2d ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 = 𝑀 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
15 fveq2 ⊢ ( 𝑋 = 𝑀 → ( 𝐶 ‘ 𝑋 ) = ( 𝐶 ‘ 𝑀 ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐶 ‘ 𝑋 ) = ( 𝐶 ‘ 𝑀 ) )
17 5 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
18 iftrue ⊢ ( 𝑦 = 𝑀 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝐼 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝐼 )
20 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
21 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
22 1 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
23 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
24 23 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
25 20 21 21 22 24 elfzd ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑀 ) )
26 17 19 25 2 fvmptd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑀 ) = 𝐼 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐶 ‘ 𝑀 ) = 𝐼 )
28 16 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐶 ‘ 𝑋 ) = 𝐼 )
29 iftrue ⊢ ( ( 𝐶 ‘ 𝑋 ) = 𝐼 → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑀 )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑀 )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝑋 = 𝑀 )
32 31 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝑀 = 𝑋 )
33 30 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 = 𝑀 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
35 14 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 = 𝑀 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = 𝑋 )
36 1 2 3 5 metakunt2 ⊢ ( 𝜑 → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
38 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
39 37 38 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐶 ‘ 𝑋 ) ∈ ( 1 ... 𝑀 ) )
40 7 35 39 38 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )