Theorem metakunt6

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

	Ref	Expression
Hypotheses	metakunt6.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt6.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt6.3	$$⊢\phi \to I\le M$$
	metakunt6.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
	metakunt6.5	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
	metakunt6.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
Assertion	metakunt6	$$⊢\left(\phi \wedge X<I\right)\to C\left(A\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		metakunt6.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt6.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt6.3	$$⊢\phi \to I\le M$$
4		metakunt6.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
5		metakunt6.5	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
6		metakunt6.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
7	5	a1i	$$⊢\left(\phi \wedge X<I\right)\to C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
8	4	a1i	$$⊢\left(\phi \wedge X<I\right)\to A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
9		id	$$⊢x=X\to x=X$$
10	9	eqeq1d	$$⊢x=X\to \left(x=I\leftrightarrow X=I\right)$$
11		breq1	$$⊢x=X\to \left(x<I\leftrightarrow X<I\right)$$
12		oveq1	$$⊢x=X\to x-1=X-1$$
13	11 9 12	ifbieq12d	$$⊢x=X\to if\left(x<I,x,x-1\right)=if\left(X<I,X,X-1\right)$$
14	10 13	ifbieq2d	$$⊢x=X\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(X=I,M,if\left(X<I,X,X-1\right)\right)$$
15	14	adantl	$$⊢\left(\left(\phi \wedge X<I\right)\wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(X=I,M,if\left(X<I,X,X-1\right)\right)$$
16		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
17	6 16	syl	$$⊢\phi \to X\in \mathbb{N}$$
18	17	nnred	$$⊢\phi \to X\in ℝ$$
19	18	adantr	$$⊢\left(\phi \wedge X<I\right)\to X\in ℝ$$
20		simpr	$$⊢\left(\phi \wedge X<I\right)\to X<I$$
21	19 20	ltned	$$⊢\left(\phi \wedge X<I\right)\to X\ne I$$
22		df-ne	$$⊢X\ne I\leftrightarrow \neg X=I$$
23	21 22	sylib	$$⊢\left(\phi \wedge X<I\right)\to \neg X=I$$
24		iffalse	$$⊢\neg X=I\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=if\left(X<I,X,X-1\right)$$
25	23 24	syl	$$⊢\left(\phi \wedge X<I\right)\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=if\left(X<I,X,X-1\right)$$
26		iftrue	$$⊢X<I\to if\left(X<I,X,X-1\right)=X$$
27	26	adantl	$$⊢\left(\phi \wedge X<I\right)\to if\left(X<I,X,X-1\right)=X$$
28	25 27	eqtrd	$$⊢\left(\phi \wedge X<I\right)\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=X$$
29	28	adantr	$$⊢\left(\left(\phi \wedge X<I\right)\wedge x=X\right)\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=X$$
30	15 29	eqtrd	$$⊢\left(\left(\phi \wedge X<I\right)\wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=X$$
31	6	adantr	$$⊢\left(\phi \wedge X<I\right)\to X\in \left(1\dots M\right)$$
32	8 30 31 31	fvmptd	$$⊢\left(\phi \wedge X<I\right)\to A\left(X\right)=X$$
33		eqcom	$$⊢A\left(X\right)=X\leftrightarrow X=A\left(X\right)$$
34	33	imbi2i	$$⊢\left(\left(\phi \wedge X<I\right)\to A\left(X\right)=X\right)\leftrightarrow \left(\left(\phi \wedge X<I\right)\to X=A\left(X\right)\right)$$
35	32 34	mpbi	$$⊢\left(\phi \wedge X<I\right)\to X=A\left(X\right)$$
36	35	eqeq2d	$$⊢\left(\phi \wedge X<I\right)\to \left(y=X\leftrightarrow y=A\left(X\right)\right)$$
37		eqeq1	$$⊢y=X\to \left(y=M\leftrightarrow X=M\right)$$
38		breq1	$$⊢y=X\to \left(y<I\leftrightarrow X<I\right)$$
39		id	$$⊢y=X\to y=X$$
40		oveq1	$$⊢y=X\to y+1=X+1$$
41	38 39 40	ifbieq12d	$$⊢y=X\to if\left(y<I,y,y+1\right)=if\left(X<I,X,X+1\right)$$
42	37 41	ifbieq2d	$$⊢y=X\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$
43	42	adantl	$$⊢\left(\left(\phi \wedge X<I\right)\wedge y=X\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$
44	2	nnred	$$⊢\phi \to I\in ℝ$$
45	44	adantr	$$⊢\left(\phi \wedge X<I\right)\to I\in ℝ$$
46	1	nnred	$$⊢\phi \to M\in ℝ$$
47	46	adantr	$$⊢\left(\phi \wedge X<I\right)\to M\in ℝ$$
48	3	adantr	$$⊢\left(\phi \wedge X<I\right)\to I\le M$$
49	19 45 47 20 48	ltletrd	$$⊢\left(\phi \wedge X<I\right)\to X<M$$
50	19 49	ltned	$$⊢\left(\phi \wedge X<I\right)\to X\ne M$$
51	50	neneqd	$$⊢\left(\phi \wedge X<I\right)\to \neg X=M$$
52		iffalse	$$⊢\neg X=M\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=if\left(X<I,X,X+1\right)$$
53	51 52	syl	$$⊢\left(\phi \wedge X<I\right)\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=if\left(X<I,X,X+1\right)$$
54		iftrue	$$⊢X<I\to if\left(X<I,X,X+1\right)=X$$
55	54	adantl	$$⊢\left(\phi \wedge X<I\right)\to if\left(X<I,X,X+1\right)=X$$
56	53 55	eqtrd	$$⊢\left(\phi \wedge X<I\right)\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=X$$
57	56	adantr	$$⊢\left(\left(\phi \wedge X<I\right)\wedge y=X\right)\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=X$$
58	43 57	eqtrd	$$⊢\left(\left(\phi \wedge X<I\right)\wedge y=X\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X$$
59	58	ex	$$⊢\left(\phi \wedge X<I\right)\to \left(y=X\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X\right)$$
60	36 59	sylbird	$$⊢\left(\phi \wedge X<I\right)\to \left(y=A\left(X\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X\right)$$
61	60	imp	$$⊢\left(\left(\phi \wedge X<I\right)\wedge y=A\left(X\right)\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X$$
62	1	adantr	$$⊢\left(\phi \wedge X<I\right)\to M\in \mathbb{N}$$
63	2	adantr	$$⊢\left(\phi \wedge X<I\right)\to I\in \mathbb{N}$$
64	62 63 48 4	metakunt1	$$⊢\left(\phi \wedge X<I\right)\to A:\left(1\dots M\right)⟶\left(1\dots M\right)$$
65	64 31	ffvelrnd	$$⊢\left(\phi \wedge X<I\right)\to A\left(X\right)\in \left(1\dots M\right)$$
66	7 61 65 31	fvmptd	$$⊢\left(\phi \wedge X<I\right)\to C\left(A\left(X\right)\right)=X$$