metakunt10

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt10.1	$⊢ φ \to M \in ℕ$
2		metakunt10.2	$⊢ φ \to I \in ℕ$
3		metakunt10.3	$⊢ φ \to I \leq M$
4		metakunt10.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
5		metakunt10.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
6		metakunt10.6	$⊢ φ \to X \in (1 \dots M)$
7	4	a1i	$⊢ (φ \land X = M) \to A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
8		eqeq1	$⊢ x = C (X) \to (x = I \leftrightarrow C (X) = I)$
9		breq1	$⊢ x = C (X) \to (x < I \leftrightarrow C (X) < I)$
10		id	$⊢ x = C (X) \to x = C (X)$
11		oveq1	$⊢ x = C (X) \to x - 1 = C (X) - 1$
12	9 10 11	ifbieq12d	$⊢ x = C (X) \to if (x < I, x, x - 1) = if (C (X) < I, C (X), C (X) - 1)$
13	8 12	ifbieq2d	$⊢ x = C (X) \to if (x = I, M, if (x < I, x, x - 1)) = if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1))$
14	13	adantl	$⊢ ((φ \land X = M) \land x = C (X)) \to if (x = I, M, if (x < I, x, x - 1)) = if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1))$
15		fveq2	$⊢ X = M \to C (X) = C (M)$
16	15	adantl	$⊢ (φ \land X = M) \to C (X) = C (M)$
17	5	a1i	$⊢ φ \to C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
18		iftrue	$⊢ y = M \to if (y = M, I, if (y < I, y, y + 1)) = I$
19	18	adantl	$⊢ (φ \land y = M) \to if (y = M, I, if (y < I, y, y + 1)) = I$
20		1zzd	$⊢ φ \to 1 \in ℤ$
21	1	nnzd	$⊢ φ \to M \in ℤ$
22	1	nnge1d	$⊢ φ \to 1 \leq M$
23	1	nnred	$⊢ φ \to M \in ℝ$
24	23	leidd	$⊢ φ \to M \leq M$
25	20 21 21 22 24	elfzd	$⊢ φ \to M \in (1 \dots M)$
26	17 19 25 2	fvmptd	$⊢ φ \to C (M) = I$
27	26	adantr	$⊢ (φ \land X = M) \to C (M) = I$
28	16 27	eqtrd	$⊢ (φ \land X = M) \to C (X) = I$
29		iftrue	$⊢ C (X) = I \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = M$
30	28 29	syl	$⊢ (φ \land X = M) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = M$
31		simpr	$⊢ (φ \land X = M) \to X = M$
32	31	eqcomd	$⊢ (φ \land X = M) \to M = X$
33	30 32	eqtrd	$⊢ (φ \land X = M) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
34	33	adantr	$⊢ ((φ \land X = M) \land x = C (X)) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
35	14 34	eqtrd	$⊢ ((φ \land X = M) \land x = C (X)) \to if (x = I, M, if (x < I, x, x - 1)) = X$
36	1 2 3 5	metakunt2	$⊢ φ \to C : (1 \dots M) ⟶ (1 \dots M)$
37	36	adantr	$⊢ (φ \land X = M) \to C : (1 \dots M) ⟶ (1 \dots M)$
38	6	adantr	$⊢ (φ \land X = M) \to X \in (1 \dots M)$
39	37 38	ffvelrnd	$⊢ (φ \land X = M) \to C (X) \in (1 \dots M)$
40	7 35 39 38	fvmptd	$⊢ (φ \land X = M) \to A (C (X)) = X$

Metamath Proof Explorer

Theorem metakunt10

Proof