hashmap

Description: The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014) (Proof shortened by AV, 18-Jul-2022)

		Ref	Expression
	Assertion	hashmap	$⊢ (A \in Fin \land B \in Fin) \to \|A^{B}\| = {\|A\|}^{\|B\|}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to A^{x} = A^{\emptyset}$
2	1	fveq2d	$⊢ x = \emptyset \to \|A^{x}\| = \|A^{\emptyset}\|$
3		fveq2	$⊢ x = \emptyset \to \|x\| = \|\emptyset\|$
4	3	oveq2d	$⊢ x = \emptyset \to {\|A\|}^{\|x\|} = {\|A\|}^{\|\emptyset\|}$
5	2 4	eqeq12d	$⊢ x = \emptyset \to (\|A^{x}\| = {\|A\|}^{\|x\|} \leftrightarrow \|A^{\emptyset}\| = {\|A\|}^{\|\emptyset\|})$
6	5	imbi2d	$⊢ x = \emptyset \to ((A \in Fin \to \|A^{x}\| = {\|A\|}^{\|x\|}) \leftrightarrow (A \in Fin \to \|A^{\emptyset}\| = {\|A\|}^{\|\emptyset\|}))$
7		oveq2	$⊢ x = y \to A^{x} = A^{y}$
8	7	fveq2d	$⊢ x = y \to \|A^{x}\| = \|A^{y}\|$
9		fveq2	$⊢ x = y \to \|x\| = \|y\|$
10	9	oveq2d	$⊢ x = y \to {\|A\|}^{\|x\|} = {\|A\|}^{\|y\|}$
11	8 10	eqeq12d	$⊢ x = y \to (\|A^{x}\| = {\|A\|}^{\|x\|} \leftrightarrow \|A^{y}\| = {\|A\|}^{\|y\|})$
12	11	imbi2d	$⊢ x = y \to ((A \in Fin \to \|A^{x}\| = {\|A\|}^{\|x\|}) \leftrightarrow (A \in Fin \to \|A^{y}\| = {\|A\|}^{\|y\|}))$
13		oveq2	$⊢ x = y \cup \{z\} \to A^{x} = A^{(y \cup \{z\})}$
14	13	fveq2d	$⊢ x = y \cup \{z\} \to \|A^{x}\| = \|A^{(y \cup \{z\})}\|$
15		fveq2	$⊢ x = y \cup \{z\} \to \|x\| = \|y \cup \{z\}\|$
16	15	oveq2d	$⊢ x = y \cup \{z\} \to {\|A\|}^{\|x\|} = {\|A\|}^{\|y \cup \{z\}\|}$
17	14 16	eqeq12d	$⊢ x = y \cup \{z\} \to (\|A^{x}\| = {\|A\|}^{\|x\|} \leftrightarrow \|A^{(y \cup \{z\})}\| = {\|A\|}^{\|y \cup \{z\}\|})$
18	17	imbi2d	$⊢ x = y \cup \{z\} \to ((A \in Fin \to \|A^{x}\| = {\|A\|}^{\|x\|}) \leftrightarrow (A \in Fin \to \|A^{(y \cup \{z\})}\| = {\|A\|}^{\|y \cup \{z\}\|}))$
19		oveq2	$⊢ x = B \to A^{x} = A^{B}$
20	19	fveq2d	$⊢ x = B \to \|A^{x}\| = \|A^{B}\|$
21		fveq2	$⊢ x = B \to \|x\| = \|B\|$
22	21	oveq2d	$⊢ x = B \to {\|A\|}^{\|x\|} = {\|A\|}^{\|B\|}$
23	20 22	eqeq12d	$⊢ x = B \to (\|A^{x}\| = {\|A\|}^{\|x\|} \leftrightarrow \|A^{B}\| = {\|A\|}^{\|B\|})$
24	23	imbi2d	$⊢ x = B \to ((A \in Fin \to \|A^{x}\| = {\|A\|}^{\|x\|}) \leftrightarrow (A \in Fin \to \|A^{B}\| = {\|A\|}^{\|B\|}))$
25		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
26	25	nn0cnd	$⊢ A \in Fin \to \|A\| \in ℂ$
27	26	exp0d	$⊢ A \in Fin \to {\|A\|}^{0} = 1$
28		hash0	$⊢ \|\emptyset\| = 0$
29	28	oveq2i	$⊢ {\|A\|}^{\|\emptyset\|} = {\|A\|}^{0}$
30	29	a1i	$⊢ A \in Fin \to {\|A\|}^{\|\emptyset\|} = {\|A\|}^{0}$
31		mapdm0	$⊢ A \in Fin \to A^{\emptyset} = \{\emptyset\}$
32	31	fveq2d	$⊢ A \in Fin \to \|A^{\emptyset}\| = \|\{\emptyset\}\|$
33		0ex	$⊢ \emptyset \in V$
34		hashsng	$⊢ \emptyset \in V \to \|\{\emptyset\}\| = 1$
35	33 34	mp1i	$⊢ A \in Fin \to \|\{\emptyset\}\| = 1$
36	32 35	eqtrd	$⊢ A \in Fin \to \|A^{\emptyset}\| = 1$
37	27 30 36	3eqtr4rd	$⊢ A \in Fin \to \|A^{\emptyset}\| = {\|A\|}^{\|\emptyset\|}$
38		oveq1	$⊢ \|A^{y}\| = {\|A\|}^{\|y\|} \to \|A^{y}\| \|A\| = {\|A\|}^{\|y\|} \|A\|$
39		vex	$⊢ y \in V$
40	39	a1i	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to y \in V$
41		vsnex	$⊢ \{z\} \in V$
42	41	a1i	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \{z\} \in V$
43		elex	$⊢ A \in Fin \to A \in V$
44	43	adantr	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to A \in V$
45		simprr	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \neg z \in y$
46		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
47	45 46	sylibr	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to y \cap \{z\} = \emptyset$
48		mapunen	$⊢ ((y \in V \land \{z\} \in V \land A \in V) \land y \cap \{z\} = \emptyset) \to (A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}}))$
49	40 42 44 47 48	syl31anc	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}}))$
50		simpl	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to A \in Fin$
51		simprl	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to y \in Fin$
52		snfi	$⊢ \{z\} \in Fin$
53		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
54	51 52 53	sylancl	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to y \cup \{z\} \in Fin$
55		mapfi	$⊢ (A \in Fin \land y \cup \{z\} \in Fin) \to A^{(y \cup \{z\})} \in Fin$
56	50 54 55	syl2anc	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to A^{(y \cup \{z\})} \in Fin$
57		mapfi	$⊢ (A \in Fin \land y \in Fin) \to A^{y} \in Fin$
58	57	adantrr	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to A^{y} \in Fin$
59		mapfi	$⊢ (A \in Fin \land \{z\} \in Fin) \to A^{\{z\}} \in Fin$
60	50 52 59	sylancl	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to A^{\{z\}} \in Fin$
61		xpfi	$⊢ (A^{y} \in Fin \land A^{\{z\}} \in Fin) \to (A^{y}) \times (A^{\{z\}}) \in Fin$
62	58 60 61	syl2anc	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (A^{y}) \times (A^{\{z\}}) \in Fin$
63		hashen	$⊢ (A^{(y \cup \{z\})} \in Fin \land (A^{y}) \times (A^{\{z\}}) \in Fin) \to (\|A^{(y \cup \{z\})}\| = \|(A^{y}) \times (A^{\{z\}})\| \leftrightarrow (A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}})))$
64	56 62 63	syl2anc	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (\|A^{(y \cup \{z\})}\| = \|(A^{y}) \times (A^{\{z\}})\| \leftrightarrow (A^{(y \cup \{z\})}) \approx ((A^{y}) \times (A^{\{z\}})))$
65	49 64	mpbird	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|A^{(y \cup \{z\})}\| = \|(A^{y}) \times (A^{\{z\}})\|$
66		hashxp	$⊢ (A^{y} \in Fin \land A^{\{z\}} \in Fin) \to \|(A^{y}) \times (A^{\{z\}})\| = \|A^{y}\| \|A^{\{z\}}\|$
67	58 60 66	syl2anc	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|(A^{y}) \times (A^{\{z\}})\| = \|A^{y}\| \|A^{\{z\}}\|$
68		vex	$⊢ z \in V$
69	68	a1i	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to z \in V$
70	50 69	mapsnend	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (A^{\{z\}}) \approx A$
71		hashen	$⊢ (A^{\{z\}} \in Fin \land A \in Fin) \to (\|A^{\{z\}}\| = \|A\| \leftrightarrow (A^{\{z\}}) \approx A)$
72	60 50 71	syl2anc	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (\|A^{\{z\}}\| = \|A\| \leftrightarrow (A^{\{z\}}) \approx A)$
73	70 72	mpbird	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|A^{\{z\}}\| = \|A\|$
74	73	oveq2d	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|A^{y}\| \|A^{\{z\}}\| = \|A^{y}\| \|A\|$
75	65 67 74	3eqtrd	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|A^{(y \cup \{z\})}\| = \|A^{y}\| \|A\|$
76		hashunsng	$⊢ z \in V \to ((y \in Fin \land \neg z \in y) \to \|y \cup \{z\}\| = \|y\| + 1)$
77	76	elv	$⊢ (y \in Fin \land \neg z \in y) \to \|y \cup \{z\}\| = \|y\| + 1$
78	77	adantl	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|y \cup \{z\}\| = \|y\| + 1$
79	78	oveq2d	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to {\|A\|}^{\|y \cup \{z\}\|} = {\|A\|}^{\|y\| + 1}$
80	26	adantr	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|A\| \in ℂ$
81		hashcl	$⊢ y \in Fin \to \|y\| \in ℕ_{0}$
82	81	ad2antrl	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to \|y\| \in ℕ_{0}$
83	80 82	expp1d	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to {\|A\|}^{\|y\| + 1} = {\|A\|}^{\|y\|} \|A\|$
84	79 83	eqtrd	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to {\|A\|}^{\|y \cup \{z\}\|} = {\|A\|}^{\|y\|} \|A\|$
85	75 84	eqeq12d	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (\|A^{(y \cup \{z\})}\| = {\|A\|}^{\|y \cup \{z\}\|} \leftrightarrow \|A^{y}\| \|A\| = {\|A\|}^{\|y\|} \|A\|)$
86	38 85	imbitrrid	$⊢ (A \in Fin \land (y \in Fin \land \neg z \in y)) \to (\|A^{y}\| = {\|A\|}^{\|y\|} \to \|A^{(y \cup \{z\})}\| = {\|A\|}^{\|y \cup \{z\}\|})$
87	86	expcom	$⊢ (y \in Fin \land \neg z \in y) \to (A \in Fin \to (\|A^{y}\| = {\|A\|}^{\|y\|} \to \|A^{(y \cup \{z\})}\| = {\|A\|}^{\|y \cup \{z\}\|}))$
88	87	a2d	$⊢ (y \in Fin \land \neg z \in y) \to ((A \in Fin \to \|A^{y}\| = {\|A\|}^{\|y\|}) \to (A \in Fin \to \|A^{(y \cup \{z\})}\| = {\|A\|}^{\|y \cup \{z\}\|}))$
89	6 12 18 24 37 88	findcard2s	$⊢ B \in Fin \to (A \in Fin \to \|A^{B}\| = {\|A\|}^{\|B\|})$
90	89	impcom	$⊢ (A \in Fin \land B \in Fin) \to \|A^{B}\| = {\|A\|}^{\|B\|}$

Metamath Proof Explorer

Theorem hashmap

Proof