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	$⊢ φ \to M \in ℕ$
	metakunt14.2	$⊢ φ \to I \in ℕ$
	metakunt14.3	$⊢ φ \to I \leq M$
	metakunt14.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
	metakunt14.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
Assertion	metakunt14	$⊢ φ \to (A : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \land A^{-1} = C)$

Proof

Step	Hyp	Ref	Expression
1		metakunt14.1	$⊢ φ \to M \in ℕ$
2		metakunt14.2	$⊢ φ \to I \in ℕ$
3		metakunt14.3	$⊢ φ \to I \leq M$
4		metakunt14.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
5		metakunt14.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
6	1 2 3 4	metakunt1	$⊢ φ \to A : (1 \dots M) ⟶ (1 \dots M)$
7	1 2 3 5	metakunt2	$⊢ φ \to C : (1 \dots M) ⟶ (1 \dots M)$
8	1	adantr	$⊢ (φ \land a \in (1 \dots M)) \to M \in ℕ$
9	2	adantr	$⊢ (φ \land a \in (1 \dots M)) \to I \in ℕ$
10	3	adantr	$⊢ (φ \land a \in (1 \dots M)) \to I \leq M$
11		simpr	$⊢ (φ \land a \in (1 \dots M)) \to a \in (1 \dots M)$
12	8 9 10 4 5 11	metakunt9	$⊢ (φ \land a \in (1 \dots M)) \to C (A (a)) = a$
13	12	ralrimiva	$⊢ φ \to \forall a \in (1 \dots M) C (A (a)) = a$
14	1	adantr	$⊢ (φ \land b \in (1 \dots M)) \to M \in ℕ$
15	2	adantr	$⊢ (φ \land b \in (1 \dots M)) \to I \in ℕ$
16	3	adantr	$⊢ (φ \land b \in (1 \dots M)) \to I \leq M$
17		simpr	$⊢ (φ \land b \in (1 \dots M)) \to b \in (1 \dots M)$
18	14 15 16 4 5 17	metakunt13	$⊢ (φ \land b \in (1 \dots M)) \to A (C (b)) = b$
19	18	ralrimiva	$⊢ φ \to \forall b \in (1 \dots M) A (C (b)) = b$
20	6 7 13 19	2fvidf1od	$⊢ φ \to A : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
21	6 7 13 19	2fvidinvd	$⊢ φ \to A^{-1} = C$
22	20 21	jca	$⊢ φ \to (A : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \land A^{-1} = C)$

Metamath Proof Explorer

Theorem metakunt14

Proof