Theorem hashxplem

Description: Lemma for hashxp . (Contributed by Paul Chapman, 30-Nov-2012)

	Ref	Expression
Hypothesis	hashxplem.1	$$⊢B\in \mathrm{Fin}$$
Assertion	hashxplem	$$⊢A\in \mathrm{Fin}\to \left|A\times B\right|=\left|A\right|\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		hashxplem.1	$$⊢B\in \mathrm{Fin}$$
2		xpeq1	$$⊢x=\varnothing \to x\times B=\varnothing \times B$$
3	2	fveq2d	$$⊢x=\varnothing \to \left|x\times B\right|=\left|\varnothing \times B\right|$$
4		fveq2	$$⊢x=\varnothing \to \left|x\right|=\left|\varnothing \right|$$
5	4	oveq1d	$$⊢x=\varnothing \to \left|x\right|\left|B\right|=\left|\varnothing \right|\left|B\right|$$
6	3 5	eqeq12d	$$⊢x=\varnothing \to \left(\left|x\times B\right|=\left|x\right|\left|B\right|\leftrightarrow \left|\varnothing \times B\right|=\left|\varnothing \right|\left|B\right|\right)$$
7		xpeq1	$$⊢x=y\to x\times B=y\times B$$
8	7	fveq2d	$$⊢x=y\to \left|x\times B\right|=\left|y\times B\right|$$
9		fveq2	$$⊢x=y\to \left|x\right|=\left|y\right|$$
10	9	oveq1d	$$⊢x=y\to \left|x\right|\left|B\right|=\left|y\right|\left|B\right|$$
11	8 10	eqeq12d	$$⊢x=y\to \left(\left|x\times B\right|=\left|x\right|\left|B\right|\leftrightarrow \left|y\times B\right|=\left|y\right|\left|B\right|\right)$$
12		xpeq1	$$⊢x=y\cup \left\{z\right\}\to x\times B=\left(y\cup \left\{z\right\}\right)\times B$$
13	12	fveq2d	$$⊢x=y\cup \left\{z\right\}\to \left|x\times B\right|=\left|\left(y\cup \left\{z\right\}\right)\times B\right|$$
14		fveq2	$$⊢x=y\cup \left\{z\right\}\to \left|x\right|=\left|y\cup \left\{z\right\}\right|$$
15	14	oveq1d	$$⊢x=y\cup \left\{z\right\}\to \left|x\right|\left|B\right|=\left|y\cup \left\{z\right\}\right|\left|B\right|$$
16	13 15	eqeq12d	$$⊢x=y\cup \left\{z\right\}\to \left(\left|x\times B\right|=\left|x\right|\left|B\right|\leftrightarrow \left|\left(y\cup \left\{z\right\}\right)\times B\right|=\left|y\cup \left\{z\right\}\right|\left|B\right|\right)$$
17		xpeq1	$$⊢x=A\to x\times B=A\times B$$
18	17	fveq2d	$$⊢x=A\to \left|x\times B\right|=\left|A\times B\right|$$
19		fveq2	$$⊢x=A\to \left|x\right|=\left|A\right|$$
20	19	oveq1d	$$⊢x=A\to \left|x\right|\left|B\right|=\left|A\right|\left|B\right|$$
21	18 20	eqeq12d	$$⊢x=A\to \left(\left|x\times B\right|=\left|x\right|\left|B\right|\leftrightarrow \left|A\times B\right|=\left|A\right|\left|B\right|\right)$$
22		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
23	22	nn0cnd	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in ℂ$$
24	23	mul02d	$$⊢B\in \mathrm{Fin}\to 0\cdot \left|B\right|=0$$
25	1 24	ax-mp	$$⊢0\cdot \left|B\right|=0$$
26		hash0	$$⊢\left|\varnothing \right|=0$$
27	26	oveq1i	$$⊢\left|\varnothing \right|\left|B\right|=0\cdot \left|B\right|$$
28		0xp	$$⊢\varnothing \times B=\varnothing$$
29	28	fveq2i	$$⊢\left|\varnothing \times B\right|=\left|\varnothing \right|$$
30	29 26	eqtri	$$⊢\left|\varnothing \times B\right|=0$$
31	25 27 30	3eqtr4ri	$$⊢\left|\varnothing \times B\right|=\left|\varnothing \right|\left|B\right|$$
32		oveq1	$$⊢\left|y\times B\right|=\left|y\right|\left|B\right|\to \left|y\times B\right|+\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
33	32	adantl	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge \left|y\times B\right|=\left|y\right|\left|B\right|\right)\to \left|y\times B\right|+\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
34		xpundir	$$⊢\left(y\cup \left\{z\right\}\right)\times B=\left(y\times B\right)\cup \left(\left\{z\right\}\times B\right)$$
35	34	fveq2i	$$⊢\left|\left(y\cup \left\{z\right\}\right)\times B\right|=\left|\left(y\times B\right)\cup \left(\left\{z\right\}\times B\right)\right|$$
36		xpfi	$$⊢\left(y\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to y\times B\in \mathrm{Fin}$$
37	1 36	mpan2	$$⊢y\in \mathrm{Fin}\to y\times B\in \mathrm{Fin}$$
38		inxp	$$⊢\left(y\times B\right)\cap \left(\left\{z\right\}\times B\right)=\left(y\cap \left\{z\right\}\right)\times \left(B\cap B\right)$$
39		disjsn	$$⊢y\cap \left\{z\right\}=\varnothing \leftrightarrow \neg z\in y$$
40	39	biimpri	$$⊢\neg z\in y\to y\cap \left\{z\right\}=\varnothing$$
41	40	xpeq1d	$$⊢\neg z\in y\to \left(y\cap \left\{z\right\}\right)\times \left(B\cap B\right)=\varnothing \times \left(B\cap B\right)$$
42		0xp	$$⊢\varnothing \times \left(B\cap B\right)=\varnothing$$
43	41 42	eqtrdi	$$⊢\neg z\in y\to \left(y\cap \left\{z\right\}\right)\times \left(B\cap B\right)=\varnothing$$
44	38 43	eqtrid	$$⊢\neg z\in y\to \left(y\times B\right)\cap \left(\left\{z\right\}\times B\right)=\varnothing$$
45		snfi	$$⊢\left\{z\right\}\in \mathrm{Fin}$$
46		xpfi	$$⊢\left(\left\{z\right\}\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left\{z\right\}\times B\in \mathrm{Fin}$$
47	45 1 46	mp2an	$$⊢\left\{z\right\}\times B\in \mathrm{Fin}$$
48		hashun	$$⊢\left(y\times B\in \mathrm{Fin}\wedge \left\{z\right\}\times B\in \mathrm{Fin}\wedge \left(y\times B\right)\cap \left(\left\{z\right\}\times B\right)=\varnothing \right)\to \left|\left(y\times B\right)\cup \left(\left\{z\right\}\times B\right)\right|=\left|y\times B\right|+\left|\left\{z\right\}\times B\right|$$
49	47 48	mp3an2	$$⊢\left(y\times B\in \mathrm{Fin}\wedge \left(y\times B\right)\cap \left(\left\{z\right\}\times B\right)=\varnothing \right)\to \left|\left(y\times B\right)\cup \left(\left\{z\right\}\times B\right)\right|=\left|y\times B\right|+\left|\left\{z\right\}\times B\right|$$
50	37 44 49	syl2an	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|\left(y\times B\right)\cup \left(\left\{z\right\}\times B\right)\right|=\left|y\times B\right|+\left|\left\{z\right\}\times B\right|$$
51		snex	$$⊢\left\{z\right\}\in \mathrm{V}$$
52	1	elexi	$$⊢B\in \mathrm{V}$$
53	51 52	xpcomen	$$⊢\left(\left\{z\right\}\times B\right)\approx \left(B\times \left\{z\right\}\right)$$
54		vex	$$⊢z\in \mathrm{V}$$
55	52 54	xpsnen	$$⊢\left(B\times \left\{z\right\}\right)\approx B$$
56	53 55	entri	$$⊢\left(\left\{z\right\}\times B\right)\approx B$$
57		hashen	$$⊢\left(\left\{z\right\}\times B\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|\left\{z\right\}\times B\right|=\left|B\right|\leftrightarrow \left(\left\{z\right\}\times B\right)\approx B\right)$$
58	47 1 57	mp2an	$$⊢\left|\left\{z\right\}\times B\right|=\left|B\right|\leftrightarrow \left(\left\{z\right\}\times B\right)\approx B$$
59	56 58	mpbir	$$⊢\left|\left\{z\right\}\times B\right|=\left|B\right|$$
60	59	oveq2i	$$⊢\left|y\times B\right|+\left|\left\{z\right\}\times B\right|=\left|y\times B\right|+\left|B\right|$$
61	50 60	eqtrdi	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|\left(y\times B\right)\cup \left(\left\{z\right\}\times B\right)\right|=\left|y\times B\right|+\left|B\right|$$
62	35 61	eqtrid	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|\left(y\cup \left\{z\right\}\right)\times B\right|=\left|y\times B\right|+\left|B\right|$$
63	62	adantr	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge \left|y\times B\right|=\left|y\right|\left|B\right|\right)\to \left|\left(y\cup \left\{z\right\}\right)\times B\right|=\left|y\times B\right|+\left|B\right|$$
64		hashunsng	$$⊢z\in \mathrm{V}\to \left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|y\cup \left\{z\right\}\right|=\left|y\right|+1\right)$$
65	54 64	ax-mp	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|y\cup \left\{z\right\}\right|=\left|y\right|+1$$
66	65	oveq1d	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|y\cup \left\{z\right\}\right|\left|B\right|=\left(\left|y\right|+1\right)\left|B\right|$$
67		hashcl	$$⊢y\in \mathrm{Fin}\to \left|y\right|\in {\mathbb{N}}_0$$
68	67	nn0cnd	$$⊢y\in \mathrm{Fin}\to \left|y\right|\in ℂ$$
69		ax-1cn	$$⊢1\in ℂ$$
70		nn0cn	$$⊢\left|B\right|\in {\mathbb{N}}_0\to \left|B\right|\in ℂ$$
71	1 22 70	mp2b	$$⊢\left|B\right|\in ℂ$$
72		adddir	$$⊢\left(\left|y\right|\in ℂ\wedge 1\in ℂ\wedge \left|B\right|\in ℂ\right)\to \left(\left|y\right|+1\right)\left|B\right|=\left|y\right|\left|B\right|+1\left|B\right|$$
73	69 71 72	mp3an23	$$⊢\left|y\right|\in ℂ\to \left(\left|y\right|+1\right)\left|B\right|=\left|y\right|\left|B\right|+1\left|B\right|$$
74	68 73	syl	$$⊢y\in \mathrm{Fin}\to \left(\left|y\right|+1\right)\left|B\right|=\left|y\right|\left|B\right|+1\left|B\right|$$
75	71	mulid2i	$$⊢1\left|B\right|=\left|B\right|$$
76	75	oveq2i	$$⊢\left|y\right|\left|B\right|+1\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
77	74 76	eqtrdi	$$⊢y\in \mathrm{Fin}\to \left(\left|y\right|+1\right)\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
78	77	adantr	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left(\left|y\right|+1\right)\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
79	66 78	eqtrd	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left|y\cup \left\{z\right\}\right|\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
80	79	adantr	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge \left|y\times B\right|=\left|y\right|\left|B\right|\right)\to \left|y\cup \left\{z\right\}\right|\left|B\right|=\left|y\right|\left|B\right|+\left|B\right|$$
81	33 63 80	3eqtr4d	$$⊢\left(\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\wedge \left|y\times B\right|=\left|y\right|\left|B\right|\right)\to \left|\left(y\cup \left\{z\right\}\right)\times B\right|=\left|y\cup \left\{z\right\}\right|\left|B\right|$$
82	81	ex	$$⊢\left(y\in \mathrm{Fin}\wedge \neg z\in y\right)\to \left(\left|y\times B\right|=\left|y\right|\left|B\right|\to \left|\left(y\cup \left\{z\right\}\right)\times B\right|=\left|y\cup \left\{z\right\}\right|\left|B\right|\right)$$
83	6 11 16 21 31 82	findcard2s	$$⊢A\in \mathrm{Fin}\to \left|A\times B\right|=\left|A\right|\left|B\right|$$