Metamath Proof Explorer

Theorem metakunt14

Description: A is a primitive permutation that moves the I-th element to the end and C is its inverse that moves the last element back to the I-th position. (Contributed by metakunt, 25-May-2024)

Ref Expression
Hypotheses metakunt14.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt14.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt14.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt14.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
metakunt14.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
Assertion metakunt14 ( 𝜑 → ( 𝐴 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ◡ 𝐴 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 metakunt14.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt14.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt14.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt14.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt14.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 1 2 3 4 metakunt1 ⊢ ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
7 1 2 3 5 metakunt2 ⊢ ( 𝜑 → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ∈ ℕ )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ≤ 𝑀 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → 𝑎 ∈ ( 1 ... 𝑀 ) )
12 8 9 10 4 5 11 metakunt9 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 1 ... 𝑀 ) ) → ( 𝐶 ‘ ( 𝐴 ‘ 𝑎 ) ) = 𝑎 )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝑀 ) ( 𝐶 ‘ ( 𝐴 ‘ 𝑎 ) ) = 𝑎 )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℕ )
15 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ∈ ℕ )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ≤ 𝑀 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑀 ) ) → 𝑏 ∈ ( 1 ... 𝑀 ) )
18 14 15 16 4 5 17 metakunt13 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑏 ) ) = 𝑏 )
19 18 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝑀 ) ( 𝐴 ‘ ( 𝐶 ‘ 𝑏 ) ) = 𝑏 )
20 6 7 13 19 2fvidf1od ⊢ ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
21 6 7 13 19 2fvidinvd ⊢ ( 𝜑 → ◡ 𝐴 = 𝐶 )
22 20 21 jca ⊢ ( 𝜑 → ( 𝐴 : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ∧ ◡ 𝐴 = 𝐶 ) )