This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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