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 13080

Description: Lemma for hashxp 13081. (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 5052	. . . 4 ⊢ (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵))
2	1	fveq2d 6107	. . 3 ⊢ (𝑥 = ∅ → (#‘(𝑥 × 𝐵)) = (#‘(∅ × 𝐵)))
3		fveq2 6103	. . . 4 ⊢ (𝑥 = ∅ → (#‘𝑥) = (#‘∅))
4	3	oveq1d 6564	. . 3 ⊢ (𝑥 = ∅ → ((#‘𝑥) · (#‘𝐵)) = ((#‘∅) · (#‘𝐵)))
5	2, 4	eqeq12d 2625	. 2 ⊢ (𝑥 = ∅ → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘(∅ × 𝐵)) = ((#‘∅) · (#‘𝐵))))
6		xpeq1 5052	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵))
7	6	fveq2d 6107	. . 3 ⊢ (𝑥 = 𝑦 → (#‘(𝑥 × 𝐵)) = (#‘(𝑦 × 𝐵)))
8		fveq2 6103	. . . 4 ⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
9	8	oveq1d 6564	. . 3 ⊢ (𝑥 = 𝑦 → ((#‘𝑥) · (#‘𝐵)) = ((#‘𝑦) · (#‘𝐵)))
10	7, 9	eqeq12d 2625	. 2 ⊢ (𝑥 = 𝑦 → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))))
11		xpeq1 5052	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∪ {𝑧}) × 𝐵))
12	11	fveq2d 6107	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑥 × 𝐵)) = (#‘((𝑦 ∪ {𝑧}) × 𝐵)))
13		fveq2 6103	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (#‘𝑥) = (#‘(𝑦 ∪ {𝑧})))
14	13	oveq1d 6564	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑥) · (#‘𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)))
15	12, 14	eqeq12d 2625	. 2 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵))))
16		xpeq1 5052	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵))
17	16	fveq2d 6107	. . 3 ⊢ (𝑥 = 𝐴 → (#‘(𝑥 × 𝐵)) = (#‘(𝐴 × 𝐵)))
18		fveq2 6103	. . . 4 ⊢ (𝑥 = 𝐴 → (#‘𝑥) = (#‘𝐴))
19	18	oveq1d 6564	. . 3 ⊢ (𝑥 = 𝐴 → ((#‘𝑥) · (#‘𝐵)) = ((#‘𝐴) · (#‘𝐵)))
20	17, 19	eqeq12d 2625	. 2 ⊢ (𝑥 = 𝐴 → ((#‘(𝑥 × 𝐵)) = ((#‘𝑥) · (#‘𝐵)) ↔ (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵))))
21		hashxplem.1	. . . 4 ⊢ 𝐵 ∈ Fin
22		hashcl 13009	. . . . . 6 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℕ₀)
23	22	nn0cnd 11230	. . . . 5 ⊢ (𝐵 ∈ Fin → (#‘𝐵) ∈ ℂ)
24	23	mul02d 10113	. . . 4 ⊢ (𝐵 ∈ Fin → (0 · (#‘𝐵)) = 0)
25	21, 24	ax-mp 5	. . 3 ⊢ (0 · (#‘𝐵)) = 0
26		hash0 13019	. . . 4 ⊢ (#‘∅) = 0
27	26	oveq1i 6559	. . 3 ⊢ ((#‘∅) · (#‘𝐵)) = (0 · (#‘𝐵))
28		0xp 5122	. . . . 5 ⊢ (∅ × 𝐵) = ∅
29	28	fveq2i 6106	. . . 4 ⊢ (#‘(∅ × 𝐵)) = (#‘∅)
30	29, 26	eqtri 2632	. . 3 ⊢ (#‘(∅ × 𝐵)) = 0
31	25, 27, 30	3eqtr4ri 2643	. 2 ⊢ (#‘(∅ × 𝐵)) = ((#‘∅) · (#‘𝐵))
32		oveq1 6556	. . . . 5 ⊢ ((#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵)) → ((#‘(𝑦 × 𝐵)) + (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
33	32	adantl 481	. . . 4 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → ((#‘(𝑦 × 𝐵)) + (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
34		xpundir 5095	. . . . . . 7 ⊢ ((𝑦 ∪ {𝑧}) × 𝐵) = ((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))
35	34	fveq2i 6106	. . . . . 6 ⊢ (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵)))
36		xpfi 8116	. . . . . . . . 9 ⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑦 × 𝐵) ∈ Fin)
37	21, 36	mpan2 703	. . . . . . . 8 ⊢ (𝑦 ∈ Fin → (𝑦 × 𝐵) ∈ Fin)
38		inxp 5176	. . . . . . . . 9 ⊢ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵))
39		disjsn 4192	. . . . . . . . . . . 12 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
40	39	biimpri 217	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ 𝑦 → (𝑦 ∩ {𝑧}) = ∅)
41	40	xpeq1d 5062	. . . . . . . . . 10 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = (∅ × (𝐵 ∩ 𝐵)))
42		0xp 5122	. . . . . . . . . 10 ⊢ (∅ × (𝐵 ∩ 𝐵)) = ∅
43	41, 42	syl6eq 2660	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = ∅)
44	38, 43	syl5eq 2656	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅)
45		snfi 7923	. . . . . . . . . 10 ⊢ {𝑧} ∈ Fin
46		xpfi 8116	. . . . . . . . . 10 ⊢ (({𝑧} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ∈ Fin)
47	45, 21, 46	mp2an 704	. . . . . . . . 9 ⊢ ({𝑧} × 𝐵) ∈ Fin
48		hashun 13032	. . . . . . . . 9 ⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ({𝑧} × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))))
49	47, 48	mp3an2 1404	. . . . . . . 8 ⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))))
50	37, 44, 49	syl2an 493	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))))
51		snex 4835	. . . . . . . . . . 11 ⊢ {𝑧} ∈ V
52	21	elexi 3186	. . . . . . . . . . 11 ⊢ 𝐵 ∈ V
53	51, 52	xpcomen 7936	. . . . . . . . . 10 ⊢ ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧})
54		vex 3176	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
55	52, 54	xpsnen 7929	. . . . . . . . . 10 ⊢ (𝐵 × {𝑧}) ≈ 𝐵
56	53, 55	entri 7896	. . . . . . . . 9 ⊢ ({𝑧} × 𝐵) ≈ 𝐵
57		hashen 12997	. . . . . . . . . 10 ⊢ ((({𝑧} × 𝐵) ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘({𝑧} × 𝐵)) = (#‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵))
58	47, 21, 57	mp2an 704	. . . . . . . . 9 ⊢ ((#‘({𝑧} × 𝐵)) = (#‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵)
59	56, 58	mpbir 220	. . . . . . . 8 ⊢ (#‘({𝑧} × 𝐵)) = (#‘𝐵)
60	59	oveq2i 6560	. . . . . . 7 ⊢ ((#‘(𝑦 × 𝐵)) + (#‘({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵))
61	50, 60	syl6eq 2660	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵)))
62	35, 61	syl5eq 2656	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵)))
63	62	adantr 480	. . . 4 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 × 𝐵)) + (#‘𝐵)))
64		hashunsng 13042	. . . . . . . 8 ⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1)))
65	54, 64	ax-mp 5	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (#‘(𝑦 ∪ {𝑧})) = ((#‘𝑦) + 1))
66	65	oveq1d 6564	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)) = (((#‘𝑦) + 1) · (#‘𝐵)))
67		hashcl 13009	. . . . . . . . . 10 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℕ₀)
68	67	nn0cnd 11230	. . . . . . . . 9 ⊢ (𝑦 ∈ Fin → (#‘𝑦) ∈ ℂ)
69		ax-1cn 9873	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
70		nn0cn 11179	. . . . . . . . . . 11 ⊢ ((#‘𝐵) ∈ ℕ₀ → (#‘𝐵) ∈ ℂ)
71	21, 22, 70	mp2b 10	. . . . . . . . . 10 ⊢ (#‘𝐵) ∈ ℂ
72		adddir 9910	. . . . . . . . . 10 ⊢ (((#‘𝑦) ∈ ℂ ∧ 1 ∈ ℂ ∧ (#‘𝐵) ∈ ℂ) → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))))
73	69, 71, 72	mp3an23 1408	. . . . . . . . 9 ⊢ ((#‘𝑦) ∈ ℂ → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))))
74	68, 73	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ Fin → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))))
75	71	mulid2i 9922	. . . . . . . . 9 ⊢ (1 · (#‘𝐵)) = (#‘𝐵)
76	75	oveq2i 6560	. . . . . . . 8 ⊢ (((#‘𝑦) · (#‘𝐵)) + (1 · (#‘𝐵))) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵))
77	74, 76	syl6eq 2660	. . . . . . 7 ⊢ (𝑦 ∈ Fin → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
78	77	adantr 480	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((#‘𝑦) + 1) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
79	66, 78	eqtrd 2644	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
80	79	adantr 480	. . . 4 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)) = (((#‘𝑦) · (#‘𝐵)) + (#‘𝐵)))
81	33, 63, 80	3eqtr4d 2654	. . 3 ⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵))) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵)))
82	81	ex 449	. 2 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((#‘(𝑦 × 𝐵)) = ((#‘𝑦) · (#‘𝐵)) → (#‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((#‘(𝑦 ∪ {𝑧})) · (#‘𝐵))))
83	5, 10, 15, 20, 31, 82	findcard2s 8086	1 ⊢ (𝐴 ∈ Fin → (#‘(𝐴 × 𝐵)) = ((#‘𝐴) · (#‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 ∩ cin 3539 ∅c0 3874 {csn 4125 class class class wbr 4583 × cxp 5036 ‘cfv 5804 (class class class)co 6549 ≈ cen 7838 Fincfn 7841 ℂcc 9813 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 ℕ₀cn0 11169 #chash 12979

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-hash 12980

This theorem is referenced by: hashxp 13081

W3C validator