Theorem metakunt8

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

	Ref	Expression
Hypotheses	metakunt8.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt8.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt8.3	$$⊢\phi \to I\le M$$
	metakunt8.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)$$
	metakunt8.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)$$
	metakunt8.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
Assertion	metakunt8	$$⊢\left(\phi \wedge I<X\right)\to C\left(A\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		metakunt8.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt8.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt8.3	$$⊢\phi \to I\le M$$
4		metakunt8.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		metakunt8.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		metakunt8.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
7	5	a1i	$$⊢\left(\phi \wedge I<X\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		eqeq1	$$⊢y=A\left(X\right)\to \left(y=M\leftrightarrow A\left(X\right)=M\right)$$
9		breq1	$$⊢y=A\left(X\right)\to \left(y<I\leftrightarrow A\left(X\right)<I\right)$$
10		id	$$⊢y=A\left(X\right)\to y=A\left(X\right)$$
11		oveq1	$$⊢y=A\left(X\right)\to y+1=A\left(X\right)+1$$
12	9 10 11	ifbieq12d	$$⊢y=A\left(X\right)\to if\left(y<I,y,y+1\right)=if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)$$
13	8 12	ifbieq2d	$$⊢y=A\left(X\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)$$
14	13	adantl	$$⊢\left(\left(\phi \wedge I<X\right)\wedge y=A\left(X\right)\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)$$
15	1 2 3 4 5 6	metakunt7	$$⊢\left(\phi \wedge I<X\right)\to \left(A\left(X\right)=X-1\wedge \neg A\left(X\right)=M\wedge \neg A\left(X\right)<I\right)$$
16	15	simp2d	$$⊢\left(\phi \wedge I<X\right)\to \neg A\left(X\right)=M$$
17		iffalse	$$⊢\neg A\left(X\right)=M\to if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)=if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)$$
18	16 17	syl	$$⊢\left(\phi \wedge I<X\right)\to if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)=if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)$$
19	15	simp3d	$$⊢\left(\phi \wedge I<X\right)\to \neg A\left(X\right)<I$$
20		iffalse	$$⊢\neg A\left(X\right)<I\to if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)=A\left(X\right)+1$$
21	19 20	syl	$$⊢\left(\phi \wedge I<X\right)\to if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)=A\left(X\right)+1$$
22	18 21	eqtrd	$$⊢\left(\phi \wedge I<X\right)\to if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)=A\left(X\right)+1$$
23	15	simp1d	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)=X-1$$
24	23	oveq1d	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)+1=X-1+1$$
25		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
26	6 25	syl	$$⊢\phi \to X\in \mathbb{N}$$
27	26	nncnd	$$⊢\phi \to X\in ℂ$$
28		1cnd	$$⊢\phi \to 1\in ℂ$$
29	27 28	npcand	$$⊢\phi \to X-1+1=X$$
30	29	adantr	$$⊢\left(\phi \wedge I<X\right)\to X-1+1=X$$
31	24 30	eqtrd	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)+1=X$$
32	22 31	eqtrd	$$⊢\left(\phi \wedge I<X\right)\to if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)=X$$
33	32	adantr	$$⊢\left(\left(\phi \wedge I<X\right)\wedge y=A\left(X\right)\right)\to if\left(A\left(X\right)=M,I,if\left(A\left(X\right)<I,A\left(X\right),A\left(X\right)+1\right)\right)=X$$
34	14 33	eqtrd	$$⊢\left(\left(\phi \wedge I<X\right)\wedge y=A\left(X\right)\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X$$
35	1 2 3 4	metakunt1	$$⊢\phi \to A:\left(1\dots M\right)⟶\left(1\dots M\right)$$
36	35	adantr	$$⊢\left(\phi \wedge I<X\right)\to A:\left(1\dots M\right)⟶\left(1\dots M\right)$$
37	6	adantr	$$⊢\left(\phi \wedge I<X\right)\to X\in \left(1\dots M\right)$$
38	36 37	ffvelrnd	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)\in \left(1\dots M\right)$$
39	7 34 38 37	fvmptd	$$⊢\left(\phi \wedge I<X\right)\to C\left(A\left(X\right)\right)=X$$