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 
|- M = ( EndoFMnd ` NN0 )
smndex2dbas.b 
|- B = ( Base ` M )
smndex2dbas.0 
|- .0. = ( 0g ` M )
smndex2dbas.d 
|- D = ( x e. NN0 |-> ( 2 x. x ) )
smndex2hbas.n 
|- N e. NN0
smndex2hbas.h 
|- H = ( x e. NN0 |-> if ( 2 || x , ( x / 2 ) , N ) )
Assertion smndex2dlinvh 
|- ( H o. D ) = .0.

Proof

Step Hyp Ref Expression
1 smndex2dbas.m 
 |-  M = ( EndoFMnd ` NN0 )
2 smndex2dbas.b 
 |-  B = ( Base ` M )
3 smndex2dbas.0 
 |-  .0. = ( 0g ` M )
4 smndex2dbas.d 
 |-  D = ( x e. NN0 |-> ( 2 x. x ) )
5 smndex2hbas.n 
 |-  N e. NN0
6 smndex2hbas.h 
 |-  H = ( x e. NN0 |-> if ( 2 || x , ( x / 2 ) , N ) )
7 2nn0 
 |-  2 e. NN0
8 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ y e. NN0 ) -> ( 2 x. y ) e. NN0 )
9 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
10 9 cbvmptv 
 |-  ( x e. NN0 |-> ( 2 x. x ) ) = ( y e. NN0 |-> ( 2 x. y ) )
11 4 10 eqtri 
 |-  D = ( y e. NN0 |-> ( 2 x. y ) )
12 11 a1i 
 |-  ( 2 e. NN0 -> D = ( y e. NN0 |-> ( 2 x. y ) ) )
13 6 a1i 
 |-  ( 2 e. NN0 -> H = ( x e. NN0 |-> if ( 2 || x , ( x / 2 ) , N ) ) )
14 breq2 
 |-  ( x = ( 2 x. y ) -> ( 2 || x <-> 2 || ( 2 x. y ) ) )
15 oveq1 
 |-  ( x = ( 2 x. y ) -> ( x / 2 ) = ( ( 2 x. y ) / 2 ) )
16 14 15 ifbieq1d 
 |-  ( x = ( 2 x. y ) -> if ( 2 || x , ( x / 2 ) , N ) = if ( 2 || ( 2 x. y ) , ( ( 2 x. y ) / 2 ) , N ) )
17 8 12 13 16 fmptco 
 |-  ( 2 e. NN0 -> ( H o. D ) = ( y e. NN0 |-> if ( 2 || ( 2 x. y ) , ( ( 2 x. y ) / 2 ) , N ) ) )
18 7 17 ax-mp 
 |-  ( H o. D ) = ( y e. NN0 |-> if ( 2 || ( 2 x. y ) , ( ( 2 x. y ) / 2 ) , N ) )
19 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
20 eqidd 
 |-  ( y e. NN0 -> ( 2 x. y ) = ( 2 x. y ) )
21 2teven 
 |-  ( ( y e. ZZ /\ ( 2 x. y ) = ( 2 x. y ) ) -> 2 || ( 2 x. y ) )
22 19 20 21 syl2anc 
 |-  ( y e. NN0 -> 2 || ( 2 x. y ) )
23 22 iftrued 
 |-  ( y e. NN0 -> if ( 2 || ( 2 x. y ) , ( ( 2 x. y ) / 2 ) , N ) = ( ( 2 x. y ) / 2 ) )
24 23 mpteq2ia 
 |-  ( y e. NN0 |-> if ( 2 || ( 2 x. y ) , ( ( 2 x. y ) / 2 ) , N ) ) = ( y e. NN0 |-> ( ( 2 x. y ) / 2 ) )
25 nn0cn 
 |-  ( y e. NN0 -> y e. CC )
26 2cnd 
 |-  ( y e. NN0 -> 2 e. CC )
27 2ne0 
 |-  2 =/= 0
28 27 a1i 
 |-  ( y e. NN0 -> 2 =/= 0 )
29 25 26 28 divcan3d 
 |-  ( y e. NN0 -> ( ( 2 x. y ) / 2 ) = y )
30 29 mpteq2ia 
 |-  ( y e. NN0 |-> ( ( 2 x. y ) / 2 ) ) = ( y e. NN0 |-> y )
31 nn0ex 
 |-  NN0 e. _V
32 1 efmndid 
 |-  ( NN0 e. _V -> ( _I |` NN0 ) = ( 0g ` M ) )
33 31 32 ax-mp 
 |-  ( _I |` NN0 ) = ( 0g ` M )
34 mptresid 
 |-  ( _I |` NN0 ) = ( y e. NN0 |-> y )
35 3 33 34 3eqtr2ri 
 |-  ( y e. NN0 |-> y ) = .0.
36 30 35 eqtri 
 |-  ( y e. NN0 |-> ( ( 2 x. y ) / 2 ) ) = .0.
37 24 36 eqtri 
 |-  ( y e. NN0 |-> if ( 2 || ( 2 x. y ) , ( ( 2 x. y ) / 2 ) , N ) ) = .0.
38 18 37 eqtri 
 |-  ( H o. D ) = .0.