hashxplem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > hashxplem		Structured version Visualization version GIF version

Theorem hashxplem 13220

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

**Hypothesis**
Ref	Expression
hashxplem.1	⊢ 𝐵 ∈ Fin

**Assertion**
Ref	Expression
hashxplem	⊢ (𝐴 ∈ Fin → (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵)))

Proof of Theorem hashxplem Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpeq1 5128	. . . 4 ⊢ (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
2	1	fveq2d 6195	. . 3 ⊢ (𝑥 = ∅ → (#‘(𝑥 × 𝐵)) = (#‘(∅ × 𝐵)))
3		fveq2 6191	. . . 4 ⊢ (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
4	3	oveq1d 6665	. . 3 ⊢ (𝑥 = ∅ → ((#‘𝑥) · (#‘𝐵)) = ((#‘∅) · (#‘𝐵)))
5	2, 4	eqeq12d 2637	. 2 ⊢ (𝑥 = ∅ → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘(∅ × 𝐵)) = ((#‘∅) · (#‘𝐵))))
6		xpeq1 5128	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
7	6	fveq2d 6195	. . 3 ⊢ (𝑥 = 𝑦 → (#‘(𝑥 × 𝐵)) = (#‘(𝑦 × 𝐵)))
8		fveq2 6191	. . . 4 ⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
9	8	oveq1d 6665	. . 3 ⊢ (𝑥 = 𝑦 → ((#‘𝑥) · (#‘𝐵)) = ((#‘𝑦) · (#‘𝐵)))
10	7, 9	eqeq12d 2637	. 2 ⊢ (𝑥 = 𝑦 → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))))
11		xpeq1 5128	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∪ {𝑧}) × 𝐵))
12	11	fveq2d 6195	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑥 × 𝐵)) = (#‘((𝑦 ∪ {𝑧}) × 𝐵)))
13		fveq2 6191	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑧})))
14	13	oveq1d 6665	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑥) · (#‘𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)))
15	12, 14	eqeq12d 2637	. 2 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵))))
16		xpeq1 5128	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
17	16	fveq2d 6195	. . 3 ⊢ (𝑥 = 𝐴 → (#‘(𝑥 × 𝐵)) = (#‘(𝐴 × 𝐵)))
18		fveq2 6191	. . . 4 ⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴))
19	18	oveq1d 6665	. . 3 ⊢ (𝑥 = 𝐴 → ((#‘𝑥) · (#‘𝐵)) = ((#‘𝐴) · (#‘𝐵)))
20	17, 19	eqeq12d 2637	. 2 ⊢ (𝑥 = 𝐴 → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵))))
21		hashxplem.1	. . . 4 ⊢ 𝐵 ∈ Fin
22		hashcl 13147	. . . . . 6 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ₀)
23	22	nn0cnd 11353	. . . . 5 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℂ)
24	23	mul02d 10234	. . . 4 ⊢ (𝐵 ∈ Fin → (0 · (#‘𝐵)) = 0)
25	21, 24	ax-mp 5	. . 3 ⊢ (0 · (#‘𝐵)) = 0
26		hash0 13158	. . . 4 ⊢ (#‘∅) = 0
27	26	oveq1i 6660	. . 3 ⊢ ((#‘∅) · (#‘𝐵)) = (0 · (#‘𝐵))
28		0xp 5199	. . . . 5 ⊢ (∅ × 𝐵) = ∅
29	28	fveq2i 6194	. . . 4 ⊢ (#‘(∅ × 𝐵)) = (#‘∅)
30	29, 26	eqtri 2644	. . 3 ⊢ (#‘(∅ × 𝐵)) = 0
31	25, 27, 30	3eqtr4ri 2655	. 2 ⊢ (#‘(∅ × 𝐵)) = ((#‘∅) · (#‘𝐵))
32		oveq1 6657	. . . . 5 ⊢ ((#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵)) → ((#‘(𝑦 × 𝐵)) + (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
33	32	adantl 482	. . . 4 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → ((#‘(𝑦 × 𝐵)) + (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
34		xpundir 5172	. . . . . . 7 ⊢ ((𝑦 ∪ {𝑧}) × 𝐵) = ((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))
35	34	fveq2i 6194	. . . . . 6 ⊢ (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵)))
36		xpfi 8231	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)
37	21, 36	mpan2 707	. . . . . . . 8 ⊢ (𝑦 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)
38		inxp 5254	. . . . . . . . 9 ⊢ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵))
39		disjsn 4246	. . . . . . . . . . . 12 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
40	39	biimpri 218	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ 𝑦 → (𝑦 ∩ {𝑧}) = ∅)
41	40	xpeq1d 5138	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = (∅ × (𝐵 ∩ 𝐵)))
42		0xp 5199	. . . . . . . . . 10 ⊢ (∅ × (𝐵 ∩ 𝐵)) = ∅
43	41, 42	syl6eq 2672	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = ∅)
44	38, 43	syl5eq 2668	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅)
45		snfi 8038	. . . . . . . . . 10 ⊢ {𝑧} ∈ Fin
46		xpfi 8231	. . . . . . . . . 10 ⊢ (({𝑧} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ∈ Fin)
47	45, 21, 46	mp2an 708	. . . . . . . . 9 ⊢ ({𝑧} × 𝐵) ∈ Fin
48		hashun 13171	. . . . . . . . 9 ⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ({𝑧} × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))))
49	47, 48	mp3an2 1412	. . . . . . . 8 ⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))))
50	37, 44, 49	syl2an 494	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))))
51		snex 4908	. . . . . . . . . . 11 ⊢ {𝑧} ∈ V
52	21	elexi 3213	. . . . . . . . . . 11 ⊢ 𝐵 ∈ V
53	51, 52	xpcomen 8051	. . . . . . . . . 10 ⊢ ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧})
54		vex 3203	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
55	52, 54	xpsnen 8044	. . . . . . . . . 10 ⊢ (𝐵 × {𝑧}) ≈ 𝐵
56	53, 55	entri 8010	. . . . . . . . 9 ⊢ ({𝑧} × 𝐵) ≈ 𝐵
57		hashen 13135	. . . . . . . . . 10 ⊢ ((({𝑧} × 𝐵) ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘({𝑧} × 𝐵)) = (#‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵))
58	47, 21, 57	mp2an 708	. . . . . . . . 9 ⊢ ((#‘({𝑧} × 𝐵)) = (#‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵)
59	56, 58	mpbir 221	. . . . . . . 8 ⊢ (#‘({𝑧} × 𝐵)) = (#‘𝐵)
60	59	oveq2i 6661	. . . . . . 7 ⊢ ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵))
61	50, 60	syl6eq 2672	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵)))
62	35, 61	syl5eq 2668	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵)))
63	62	adantr 481	. . . 4 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵)))
64		hashunsng 13181	. . . . . . . 8 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)))
65	54, 64	ax-mp 5	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
66	65	oveq1d 6665	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)) = (((#‘𝑦) + 1) · (#‘𝐵)))
67		hashcl 13147	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ₀)
68	67	nn0cnd 11353	. . . . . . . . 9 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℂ)
69		ax-1cn 9994	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
70		nn0cn 11302	. . . . . . . . . . 11 ⊢ ((#‘𝐵) ∈ ℕ₀ → (#‘𝐵) ∈ ℂ)
71	21, 22, 70	mp2b 10	. . . . . . . . . 10 ⊢ (#‘𝐵) ∈ ℂ
72		adddir 10031	. . . . . . . . . 10 ⊢ (((#‘𝑦) ∈ ℂ ∧ 1 ∈ ℂ ∧ (#‘𝐵) ∈ ℂ) → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))))
73	69, 71, 72	mp3an23 1416	. . . . . . . . 9 ⊢ ((#‘𝑦) ∈ ℂ → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))))
74	68, 73	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ Fin → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))))
75	71	mulid2i 10043	. . . . . . . . 9 ⊢ (1 · (#‘𝐵)) = (#‘𝐵)
76	75	oveq2i 6661	. . . . . . . 8 ⊢ (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵))
77	74, 76	syl6eq 2672	. . . . . . 7 ⊢ (𝑦 ∈ Fin → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
78	77	adantr 481	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
79	66, 78	eqtrd 2656	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
80	79	adantr 481	. . . 4 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
81	33, 63, 80	3eqtr4d 2666	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)))
82	81	ex 450	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵)) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵))))
83	5, 10, 15, 20, 31, 82	findcard2s 8201	1 ⊢ (𝐴 ∈ Fin → (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 Vcvv 3200 ∪ cun 3572 ∩ cin 3573 ∅c0 3915 {csn 4177 class class class wbr 4653 × cxp 5112 ‘cfv 5888 (class class class)co 6650 ≈ cen 7952 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 ℕ₀cn0 11292 #chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-hash 13118

This theorem is referenced by: hashxp 13221

W3C validator