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={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	hashgadd	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to G\left(A{+}_{𝑜}B\right)=G\left(A\right)+G\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashgadd.1	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
2		oveq2	$$⊢n=\varnothing \to A{+}_{𝑜}n=A{+}_{𝑜}\varnothing$$
3	2	fveq2d	$$⊢n=\varnothing \to G\left(A{+}_{𝑜}n\right)=G\left(A{+}_{𝑜}\varnothing \right)$$
4		fveq2	$$⊢n=\varnothing \to G\left(n\right)=G\left(\varnothing \right)$$
5	4	oveq2d	$$⊢n=\varnothing \to G\left(A\right)+G\left(n\right)=G\left(A\right)+G\left(\varnothing \right)$$
6	3 5	eqeq12d	$$⊢n=\varnothing \to \left(G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\leftrightarrow G\left(A{+}_{𝑜}\varnothing \right)=G\left(A\right)+G\left(\varnothing \right)\right)$$
7	6	imbi2d	$$⊢n=\varnothing \to \left(\left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\right)\leftrightarrow \left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}\varnothing \right)=G\left(A\right)+G\left(\varnothing \right)\right)\right)$$
8		oveq2	$$⊢n=z\to A{+}_{𝑜}n=A{+}_{𝑜}z$$
9	8	fveq2d	$$⊢n=z\to G\left(A{+}_{𝑜}n\right)=G\left(A{+}_{𝑜}z\right)$$
10		fveq2	$$⊢n=z\to G\left(n\right)=G\left(z\right)$$
11	10	oveq2d	$$⊢n=z\to G\left(A\right)+G\left(n\right)=G\left(A\right)+G\left(z\right)$$
12	9 11	eqeq12d	$$⊢n=z\to \left(G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\leftrightarrow G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)$$
13	12	imbi2d	$$⊢n=z\to \left(\left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\right)\leftrightarrow \left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\right)$$
14		oveq2	$$⊢n=\mathrm{suc}z\to A{+}_{𝑜}n=A{+}_{𝑜}\mathrm{suc}z$$
15	14	fveq2d	$$⊢n=\mathrm{suc}z\to G\left(A{+}_{𝑜}n\right)=G\left(A{+}_{𝑜}\mathrm{suc}z\right)$$
16		fveq2	$$⊢n=\mathrm{suc}z\to G\left(n\right)=G\left(\mathrm{suc}z\right)$$
17	16	oveq2d	$$⊢n=\mathrm{suc}z\to G\left(A\right)+G\left(n\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)$$
18	15 17	eqeq12d	$$⊢n=\mathrm{suc}z\to \left(G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\leftrightarrow G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)\right)$$
19	18	imbi2d	$$⊢n=\mathrm{suc}z\to \left(\left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\right)\leftrightarrow \left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)\right)\right)$$
20		oveq2	$$⊢n=B\to A{+}_{𝑜}n=A{+}_{𝑜}B$$
21	20	fveq2d	$$⊢n=B\to G\left(A{+}_{𝑜}n\right)=G\left(A{+}_{𝑜}B\right)$$
22		fveq2	$$⊢n=B\to G\left(n\right)=G\left(B\right)$$
23	22	oveq2d	$$⊢n=B\to G\left(A\right)+G\left(n\right)=G\left(A\right)+G\left(B\right)$$
24	21 23	eqeq12d	$$⊢n=B\to \left(G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\leftrightarrow G\left(A{+}_{𝑜}B\right)=G\left(A\right)+G\left(B\right)\right)$$
25	24	imbi2d	$$⊢n=B\to \left(\left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}n\right)=G\left(A\right)+G\left(n\right)\right)\leftrightarrow \left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}B\right)=G\left(A\right)+G\left(B\right)\right)\right)$$
26	1	hashgf1o	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
27		f1of	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to G:\mathrm{\omega }⟶{\mathbb{N}}_0$$
28	26 27	ax-mp	$$⊢G:\mathrm{\omega }⟶{\mathbb{N}}_0$$
29	28	ffvelrni	$$⊢A\in \mathrm{\omega }\to G\left(A\right)\in {\mathbb{N}}_0$$
30	29	nn0cnd	$$⊢A\in \mathrm{\omega }\to G\left(A\right)\in ℂ$$
31	30	addid1d	$$⊢A\in \mathrm{\omega }\to G\left(A\right)+0=G\left(A\right)$$
32		0z	$$⊢0\in \mathbb{Z}$$
33	32 1	om2uz0i	$$⊢G\left(\varnothing \right)=0$$
34	33	oveq2i	$$⊢G\left(A\right)+G\left(\varnothing \right)=G\left(A\right)+0$$
35	34	a1i	$$⊢A\in \mathrm{\omega }\to G\left(A\right)+G\left(\varnothing \right)=G\left(A\right)+0$$
36		nna0	$$⊢A\in \mathrm{\omega }\to A{+}_{𝑜}\varnothing =A$$
37	36	fveq2d	$$⊢A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}\varnothing \right)=G\left(A\right)$$
38	31 35 37	3eqtr4rd	$$⊢A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}\varnothing \right)=G\left(A\right)+G\left(\varnothing \right)$$
39		nnasuc	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to A{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(A{+}_{𝑜}z\right)$$
40	39	fveq2d	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(\mathrm{suc}\left(A{+}_{𝑜}z\right)\right)$$
41		nnacl	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to A{+}_{𝑜}z\in \mathrm{\omega }$$
42	32 1	om2uzsuci	$$⊢A{+}_{𝑜}z\in \mathrm{\omega }\to G\left(\mathrm{suc}\left(A{+}_{𝑜}z\right)\right)=G\left(A{+}_{𝑜}z\right)+1$$
43	41 42	syl	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to G\left(\mathrm{suc}\left(A{+}_{𝑜}z\right)\right)=G\left(A{+}_{𝑜}z\right)+1$$
44	40 43	eqtrd	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A{+}_{𝑜}z\right)+1$$
45	44	3adant3	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\wedge G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A{+}_{𝑜}z\right)+1$$
46	28	ffvelrni	$$⊢z\in \mathrm{\omega }\to G\left(z\right)\in {\mathbb{N}}_0$$
47	46	nn0cnd	$$⊢z\in \mathrm{\omega }\to G\left(z\right)\in ℂ$$
48		ax-1cn	$$⊢1\in ℂ$$
49		addass	$$⊢\left(G\left(A\right)\in ℂ\wedge G\left(z\right)\in ℂ\wedge 1\in ℂ\right)\to G\left(A\right)+G\left(z\right)+1=G\left(A\right)+G\left(z\right)+1$$
50	48 49	mp3an3	$$⊢\left(G\left(A\right)\in ℂ\wedge G\left(z\right)\in ℂ\right)\to G\left(A\right)+G\left(z\right)+1=G\left(A\right)+G\left(z\right)+1$$
51	30 47 50	syl2an	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to G\left(A\right)+G\left(z\right)+1=G\left(A\right)+G\left(z\right)+1$$
52	51	3adant3	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\wedge G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to G\left(A\right)+G\left(z\right)+1=G\left(A\right)+G\left(z\right)+1$$
53		oveq1	$$⊢G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\to G\left(A{+}_{𝑜}z\right)+1=G\left(A\right)+G\left(z\right)+1$$
54	53	3ad2ant3	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\wedge G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to G\left(A{+}_{𝑜}z\right)+1=G\left(A\right)+G\left(z\right)+1$$
55	32 1	om2uzsuci	$$⊢z\in \mathrm{\omega }\to G\left(\mathrm{suc}z\right)=G\left(z\right)+1$$
56	55	oveq2d	$$⊢z\in \mathrm{\omega }\to G\left(A\right)+G\left(\mathrm{suc}z\right)=G\left(A\right)+G\left(z\right)+1$$
57	56	3ad2ant2	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\wedge G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to G\left(A\right)+G\left(\mathrm{suc}z\right)=G\left(A\right)+G\left(z\right)+1$$
58	52 54 57	3eqtr4d	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\wedge G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to G\left(A{+}_{𝑜}z\right)+1=G\left(A\right)+G\left(\mathrm{suc}z\right)$$
59	45 58	eqtrd	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\wedge G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)$$
60	59	3expia	$$⊢\left(A\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to \left(G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)\right)$$
61	60	expcom	$$⊢z\in \mathrm{\omega }\to \left(A\in \mathrm{\omega }\to \left(G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)\right)\right)$$
62	61	a2d	$$⊢z\in \mathrm{\omega }\to \left(\left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}z\right)=G\left(A\right)+G\left(z\right)\right)\to \left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}\mathrm{suc}z\right)=G\left(A\right)+G\left(\mathrm{suc}z\right)\right)\right)$$
63	7 13 19 25 38 62	finds	$$⊢B\in \mathrm{\omega }\to \left(A\in \mathrm{\omega }\to G\left(A{+}_{𝑜}B\right)=G\left(A\right)+G\left(B\right)\right)$$
64	63	impcom	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to G\left(A{+}_{𝑜}B\right)=G\left(A\right)+G\left(B\right)$$