Metamath Proof Explorer

Theorem metakunt5

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

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

Proof

Step Hyp Ref Expression
1 metakunt5.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt5.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt5.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt5.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt5.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt5.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 5 a1i ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
8 fveq2 ⊢ ( 𝑋 = 𝐼 → ( 𝐴 ‘ 𝑋 ) = ( 𝐴 ‘ 𝐼 ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝐴 ‘ 𝐼 ) )
10 4 a1i ⊢ ( 𝜑 → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐼 ) → 𝑥 = 𝐼 )
12 11 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐼 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = 𝑀 )
13 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
14 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
15 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
16 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐼 )
17 13 14 15 16 3 elfzd ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑀 ) )
18 10 12 17 1 fvmptd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐼 ) = 𝑀 )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐴 ‘ 𝐼 ) = 𝑀 )
20 9 19 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐴 ‘ 𝑋 ) = 𝑀 )
21 20 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝑦 = ( 𝐴 ‘ 𝑋 ) ↔ 𝑦 = 𝑀 ) )
22 iftrue ⊢ ( 𝑦 = 𝑀 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝐼 )
23 22 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝐼 )
24 simp2 ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ∧ 𝑦 = 𝑀 ) → 𝑋 = 𝐼 )
25 23 24 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ∧ 𝑦 = 𝑀 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 )
26 25 3expia ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝑦 = 𝑀 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 ) )
27 21 26 sylbid ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝑦 = ( 𝐴 ‘ 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 ) )
28 27 imp ⊢ ( ( ( 𝜑 ∧ 𝑋 = 𝐼 ) ∧ 𝑦 = ( 𝐴 ‘ 𝑋 ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 )
29 1 2 3 4 metakunt1 ⊢ ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
31 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
32 30 31 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( 1 ... 𝑀 ) )
33 7 28 32 31 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝐼 ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = 𝑋 )