Metamath Proof Explorer

Theorem hashgadd

Description: G maps ordinal addition to integer addition. (Contributed by Paul Chapman, 30-Nov-2012) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis hashgadd.1 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
Assertion hashgadd 
|- ( ( A e. _om /\ B e. _om ) -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) )

Proof

Step Hyp Ref Expression
1 hashgadd.1 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 oveq2 
 |-  ( n = (/) -> ( A +o n ) = ( A +o (/) ) )
3 2 fveq2d 
 |-  ( n = (/) -> ( G ` ( A +o n ) ) = ( G ` ( A +o (/) ) ) )
4 fveq2 
 |-  ( n = (/) -> ( G ` n ) = ( G ` (/) ) )
5 4 oveq2d 
 |-  ( n = (/) -> ( ( G ` A ) + ( G ` n ) ) = ( ( G ` A ) + ( G ` (/) ) ) )
6 3 5 eqeq12d 
 |-  ( n = (/) -> ( ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) <-> ( G ` ( A +o (/) ) ) = ( ( G ` A ) + ( G ` (/) ) ) ) )
7 6 imbi2d 
 |-  ( n = (/) -> ( ( A e. _om -> ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) ) <-> ( A e. _om -> ( G ` ( A +o (/) ) ) = ( ( G ` A ) + ( G ` (/) ) ) ) ) )
8 oveq2 
 |-  ( n = z -> ( A +o n ) = ( A +o z ) )
9 8 fveq2d 
 |-  ( n = z -> ( G ` ( A +o n ) ) = ( G ` ( A +o z ) ) )
10 fveq2 
 |-  ( n = z -> ( G ` n ) = ( G ` z ) )
11 10 oveq2d 
 |-  ( n = z -> ( ( G ` A ) + ( G ` n ) ) = ( ( G ` A ) + ( G ` z ) ) )
12 9 11 eqeq12d 
 |-  ( n = z -> ( ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) <-> ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) )
13 12 imbi2d 
 |-  ( n = z -> ( ( A e. _om -> ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) ) <-> ( A e. _om -> ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) ) )
14 oveq2 
 |-  ( n = suc z -> ( A +o n ) = ( A +o suc z ) )
15 14 fveq2d 
 |-  ( n = suc z -> ( G ` ( A +o n ) ) = ( G ` ( A +o suc z ) ) )
16 fveq2 
 |-  ( n = suc z -> ( G ` n ) = ( G ` suc z ) )
17 16 oveq2d 
 |-  ( n = suc z -> ( ( G ` A ) + ( G ` n ) ) = ( ( G ` A ) + ( G ` suc z ) ) )
18 15 17 eqeq12d 
 |-  ( n = suc z -> ( ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) <-> ( G ` ( A +o suc z ) ) = ( ( G ` A ) + ( G ` suc z ) ) ) )
19 18 imbi2d 
 |-  ( n = suc z -> ( ( A e. _om -> ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) ) <-> ( A e. _om -> ( G ` ( A +o suc z ) ) = ( ( G ` A ) + ( G ` suc z ) ) ) ) )
20 oveq2 
 |-  ( n = B -> ( A +o n ) = ( A +o B ) )
21 20 fveq2d 
 |-  ( n = B -> ( G ` ( A +o n ) ) = ( G ` ( A +o B ) ) )
22 fveq2 
 |-  ( n = B -> ( G ` n ) = ( G ` B ) )
23 22 oveq2d 
 |-  ( n = B -> ( ( G ` A ) + ( G ` n ) ) = ( ( G ` A ) + ( G ` B ) ) )
24 21 23 eqeq12d 
 |-  ( n = B -> ( ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) <-> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) ) )
25 24 imbi2d 
 |-  ( n = B -> ( ( A e. _om -> ( G ` ( A +o n ) ) = ( ( G ` A ) + ( G ` n ) ) ) <-> ( A e. _om -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) ) ) )
26 1 hashgf1o 
 |-  G : _om -1-1-onto-> NN0
27 f1of 
 |-  ( G : _om -1-1-onto-> NN0 -> G : _om --> NN0 )
28 26 27 ax-mp 
 |-  G : _om --> NN0
29 28 ffvelrni 
 |-  ( A e. _om -> ( G ` A ) e. NN0 )
30 29 nn0cnd 
 |-  ( A e. _om -> ( G ` A ) e. CC )
31 30 addid1d 
 |-  ( A e. _om -> ( ( G ` A ) + 0 ) = ( G ` A ) )
32 0z 
 |-  0 e. ZZ
33 32 1 om2uz0i 
 |-  ( G ` (/) ) = 0
34 33 oveq2i 
 |-  ( ( G ` A ) + ( G ` (/) ) ) = ( ( G ` A ) + 0 )
35 34 a1i 
 |-  ( A e. _om -> ( ( G ` A ) + ( G ` (/) ) ) = ( ( G ` A ) + 0 ) )
36 nna0 
 |-  ( A e. _om -> ( A +o (/) ) = A )
37 36 fveq2d 
 |-  ( A e. _om -> ( G ` ( A +o (/) ) ) = ( G ` A ) )
38 31 35 37 3eqtr4rd 
 |-  ( A e. _om -> ( G ` ( A +o (/) ) ) = ( ( G ` A ) + ( G ` (/) ) ) )
39 nnasuc 
 |-  ( ( A e. _om /\ z e. _om ) -> ( A +o suc z ) = suc ( A +o z ) )
40 39 fveq2d 
 |-  ( ( A e. _om /\ z e. _om ) -> ( G ` ( A +o suc z ) ) = ( G ` suc ( A +o z ) ) )
41 nnacl 
 |-  ( ( A e. _om /\ z e. _om ) -> ( A +o z ) e. _om )
42 32 1 om2uzsuci 
 |-  ( ( A +o z ) e. _om -> ( G ` suc ( A +o z ) ) = ( ( G ` ( A +o z ) ) + 1 ) )
43 41 42 syl 
 |-  ( ( A e. _om /\ z e. _om ) -> ( G ` suc ( A +o z ) ) = ( ( G ` ( A +o z ) ) + 1 ) )
44 40 43 eqtrd 
 |-  ( ( A e. _om /\ z e. _om ) -> ( G ` ( A +o suc z ) ) = ( ( G ` ( A +o z ) ) + 1 ) )
45 44 3adant3 
 |-  ( ( A e. _om /\ z e. _om /\ ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( G ` ( A +o suc z ) ) = ( ( G ` ( A +o z ) ) + 1 ) )
46 28 ffvelrni 
 |-  ( z e. _om -> ( G ` z ) e. NN0 )
47 46 nn0cnd 
 |-  ( z e. _om -> ( G ` z ) e. CC )
48 ax-1cn 
 |-  1 e. CC
49 addass 
 |-  ( ( ( G ` A ) e. CC /\ ( G ` z ) e. CC /\ 1 e. CC ) -> ( ( ( G ` A ) + ( G ` z ) ) + 1 ) = ( ( G ` A ) + ( ( G ` z ) + 1 ) ) )
50 48 49 mp3an3 
 |-  ( ( ( G ` A ) e. CC /\ ( G ` z ) e. CC ) -> ( ( ( G ` A ) + ( G ` z ) ) + 1 ) = ( ( G ` A ) + ( ( G ` z ) + 1 ) ) )
51 30 47 50 syl2an 
 |-  ( ( A e. _om /\ z e. _om ) -> ( ( ( G ` A ) + ( G ` z ) ) + 1 ) = ( ( G ` A ) + ( ( G ` z ) + 1 ) ) )
52 51 3adant3 
 |-  ( ( A e. _om /\ z e. _om /\ ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( ( ( G ` A ) + ( G ` z ) ) + 1 ) = ( ( G ` A ) + ( ( G ` z ) + 1 ) ) )
53 oveq1 
 |-  ( ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) -> ( ( G ` ( A +o z ) ) + 1 ) = ( ( ( G ` A ) + ( G ` z ) ) + 1 ) )
54 53 3ad2ant3 
 |-  ( ( A e. _om /\ z e. _om /\ ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( ( G ` ( A +o z ) ) + 1 ) = ( ( ( G ` A ) + ( G ` z ) ) + 1 ) )
55 32 1 om2uzsuci 
 |-  ( z e. _om -> ( G ` suc z ) = ( ( G ` z ) + 1 ) )
56 55 oveq2d 
 |-  ( z e. _om -> ( ( G ` A ) + ( G ` suc z ) ) = ( ( G ` A ) + ( ( G ` z ) + 1 ) ) )
57 56 3ad2ant2 
 |-  ( ( A e. _om /\ z e. _om /\ ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( ( G ` A ) + ( G ` suc z ) ) = ( ( G ` A ) + ( ( G ` z ) + 1 ) ) )
58 52 54 57 3eqtr4d 
 |-  ( ( A e. _om /\ z e. _om /\ ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( ( G ` ( A +o z ) ) + 1 ) = ( ( G ` A ) + ( G ` suc z ) ) )
59 45 58 eqtrd 
 |-  ( ( A e. _om /\ z e. _om /\ ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( G ` ( A +o suc z ) ) = ( ( G ` A ) + ( G ` suc z ) ) )
60 59 3expia 
 |-  ( ( A e. _om /\ z e. _om ) -> ( ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) -> ( G ` ( A +o suc z ) ) = ( ( G ` A ) + ( G ` suc z ) ) ) )
61 60 expcom 
 |-  ( z e. _om -> ( A e. _om -> ( ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) -> ( G ` ( A +o suc z ) ) = ( ( G ` A ) + ( G ` suc z ) ) ) ) )
62 61 a2d 
 |-  ( z e. _om -> ( ( A e. _om -> ( G ` ( A +o z ) ) = ( ( G ` A ) + ( G ` z ) ) ) -> ( A e. _om -> ( G ` ( A +o suc z ) ) = ( ( G ` A ) + ( G ` suc z ) ) ) ) )
63 7 13 19 25 38 62 finds 
 |-  ( B e. _om -> ( A e. _om -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) ) )
64 63 impcom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) )