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	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex2dbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	smndex2dbas.0	⊢ 0 = ( 0g ‘ 𝑀 )
	smndex2dbas.d	⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
	smndex2hbas.n	⊢ 𝑁 ∈ ℕ0
	smndex2hbas.h	⊢ 𝐻 = ( 𝑥 ∈ ℕ0 ↦ if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) )
Assertion	smndex2dlinvh	⊢ ( 𝐻 ∘ 𝐷 ) = 0

Proof

Step	Hyp	Ref	Expression
1		smndex2dbas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex2dbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		smndex2dbas.0	⊢ 0 = ( 0g ‘ 𝑀 )
4		smndex2dbas.d	⊢ 𝐷 = ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) )
5		smndex2hbas.n	⊢ 𝑁 ∈ ℕ0
6		smndex2hbas.h	⊢ 𝐻 = ( 𝑥 ∈ ℕ0 ↦ if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) )
7		2nn0	⊢ 2 ∈ ℕ0
8		nn0mulcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 2 · 𝑦 ) ∈ ℕ0 )
9		oveq2	⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
10	9	cbvmptv	⊢ ( 𝑥 ∈ ℕ0 ↦ ( 2 · 𝑥 ) ) = ( 𝑦 ∈ ℕ0 ↦ ( 2 · 𝑦 ) )
11	4 10	eqtri	⊢ 𝐷 = ( 𝑦 ∈ ℕ0 ↦ ( 2 · 𝑦 ) )
12	11	a1i	⊢ ( 2 ∈ ℕ0 → 𝐷 = ( 𝑦 ∈ ℕ0 ↦ ( 2 · 𝑦 ) ) )
13	6	a1i	⊢ ( 2 ∈ ℕ0 → 𝐻 = ( 𝑥 ∈ ℕ0 ↦ if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) ) )
14		breq2	⊢ ( 𝑥 = ( 2 · 𝑦 ) → ( 2 ∥ 𝑥 ↔ 2 ∥ ( 2 · 𝑦 ) ) )
15		oveq1	⊢ ( 𝑥 = ( 2 · 𝑦 ) → ( 𝑥 / 2 ) = ( ( 2 · 𝑦 ) / 2 ) )
16	14 15	ifbieq1d	⊢ ( 𝑥 = ( 2 · 𝑦 ) → if ( 2 ∥ 𝑥 , ( 𝑥 / 2 ) , 𝑁 ) = if ( 2 ∥ ( 2 · 𝑦 ) , ( ( 2 · 𝑦 ) / 2 ) , 𝑁 ) )
17	8 12 13 16	fmptco	⊢ ( 2 ∈ ℕ0 → ( 𝐻 ∘ 𝐷 ) = ( 𝑦 ∈ ℕ0 ↦ if ( 2 ∥ ( 2 · 𝑦 ) , ( ( 2 · 𝑦 ) / 2 ) , 𝑁 ) ) )
18	7 17	ax-mp	⊢ ( 𝐻 ∘ 𝐷 ) = ( 𝑦 ∈ ℕ0 ↦ if ( 2 ∥ ( 2 · 𝑦 ) , ( ( 2 · 𝑦 ) / 2 ) , 𝑁 ) )
19		nn0z	⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ )
20		eqidd	⊢ ( 𝑦 ∈ ℕ0 → ( 2 · 𝑦 ) = ( 2 · 𝑦 ) )
21		2teven	⊢ ( ( 𝑦 ∈ ℤ ∧ ( 2 · 𝑦 ) = ( 2 · 𝑦 ) ) → 2 ∥ ( 2 · 𝑦 ) )
22	19 20 21	syl2anc	⊢ ( 𝑦 ∈ ℕ0 → 2 ∥ ( 2 · 𝑦 ) )
23	22	iftrued	⊢ ( 𝑦 ∈ ℕ0 → if ( 2 ∥ ( 2 · 𝑦 ) , ( ( 2 · 𝑦 ) / 2 ) , 𝑁 ) = ( ( 2 · 𝑦 ) / 2 ) )
24	23	mpteq2ia	⊢ ( 𝑦 ∈ ℕ0 ↦ if ( 2 ∥ ( 2 · 𝑦 ) , ( ( 2 · 𝑦 ) / 2 ) , 𝑁 ) ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 2 · 𝑦 ) / 2 ) )
25		nn0cn	⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℂ )
26		2cnd	⊢ ( 𝑦 ∈ ℕ0 → 2 ∈ ℂ )
27		2ne0	⊢ 2 ≠ 0
28	27	a1i	⊢ ( 𝑦 ∈ ℕ0 → 2 ≠ 0 )
29	25 26 28	divcan3d	⊢ ( 𝑦 ∈ ℕ0 → ( ( 2 · 𝑦 ) / 2 ) = 𝑦 )
30	29	mpteq2ia	⊢ ( 𝑦 ∈ ℕ0 ↦ ( ( 2 · 𝑦 ) / 2 ) ) = ( 𝑦 ∈ ℕ0 ↦ 𝑦 )
31		nn0ex	⊢ ℕ0 ∈ V
32	1	efmndid	⊢ ( ℕ0 ∈ V → ( I ↾ ℕ0 ) = ( 0g ‘ 𝑀 ) )
33	31 32	ax-mp	⊢ ( I ↾ ℕ0 ) = ( 0g ‘ 𝑀 )
34		mptresid	⊢ ( I ↾ ℕ0 ) = ( 𝑦 ∈ ℕ0 ↦ 𝑦 )
35	3 33 34	3eqtr2ri	⊢ ( 𝑦 ∈ ℕ0 ↦ 𝑦 ) = 0
36	30 35	eqtri	⊢ ( 𝑦 ∈ ℕ0 ↦ ( ( 2 · 𝑦 ) / 2 ) ) = 0
37	24 36	eqtri	⊢ ( 𝑦 ∈ ℕ0 ↦ if ( 2 ∥ ( 2 · 𝑦 ) , ( ( 2 · 𝑦 ) / 2 ) , 𝑁 ) ) = 0
38	18 37	eqtri	⊢ ( 𝐻 ∘ 𝐷 ) = 0