Metamath Proof Explorer

Theorem metakunt6

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

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

Proof

Step Hyp Ref Expression
1 metakunt6.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt6.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt6.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt6.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt6.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt6.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 5 a1i ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
8 4 a1i ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
9 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
10 9 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝐼 ↔ 𝑋 = 𝐼 ) )
11 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
12 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 1 ) = ( 𝑋 − 1 ) )
13 11 9 12 ifbieq12d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
14 10 13 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )
16 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
17 6 16 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
18 17 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ℝ )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 < 𝐼 )
21 19 20 ltned ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ≠ 𝐼 )
22 df-ne ⊢ ( 𝑋 ≠ 𝐼 ↔ ¬ 𝑋 = 𝐼 )
23 21 22 sylib ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝐼 )
24 iffalse ⊢ ( ¬ 𝑋 = 𝐼 → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
26 iftrue ⊢ ( 𝑋 < 𝐼 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = 𝑋 )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = 𝑋 )
28 25 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = 𝑋 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) = 𝑋 )
30 15 29 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = 𝑋 )
31 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
32 8 30 31 31 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐴 ‘ 𝑋 ) = 𝑋 )
33 eqcom ⊢ ( ( 𝐴 ‘ 𝑋 ) = 𝑋 ↔ 𝑋 = ( 𝐴 ‘ 𝑋 ) )
34 33 imbi2i ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐴 ‘ 𝑋 ) = 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 = ( 𝐴 ‘ 𝑋 ) ) )
35 32 34 mpbi ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 = ( 𝐴 ‘ 𝑋 ) )
36 35 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝑦 = 𝑋 ↔ 𝑦 = ( 𝐴 ‘ 𝑋 ) ) )
37 eqeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 = 𝑀 ↔ 𝑋 = 𝑀 ) )
38 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 < 𝐼 ↔ 𝑋 < 𝐼 ) )
39 id ⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
40 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 + 1 ) = ( 𝑋 + 1 ) )
41 38 39 40 ifbieq12d ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
42 37 41 ifbieq2d ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )
44 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐼 ∈ ℝ )
46 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑀 ∈ ℝ )
48 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑀 )
49 19 45 47 20 48 ltletrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 < 𝑀 )
50 19 49 ltned ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ≠ 𝑀 )
51 50 neneqd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝑀 )
52 iffalse ⊢ ( ¬ 𝑋 = 𝑀 → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
53 51 52 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
54 iftrue ⊢ ( 𝑋 < 𝐼 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = 𝑋 )
55 54 adantl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = 𝑋 )
56 53 55 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = 𝑋 )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = 𝑋 )
58 43 57 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 )
59 58 ex ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 ) )
60 36 59 sylbird ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝑦 = ( 𝐴 ‘ 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 ) )
61 60 imp ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = ( 𝐴 ‘ 𝑋 ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 )
62 1 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑀 ∈ ℕ )
63 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐼 ∈ ℕ )
64 62 63 48 4 metakunt1 ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
65 64 31 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( 1 ... 𝑀 ) )
66 7 61 65 31 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )