Metamath Proof Explorer

Theorem metakunt8

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

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

Proof

Step Hyp Ref Expression
1 metakunt8.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt8.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt8.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt8.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt8.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt8.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 5 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 1 2 3 4 5 6 metakunt7 ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) ∧ ¬ ( 𝐴 ‘ 𝑋 ) = 𝑀 ∧ ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 ) )
16 15 simp2d ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ¬ ( 𝐴 ‘ 𝑋 ) = 𝑀 )
17 iffalse ⊢ ( ¬ ( 𝐴 ‘ 𝑋 ) = 𝑀 → if ( ( 𝐴 ‘ 𝑋 ) = 𝑀 , 𝐼 , if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) ) = if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( ( 𝐴 ‘ 𝑋 ) = 𝑀 , 𝐼 , if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) ) = if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) )
19 15 simp3d ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 )
20 iffalse ⊢ ( ¬ ( 𝐴 ‘ 𝑋 ) < 𝐼 → if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) = ( ( 𝐴 ‘ 𝑋 ) + 1 ) )
21 19 20 syl ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) = ( ( 𝐴 ‘ 𝑋 ) + 1 ) )
22 18 21 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( ( 𝐴 ‘ 𝑋 ) = 𝑀 , 𝐼 , if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) ) = ( ( 𝐴 ‘ 𝑋 ) + 1 ) )
23 15 simp1d ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) )
24 23 oveq1d ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( ( 𝐴 ‘ 𝑋 ) + 1 ) = ( ( 𝑋 − 1 ) + 1 ) )
25 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
26 6 25 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
27 26 nncnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
28 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
29 27 28 npcand ⊢ ( 𝜑 → ( ( 𝑋 − 1 ) + 1 ) = 𝑋 )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( ( 𝑋 − 1 ) + 1 ) = 𝑋 )
31 24 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( ( 𝐴 ‘ 𝑋 ) + 1 ) = 𝑋 )
32 22 31 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → if ( ( 𝐴 ‘ 𝑋 ) = 𝑀 , 𝐼 , if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) ) = 𝑋 )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝐼 < 𝑋 ) ∧ 𝑦 = ( 𝐴 ‘ 𝑋 ) ) → if ( ( 𝐴 ‘ 𝑋 ) = 𝑀 , 𝐼 , if ( ( 𝐴 ‘ 𝑋 ) < 𝐼 , ( 𝐴 ‘ 𝑋 ) , ( ( 𝐴 ‘ 𝑋 ) + 1 ) ) ) = 𝑋 )
34 14 33 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐼 < 𝑋 ) ∧ 𝑦 = ( 𝐴 ‘ 𝑋 ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 )
35 1 2 3 4 metakunt1 ⊢ ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
37 6 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
38 36 37 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( 1 ... 𝑀 ) )
39 7 34 38 37 fvmptd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝑋 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )