Metamath Proof Explorer

Theorem metakunt12

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

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

Proof

Step Hyp Ref Expression
1 metakunt12.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt12.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt12.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt12.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt12.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt12.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 ioran ⊢ ( ¬ ( 𝑋 = 𝑀 ∨ 𝑋 < 𝐼 ) ↔ ( ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) )
8 4 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
9 eqeq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 = 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) = 𝐼 ) )
10 breq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 < 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) < 𝐼 ) )
11 id ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → 𝑥 = ( 𝐶 ‘ 𝑋 ) )
12 oveq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 − 1 ) = ( ( 𝐶 ‘ 𝑋 ) − 1 ) )
13 10 11 12 ifbieq12d ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
14 9 13 ifbieq2d ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
16 5 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
17 eqeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 = 𝑀 ↔ 𝑋 = 𝑀 ) )
18 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 < 𝐼 ↔ 𝑋 < 𝐼 ) )
19 id ⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
20 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 + 1 ) = ( 𝑋 + 1 ) )
21 18 19 20 ifbieq12d ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
22 17 21 ifbieq2d ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )
24 simp2 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝑀 )
25 iffalse ⊢ ( ¬ 𝑋 = 𝑀 → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
27 simp3 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑋 < 𝐼 )
28 iffalse ⊢ ( ¬ 𝑋 < 𝐼 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = ( 𝑋 + 1 ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = ( 𝑋 + 1 ) )
30 26 29 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = ( 𝑋 + 1 ) )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = ( 𝑋 + 1 ) )
32 23 31 eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = ( 𝑋 + 1 ) )
33 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
34 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
35 6 34 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
36 35 nnzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
37 36 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ∈ ℤ )
38 37 peano2zd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) ∈ ℤ )
39 16 32 33 38 fvmptd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) )
40 eqeq1 ⊢ ( ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) → ( ( 𝐶 ‘ 𝑋 ) = 𝐼 ↔ ( 𝑋 + 1 ) = 𝐼 ) )
41 breq1 ⊢ ( ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) → ( ( 𝐶 ‘ 𝑋 ) < 𝐼 ↔ ( 𝑋 + 1 ) < 𝐼 ) )
42 id ⊢ ( ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) → ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) )
43 oveq1 ⊢ ( ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) → ( ( 𝐶 ‘ 𝑋 ) − 1 ) = ( ( 𝑋 + 1 ) − 1 ) )
44 41 42 43 ifbieq12d ⊢ ( ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) → if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) = if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) )
45 40 44 ifbieq2d ⊢ ( ( 𝐶 ‘ 𝑋 ) = ( 𝑋 + 1 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = if ( ( 𝑋 + 1 ) = 𝐼 , 𝑀 , if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) ) )
46 39 45 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = if ( ( 𝑋 + 1 ) = 𝐼 , 𝑀 , if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) ) )
47 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
48 47 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ∈ ℝ )
49 37 zred ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ∈ ℝ )
50 38 zred ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) ∈ ℝ )
51 48 49 lenltd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼 ) )
52 27 51 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑋 )
53 49 ltp1d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 < ( 𝑋 + 1 ) )
54 48 49 50 52 53 lelttrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 < ( 𝑋 + 1 ) )
55 48 54 ltned ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ≠ ( 𝑋 + 1 ) )
56 55 necomd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) ≠ 𝐼 )
57 56 neneqd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ¬ ( 𝑋 + 1 ) = 𝐼 )
58 iffalse ⊢ ( ¬ ( 𝑋 + 1 ) = 𝐼 → if ( ( 𝑋 + 1 ) = 𝐼 , 𝑀 , if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) ) = if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) )
59 57 58 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( ( 𝑋 + 1 ) = 𝐼 , 𝑀 , if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) ) = if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) )
60 49 lep1d ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ≤ ( 𝑋 + 1 ) )
61 48 49 50 52 60 letrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐼 ≤ ( 𝑋 + 1 ) )
62 48 50 lenltd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐼 ≤ ( 𝑋 + 1 ) ↔ ¬ ( 𝑋 + 1 ) < 𝐼 ) )
63 61 62 mpbid ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ¬ ( 𝑋 + 1 ) < 𝐼 )
64 iffalse ⊢ ( ¬ ( 𝑋 + 1 ) < 𝐼 → if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) = ( ( 𝑋 + 1 ) − 1 ) )
65 63 64 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) = ( ( 𝑋 + 1 ) − 1 ) )
66 37 zcnd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝑋 ∈ ℂ )
67 1cnd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 1 ∈ ℂ )
68 66 67 pncand ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( ( 𝑋 + 1 ) − 1 ) = 𝑋 )
69 59 65 68 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( ( 𝑋 + 1 ) = 𝐼 , 𝑀 , if ( ( 𝑋 + 1 ) < 𝐼 , ( 𝑋 + 1 ) , ( ( 𝑋 + 1 ) − 1 ) ) ) = 𝑋 )
70 46 69 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
72 15 71 eqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = 𝑋 )
73 1 2 3 5 metakunt2 ⊢ ( 𝜑 → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
74 73 3ad2ant1 ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
75 74 33 ffvelrnd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐶 ‘ 𝑋 ) ∈ ( 1 ... 𝑀 ) )
76 8 72 75 33 fvmptd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )
77 76 3expb ⊢ ( ( 𝜑 ∧ ( ¬ 𝑋 = 𝑀 ∧ ¬ 𝑋 < 𝐼 ) ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )
78 7 77 sylan2b ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 = 𝑀 ∨ 𝑋 < 𝐼 ) ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )