metakunt5

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

	Ref	Expression
Hypotheses	metakunt5.1	$⊢ φ \to M \in ℕ$
	metakunt5.2	$⊢ φ \to I \in ℕ$
	metakunt5.3	$⊢ φ \to I \leq M$
	metakunt5.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
	metakunt5.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
	metakunt5.6	$⊢ φ \to X \in (1 \dots M)$
Assertion	metakunt5	$⊢ (φ \land X = I) \to C (A (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		metakunt5.1	$⊢ φ \to M \in ℕ$
2		metakunt5.2	$⊢ φ \to I \in ℕ$
3		metakunt5.3	$⊢ φ \to I \leq M$
4		metakunt5.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
5		metakunt5.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
6		metakunt5.6	$⊢ φ \to X \in (1 \dots M)$
7	5	a1i	$⊢ (φ \land X = I) \to C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
8		fveq2	$⊢ X = I \to A (X) = A (I)$
9	8	adantl	$⊢ (φ \land X = I) \to A (X) = A (I)$
10	4	a1i	$⊢ φ \to A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
11		simpr	$⊢ (φ \land x = I) \to x = I$
12	11	iftrued	$⊢ (φ \land x = I) \to if (x = I, M, if (x < I, x, x - 1)) = M$
13		1zzd	$⊢ φ \to 1 \in ℤ$
14	1	nnzd	$⊢ φ \to M \in ℤ$
15	2	nnzd	$⊢ φ \to I \in ℤ$
16	2	nnge1d	$⊢ φ \to 1 \leq I$
17	13 14 15 16 3	elfzd	$⊢ φ \to I \in (1 \dots M)$
18	10 12 17 1	fvmptd	$⊢ φ \to A (I) = M$
19	18	adantr	$⊢ (φ \land X = I) \to A (I) = M$
20	9 19	eqtrd	$⊢ (φ \land X = I) \to A (X) = M$
21	20	eqeq2d	$⊢ (φ \land X = I) \to (y = A (X) \leftrightarrow y = M)$
22		iftrue	$⊢ y = M \to if (y = M, I, if (y < I, y, y + 1)) = I$
23	22	3ad2ant3	$⊢ (φ \land X = I \land y = M) \to if (y = M, I, if (y < I, y, y + 1)) = I$
24		simp2	$⊢ (φ \land X = I \land y = M) \to X = I$
25	23 24	eqtr4d	$⊢ (φ \land X = I \land y = M) \to if (y = M, I, if (y < I, y, y + 1)) = X$
26	25	3expia	$⊢ (φ \land X = I) \to (y = M \to if (y = M, I, if (y < I, y, y + 1)) = X)$
27	21 26	sylbid	$⊢ (φ \land X = I) \to (y = A (X) \to if (y = M, I, if (y < I, y, y + 1)) = X)$
28	27	imp	$⊢ ((φ \land X = I) \land y = A (X)) \to if (y = M, I, if (y < I, y, y + 1)) = X$
29	1 2 3 4	metakunt1	$⊢ φ \to A : (1 \dots M) ⟶ (1 \dots M)$
30	29	adantr	$⊢ (φ \land X = I) \to A : (1 \dots M) ⟶ (1 \dots M)$
31	6	adantr	$⊢ (φ \land X = I) \to X \in (1 \dots M)$
32	30 31	ffvelcdmd	$⊢ (φ \land X = I) \to A (X) \in (1 \dots M)$
33	7 28 32 31	fvmptd	$⊢ (φ \land X = I) \to C (A (X)) = X$

Metamath Proof Explorer

Theorem metakunt5

Proof