Theorem smndex2dlinvh

Description: The halving functions H are left inverses of the doubling function D . (Contributed by AV, 18-Feb-2024)

	Ref	Expression
Hypotheses	smndex2dbas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
	smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
	smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
	smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
	smndex2hbas.n	$$⊢N\in {\mathbb{N}}_0$$
	smndex2hbas.h	$$⊢H=\left(x\in {\mathbb{N}}_0⟼if\left(2\parallel x,\frac{x}{2},N\right)\right)$$
Assertion	smndex2dlinvh	$$⊢H\circ D=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
2		smndex2dbas.b	$$⊢B={\mathrm{Base}}_M$$
3		smndex2dbas.0	$$⊢\underset{\dot{}}{0}=0_M$$
4		smndex2dbas.d	$$⊢D=\left(x\in {\mathbb{N}}_0⟼2x\right)$$
5		smndex2hbas.n	$$⊢N\in {\mathbb{N}}_0$$
6		smndex2hbas.h	$$⊢H=\left(x\in {\mathbb{N}}_0⟼if\left(2\parallel x,\frac{x}{2},N\right)\right)$$
7		2nn0	$$⊢2\in {\mathbb{N}}_0$$
8		nn0mulcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to 2y\in {\mathbb{N}}_0$$
9		oveq2	$$⊢x=y\to 2x=2y$$
10	9	cbvmptv	$$⊢\left(x\in {\mathbb{N}}_0⟼2x\right)=\left(y\in {\mathbb{N}}_0⟼2y\right)$$
11	4 10	eqtri	$$⊢D=\left(y\in {\mathbb{N}}_0⟼2y\right)$$
12	11	a1i	$$⊢2\in {\mathbb{N}}_0\to D=\left(y\in {\mathbb{N}}_0⟼2y\right)$$
13	6	a1i	$$⊢2\in {\mathbb{N}}_0\to H=\left(x\in {\mathbb{N}}_0⟼if\left(2\parallel x,\frac{x}{2},N\right)\right)$$
14		breq2	$$⊢x=2y\to \left(2\parallel x\leftrightarrow 2\parallel 2y\right)$$
15		oveq1	$$⊢x=2y\to \frac{x}{2}=\frac{2y}{2}$$
16	14 15	ifbieq1d	$$⊢x=2y\to if\left(2\parallel x,\frac{x}{2},N\right)=if\left(2\parallel 2y,\frac{2y}{2},N\right)$$
17	8 12 13 16	fmptco	$$⊢2\in {\mathbb{N}}_0\to H\circ D=\left(y\in {\mathbb{N}}_0⟼if\left(2\parallel 2y,\frac{2y}{2},N\right)\right)$$
18	7 17	ax-mp	$$⊢H\circ D=\left(y\in {\mathbb{N}}_0⟼if\left(2\parallel 2y,\frac{2y}{2},N\right)\right)$$
19		nn0z	$$⊢y\in {\mathbb{N}}_0\to y\in \mathbb{Z}$$
20		eqidd	$$⊢y\in {\mathbb{N}}_0\to 2y=2y$$
21		2teven	$$⊢\left(y\in \mathbb{Z}\wedge 2y=2y\right)\to 2\parallel 2y$$
22	19 20 21	syl2anc	$$⊢y\in {\mathbb{N}}_0\to 2\parallel 2y$$
23	22	iftrued	$$⊢y\in {\mathbb{N}}_0\to if\left(2\parallel 2y,\frac{2y}{2},N\right)=\frac{2y}{2}$$
24	23	mpteq2ia	$$⊢\left(y\in {\mathbb{N}}_0⟼if\left(2\parallel 2y,\frac{2y}{2},N\right)\right)=\left(y\in {\mathbb{N}}_0⟼\frac{2y}{2}\right)$$
25		nn0cn	$$⊢y\in {\mathbb{N}}_0\to y\in ℂ$$
26		2cnd	$$⊢y\in {\mathbb{N}}_0\to 2\in ℂ$$
27		2ne0	$$⊢2\ne 0$$
28	27	a1i	$$⊢y\in {\mathbb{N}}_0\to 2\ne 0$$
29	25 26 28	divcan3d	$$⊢y\in {\mathbb{N}}_0\to \frac{2y}{2}=y$$
30	29	mpteq2ia	$$⊢\left(y\in {\mathbb{N}}_0⟼\frac{2y}{2}\right)=\left(y\in {\mathbb{N}}_0⟼y\right)$$
31		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
32	1	efmndid	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=0_M$$
33	31 32	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=0_M$$
34		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{{\mathbb{N}}_0}=\left(y\in {\mathbb{N}}_0⟼y\right)$$
35	3 33 34	3eqtr2ri	$$⊢\left(y\in {\mathbb{N}}_0⟼y\right)=\underset{\dot{}}{0}$$
36	30 35	eqtri	$$⊢\left(y\in {\mathbb{N}}_0⟼\frac{2y}{2}\right)=\underset{\dot{}}{0}$$
37	24 36	eqtri	$$⊢\left(y\in {\mathbb{N}}_0⟼if\left(2\parallel 2y,\frac{2y}{2},N\right)\right)=\underset{\dot{}}{0}$$
38	18 37	eqtri	$$⊢H\circ D=\underset{\dot{}}{0}$$