Theorem metakunt5

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt5.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt5.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt5.3	$$⊢\phi \to I\le M$$
4		metakunt5.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		metakunt5.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		metakunt5.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		fveq2	$$⊢X=I\to A\left(X\right)=A\left(I\right)$$
9	8	adantl	$$⊢\left(\phi \wedge X=I\right)\to A\left(X\right)=A\left(I\right)$$
10	4	a1i	$$⊢\phi \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)$$
11		simpr	$$⊢\left(\phi \wedge x=I\right)\to x=I$$
12	11	iftrued	$$⊢\left(\phi \wedge x=I\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=M$$
13		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
14	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
15	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
16	2	nnge1d	$$⊢\phi \to 1\le I$$
17	13 14 15 16 3	elfzd	$$⊢\phi \to I\in \left(1\dots M\right)$$
18	10 12 17 1	fvmptd	$$⊢\phi \to A\left(I\right)=M$$
19	18	adantr	$$⊢\left(\phi \wedge X=I\right)\to A\left(I\right)=M$$
20	9 19	eqtrd	$$⊢\left(\phi \wedge X=I\right)\to A\left(X\right)=M$$
21	20	eqeq2d	$$⊢\left(\phi \wedge X=I\right)\to \left(y=A\left(X\right)\leftrightarrow y=M\right)$$
22		iftrue	$$⊢y=M\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=I$$
23	22	3ad2ant3	$$⊢\left(\phi \wedge X=I\wedge y=M\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=I$$
24		simp2	$$⊢\left(\phi \wedge X=I\wedge y=M\right)\to X=I$$
25	23 24	eqtr4d	$$⊢\left(\phi \wedge X=I\wedge y=M\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X$$
26	25	3expia	$$⊢\left(\phi \wedge X=I\right)\to \left(y=M\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X\right)$$
27	21 26	sylbid	$$⊢\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)$$
28	27	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$$
29	1 2 3 4	metakunt1	$$⊢\phi \to A:\left(1\dots M\right)⟶\left(1\dots M\right)$$
30	29	adantr	$$⊢\left(\phi \wedge X=I\right)\to A:\left(1\dots M\right)⟶\left(1\dots M\right)$$
31	6	adantr	$$⊢\left(\phi \wedge X=I\right)\to X\in \left(1\dots M\right)$$
32	30 31	ffvelrnd	$$⊢\left(\phi \wedge X=I\right)\to A\left(X\right)\in \left(1\dots M\right)$$
33	7 28 32 31	fvmptd	$$⊢\left(\phi \wedge X=I\right)\to C\left(A\left(X\right)\right)=X$$