Theorem hashiun

Description: The cardinality of a disjoint indexed union. (Contributed by Mario Carneiro, 24-Jan-2015) (Revised by Mario Carneiro, 10-Dec-2016)

	Ref	Expression
Hypotheses	fsumiun.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumiun.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{Fin}$$
	fsumiun.3	$$⊢\phi \to \underset{x\in A}{Disj}B$$
Assertion	hashiun	$$⊢\phi \to \left|\bigcup _{x\in A}B\right|=\sum _{x\in A}\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		fsumiun.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumiun.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{Fin}$$
3		fsumiun.3	$$⊢\phi \to \underset{x\in A}{Disj}B$$
4		1cnd	$$⊢\left(\phi \wedge \left(x\in A\wedge k\in B\right)\right)\to 1\in ℂ$$
5	1 2 3 4	fsumiun	$$⊢\phi \to \sum _{k\in \bigcup _{x\in A}B}1=\sum _{x\in A}\sum _{k\in B}1$$
6	2	ralrimiva	$$⊢\phi \to \forall x\in AB\in \mathrm{Fin}$$
7		iunfi	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in AB\in \mathrm{Fin}\right)\to \bigcup _{x\in A}B\in \mathrm{Fin}$$
8	1 6 7	syl2anc	$$⊢\phi \to \bigcup _{x\in A}B\in \mathrm{Fin}$$
9		ax-1cn	$$⊢1\in ℂ$$
10		fsumconst	$$⊢\left(\bigcup _{x\in A}B\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{k\in \bigcup _{x\in A}B}1=\left|\bigcup _{x\in A}B\right|\cdot 1$$
11	8 9 10	sylancl	$$⊢\phi \to \sum _{k\in \bigcup _{x\in A}B}1=\left|\bigcup _{x\in A}B\right|\cdot 1$$
12		hashcl	$$⊢\bigcup _{x\in A}B\in \mathrm{Fin}\to \left|\bigcup _{x\in A}B\right|\in {\mathbb{N}}_0$$
13		nn0cn	$$⊢\left|\bigcup _{x\in A}B\right|\in {\mathbb{N}}_0\to \left|\bigcup _{x\in A}B\right|\in ℂ$$
14		mulrid	$$⊢\left|\bigcup _{x\in A}B\right|\in ℂ\to \left|\bigcup _{x\in A}B\right|\cdot 1=\left|\bigcup _{x\in A}B\right|$$
15	8 12 13 14	4syl	$$⊢\phi \to \left|\bigcup _{x\in A}B\right|\cdot 1=\left|\bigcup _{x\in A}B\right|$$
16	11 15	eqtrd	$$⊢\phi \to \sum _{k\in \bigcup _{x\in A}B}1=\left|\bigcup _{x\in A}B\right|$$
17		fsumconst	$$⊢\left(B\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{k\in B}1=\left|B\right|\cdot 1$$
18	2 9 17	sylancl	$$⊢\left(\phi \wedge x\in A\right)\to \sum _{k\in B}1=\left|B\right|\cdot 1$$
19		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
20		nn0cn	$$⊢\left|B\right|\in {\mathbb{N}}_0\to \left|B\right|\in ℂ$$
21		mulrid	$$⊢\left|B\right|\in ℂ\to \left|B\right|\cdot 1=\left|B\right|$$
22	2 19 20 21	4syl	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\cdot 1=\left|B\right|$$
23	18 22	eqtrd	$$⊢\left(\phi \wedge x\in A\right)\to \sum _{k\in B}1=\left|B\right|$$
24	23	sumeq2dv	$$⊢\phi \to \sum _{x\in A}\sum _{k\in B}1=\sum _{x\in A}\left|B\right|$$
25	5 16 24	3eqtr3d	$$⊢\phi \to \left|\bigcup _{x\in A}B\right|=\sum _{x\in A}\left|B\right|$$