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 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion hashgadd ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hashgadd.1 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2 oveq2 ⊢ ( 𝑛 = ∅ → ( 𝐴 +o 𝑛 ) = ( 𝐴 +o ∅ ) )
3 2 fveq2d ⊢ ( 𝑛 = ∅ → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( 𝐺 ‘ ( 𝐴 +o ∅ ) ) )
4 fveq2 ⊢ ( 𝑛 = ∅ → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ∅ ) )
5 4 oveq2d ⊢ ( 𝑛 = ∅ → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ ∅ ) ) )
6 3 5 eqeq12d ⊢ ( 𝑛 = ∅ → ( ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐺 ‘ ( 𝐴 +o ∅ ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ ∅ ) ) ) )
7 6 imbi2d ⊢ ( 𝑛 = ∅ → ( ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o ∅ ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ ∅ ) ) ) ) )
8 oveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝐴 +o 𝑛 ) = ( 𝐴 +o 𝑧 ) )
9 8 fveq2d ⊢ ( 𝑛 = 𝑧 → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) )
10 fveq2 ⊢ ( 𝑛 = 𝑧 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑧 ) )
11 10 oveq2d ⊢ ( 𝑛 = 𝑧 → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) )
12 9 11 eqeq12d ⊢ ( 𝑛 = 𝑧 → ( ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) )
13 12 imbi2d ⊢ ( 𝑛 = 𝑧 → ( ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) ) )
14 oveq2 ⊢ ( 𝑛 = suc 𝑧 → ( 𝐴 +o 𝑛 ) = ( 𝐴 +o suc 𝑧 ) )
15 14 fveq2d ⊢ ( 𝑛 = suc 𝑧 → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) )
16 fveq2 ⊢ ( 𝑛 = suc 𝑧 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ suc 𝑧 ) )
17 16 oveq2d ⊢ ( 𝑛 = suc 𝑧 → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) )
18 15 17 eqeq12d ⊢ ( 𝑛 = suc 𝑧 → ( ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) ) )
19 18 imbi2d ⊢ ( 𝑛 = suc 𝑧 → ( ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) ) ) )
20 oveq2 ⊢ ( 𝑛 = 𝐵 → ( 𝐴 +o 𝑛 ) = ( 𝐴 +o 𝐵 ) )
21 20 fveq2d ⊢ ( 𝑛 = 𝐵 → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( 𝐺 ‘ ( 𝐴 +o 𝐵 ) ) )
22 fveq2 ⊢ ( 𝑛 = 𝐵 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝐵 ) )
23 22 oveq2d ⊢ ( 𝑛 = 𝐵 → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝐵 ) ) )
24 21 23 eqeq12d ⊢ ( 𝑛 = 𝐵 → ( ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐺 ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝐵 ) ) ) )
25 24 imbi2d ⊢ ( 𝑛 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝑛 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝐵 ) ) ) ) )
26 1 hashgf1o ⊢ 𝐺 : ω –1-1-onto→ ℕ0
27 f1of ⊢ ( 𝐺 : ω –1-1-onto→ ℕ0 → 𝐺 : ω ⟶ ℕ0 )
28 26 27 ax-mp ⊢ 𝐺 : ω ⟶ ℕ0
29 28 ffvelcdmi ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℕ0 )
30 29 nn0cnd ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℂ )
31 30 addridd ⊢ ( 𝐴 ∈ ω → ( ( 𝐺 ‘ 𝐴 ) + 0 ) = ( 𝐺 ‘ 𝐴 ) )
32 0z ⊢ 0 ∈ ℤ
33 32 1 om2uz0i ⊢ ( 𝐺 ‘ ∅ ) = 0
34 33 oveq2i ⊢ ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ ∅ ) ) = ( ( 𝐺 ‘ 𝐴 ) + 0 )
35 34 a1i ⊢ ( 𝐴 ∈ ω → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ ∅ ) ) = ( ( 𝐺 ‘ 𝐴 ) + 0 ) )
36 nna0 ⊢ ( 𝐴 ∈ ω → ( 𝐴 +o ∅ ) = 𝐴 )
37 36 fveq2d ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o ∅ ) ) = ( 𝐺 ‘ 𝐴 ) )
38 31 35 37 3eqtr4rd ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o ∅ ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ ∅ ) ) )
39 nnasuc ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝐴 +o suc 𝑧 ) = suc ( 𝐴 +o 𝑧 ) )
40 39 fveq2d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( 𝐺 ‘ suc ( 𝐴 +o 𝑧 ) ) )
41 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝐴 +o 𝑧 ) ∈ ω )
42 32 1 om2uzsuci ⊢ ( ( 𝐴 +o 𝑧 ) ∈ ω → ( 𝐺 ‘ suc ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) )
43 41 42 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝐺 ‘ suc ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) )
44 40 43 eqtrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) )
45 44 3adant3 ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) )
46 28 ffvelcdmi ⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ 𝑧 ) ∈ ℕ0 )
47 46 nn0cnd ⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
48 ax-1cn ⊢ 1 ∈ ℂ
49 addass ⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + ( ( 𝐺 ‘ 𝑧 ) + 1 ) ) )
50 48 49 mp3an3 ⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + ( ( 𝐺 ‘ 𝑧 ) + 1 ) ) )
51 30 47 50 syl2an ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + ( ( 𝐺 ‘ 𝑧 ) + 1 ) ) )
52 51 3adant3 ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + ( ( 𝐺 ‘ 𝑧 ) + 1 ) ) )
53 oveq1 ⊢ ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) → ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) = ( ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) + 1 ) )
54 53 3ad2ant3 ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) = ( ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) + 1 ) )
55 32 1 om2uzsuci ⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
56 55 oveq2d ⊢ ( 𝑧 ∈ ω → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( ( 𝐺 ‘ 𝑧 ) + 1 ) ) )
57 56 3ad2ant2 ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( ( 𝐺 ‘ 𝑧 ) + 1 ) ) )
58 52 54 57 3eqtr4d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) )
59 45 58 eqtrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) )
60 59 3expia ⊢ ( ( 𝐴 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) ) )
61 60 expcom ⊢ ( 𝑧 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) ) ) )
62 61 a2d ⊢ ( 𝑧 ∈ ω → ( ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝑧 ) ) ) → ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ suc 𝑧 ) ) ) ) )
63 7 13 19 25 38 62 finds ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝐵 ) ) ) )
64 63 impcom ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝐺 ‘ 𝐴 ) + ( 𝐺 ‘ 𝐵 ) ) )