metakunt11

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt11.1	$⊢ φ \to M \in ℕ$
2		metakunt11.2	$⊢ φ \to I \in ℕ$
3		metakunt11.3	$⊢ φ \to I \leq M$
4		metakunt11.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
5		metakunt11.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
6		metakunt11.6	$⊢ φ \to X \in (1 \dots M)$
7	4	a1i	$⊢ (φ \land X < I) \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 < I) \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	5	a1i	$⊢ (φ \land X < I) \to C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
16		eqeq1	$⊢ y = X \to (y = M \leftrightarrow X = M)$
17		breq1	$⊢ y = X \to (y < I \leftrightarrow X < I)$
18		id	$⊢ y = X \to y = X$
19		oveq1	$⊢ y = X \to y + 1 = X + 1$
20	17 18 19	ifbieq12d	$⊢ y = X \to if (y < I, y, y + 1) = if (X < I, X, X + 1)$
21	16 20	ifbieq2d	$⊢ y = X \to if (y = M, I, if (y < I, y, y + 1)) = if (X = M, I, if (X < I, X, X + 1))$
22	21	adantl	$⊢ ((φ \land X < I) \land y = X) \to if (y = M, I, if (y < I, y, y + 1)) = if (X = M, I, if (X < I, X, X + 1))$
23		elfznn	$⊢ X \in (1 \dots M) \to X \in ℕ$
24	6 23	syl	$⊢ φ \to X \in ℕ$
25	24	nnred	$⊢ φ \to X \in ℝ$
26	25	adantr	$⊢ (φ \land X < I) \to X \in ℝ$
27	2	nnred	$⊢ φ \to I \in ℝ$
28	27	adantr	$⊢ (φ \land X < I) \to I \in ℝ$
29	1	nnred	$⊢ φ \to M \in ℝ$
30	29	adantr	$⊢ (φ \land X < I) \to M \in ℝ$
31		simpr	$⊢ (φ \land X < I) \to X < I$
32	3	adantr	$⊢ (φ \land X < I) \to I \leq M$
33	26 28 30 31 32	ltletrd	$⊢ (φ \land X < I) \to X < M$
34	26 33	ltned	$⊢ (φ \land X < I) \to X \neq M$
35		df-ne	$⊢ X \neq M \leftrightarrow \neg X = M$
36	34 35	sylib	$⊢ (φ \land X < I) \to \neg X = M$
37		iffalse	$⊢ \neg X = M \to if (X = M, I, if (X < I, X, X + 1)) = if (X < I, X, X + 1)$
38	36 37	syl	$⊢ (φ \land X < I) \to if (X = M, I, if (X < I, X, X + 1)) = if (X < I, X, X + 1)$
39		iftrue	$⊢ X < I \to if (X < I, X, X + 1) = X$
40	39	adantl	$⊢ (φ \land X < I) \to if (X < I, X, X + 1) = X$
41	38 40	eqtrd	$⊢ (φ \land X < I) \to if (X = M, I, if (X < I, X, X + 1)) = X$
42	41	adantr	$⊢ ((φ \land X < I) \land y = X) \to if (X = M, I, if (X < I, X, X + 1)) = X$
43	22 42	eqtrd	$⊢ ((φ \land X < I) \land y = X) \to if (y = M, I, if (y < I, y, y + 1)) = X$
44	6	adantr	$⊢ (φ \land X < I) \to X \in (1 \dots M)$
45	15 43 44 44	fvmptd	$⊢ (φ \land X < I) \to C (X) = X$
46		eqeq1	$⊢ C (X) = X \to (C (X) = I \leftrightarrow X = I)$
47	46	ifbid	$⊢ C (X) = X \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = if (X = I, M, if (C (X) < I, C (X), C (X) - 1))$
48	45 47	syl	$⊢ (φ \land X < I) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = if (X = I, M, if (C (X) < I, C (X), C (X) - 1))$
49	26 31	ltned	$⊢ (φ \land X < I) \to X \neq I$
50	49	neneqd	$⊢ (φ \land X < I) \to \neg X = I$
51		iffalse	$⊢ \neg X = I \to if (X = I, M, if (C (X) < I, C (X), C (X) - 1)) = if (C (X) < I, C (X), C (X) - 1)$
52	50 51	syl	$⊢ (φ \land X < I) \to if (X = I, M, if (C (X) < I, C (X), C (X) - 1)) = if (C (X) < I, C (X), C (X) - 1)$
53	45	eqcomd	$⊢ (φ \land X < I) \to X = C (X)$
54		breq1	$⊢ X = C (X) \to (X < I \leftrightarrow C (X) < I)$
55		id	$⊢ X = C (X) \to X = C (X)$
56		oveq1	$⊢ X = C (X) \to X - 1 = C (X) - 1$
57	54 55 56	ifbieq12d	$⊢ X = C (X) \to if (X < I, X, X - 1) = if (C (X) < I, C (X), C (X) - 1)$
58	53 57	syl	$⊢ (φ \land X < I) \to if (X < I, X, X - 1) = if (C (X) < I, C (X), C (X) - 1)$
59	58	eqcomd	$⊢ (φ \land X < I) \to if (C (X) < I, C (X), C (X) - 1) = if (X < I, X, X - 1)$
60	31	iftrued	$⊢ (φ \land X < I) \to if (X < I, X, X - 1) = X$
61	59 60	eqtrd	$⊢ (φ \land X < I) \to if (C (X) < I, C (X), C (X) - 1) = X$
62	52 61	eqtrd	$⊢ (φ \land X < I) \to if (X = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
63	48 62	eqtrd	$⊢ (φ \land X < I) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
64	63	adantr	$⊢ ((φ \land X < I) \land x = C (X)) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
65	14 64	eqtrd	$⊢ ((φ \land X < I) \land x = C (X)) \to if (x = I, M, if (x < I, x, x - 1)) = X$
66	1 2 3 5	metakunt2	$⊢ φ \to C : (1 \dots M) ⟶ (1 \dots M)$
67	66	adantr	$⊢ (φ \land X < I) \to C : (1 \dots M) ⟶ (1 \dots M)$
68	67 44	ffvelcdmd	$⊢ (φ \land X < I) \to C (X) \in (1 \dots M)$
69	7 65 68 44	fvmptd	$⊢ (φ \land X < I) \to A (C (X)) = X$

Metamath Proof Explorer

Theorem metakunt11

Proof