Theorem hash2iun1dif1

Description: The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	hash2iun1dif1.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	hash2iun1dif1.b	$$⊢B=A\setminus \left\{x\right\}$$
	hash2iun1dif1.c	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to C\in \mathrm{Fin}$$
	hash2iun1dif1.da	$$⊢\phi \to \underset{x\in A}{Disj}\bigcup _{y\in B}C$$
	hash2iun1dif1.db	$$⊢\left(\phi \wedge x\in A\right)\to \underset{y\in B}{Disj}C$$
	hash2iun1dif1.1	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to \left|C\right|=1$$
Assertion	hash2iun1dif1	$$⊢\phi \to \left|\bigcup _{x\in A}\bigcup _{y\in B}C\right|=\left|A\right|\left(\left|A\right|-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		hash2iun1dif1.a	$$⊢\phi \to A\in \mathrm{Fin}$$
2		hash2iun1dif1.b	$$⊢B=A\setminus \left\{x\right\}$$
3		hash2iun1dif1.c	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to C\in \mathrm{Fin}$$
4		hash2iun1dif1.da	$$⊢\phi \to \underset{x\in A}{Disj}\bigcup _{y\in B}C$$
5		hash2iun1dif1.db	$$⊢\left(\phi \wedge x\in A\right)\to \underset{y\in B}{Disj}C$$
6		hash2iun1dif1.1	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to \left|C\right|=1$$
7		diffi	$$⊢A\in \mathrm{Fin}\to A\setminus \left\{x\right\}\in \mathrm{Fin}$$
8	1 7	syl	$$⊢\phi \to A\setminus \left\{x\right\}\in \mathrm{Fin}$$
9	8	adantr	$$⊢\left(\phi \wedge x\in A\right)\to A\setminus \left\{x\right\}\in \mathrm{Fin}$$
10	2 9	eqeltrid	$$⊢\left(\phi \wedge x\in A\right)\to B\in \mathrm{Fin}$$
11	1 10 3 4 5	hash2iun	$$⊢\phi \to \left|\bigcup _{x\in A}\bigcup _{y\in B}C\right|=\sum _{x\in A}\sum _{y\in B}\left|C\right|$$
12	6	2sumeq2dv	$$⊢\phi \to \sum _{x\in A}\sum _{y\in B}\left|C\right|=\sum _{x\in A}\sum _{y\in B}1$$
13		1cnd	$$⊢\left(\phi \wedge x\in A\right)\to 1\in ℂ$$
14		fsumconst	$$⊢\left(B\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{y\in B}1=\left|B\right|\cdot 1$$
15	10 13 14	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to \sum _{y\in B}1=\left|B\right|\cdot 1$$
16	15	sumeq2dv	$$⊢\phi \to \sum _{x\in A}\sum _{y\in B}1=\sum _{x\in A}\left|B\right|\cdot 1$$
17	2	a1i	$$⊢\left(\phi \wedge x\in A\right)\to B=A\setminus \left\{x\right\}$$
18	17	fveq2d	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|=\left|A\setminus \left\{x\right\}\right|$$
19		hashdifsn	$$⊢\left(A\in \mathrm{Fin}\wedge x\in A\right)\to \left|A\setminus \left\{x\right\}\right|=\left|A\right|-1$$
20	1 19	sylan	$$⊢\left(\phi \wedge x\in A\right)\to \left|A\setminus \left\{x\right\}\right|=\left|A\right|-1$$
21	18 20	eqtrd	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|=\left|A\right|-1$$
22	21	oveq1d	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\cdot 1=\left(\left|A\right|-1\right)\cdot 1$$
23	22	sumeq2dv	$$⊢\phi \to \sum _{x\in A}\left|B\right|\cdot 1=\sum _{x\in A}\left(\left|A\right|-1\right)\cdot 1$$
24		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
25	1 24	syl	$$⊢\phi \to \left|A\right|\in {\mathbb{N}}_0$$
26	25	nn0cnd	$$⊢\phi \to \left|A\right|\in ℂ$$
27		peano2cnm	$$⊢\left|A\right|\in ℂ\to \left|A\right|-1\in ℂ$$
28	26 27	syl	$$⊢\phi \to \left|A\right|-1\in ℂ$$
29	28	mulridd	$$⊢\phi \to \left(\left|A\right|-1\right)\cdot 1=\left|A\right|-1$$
30	29	sumeq2sdv	$$⊢\phi \to \sum _{x\in A}\left(\left|A\right|-1\right)\cdot 1=\sum _{x\in A}\left(\left|A\right|-1\right)$$
31		fsumconst	$$⊢\left(A\in \mathrm{Fin}\wedge \left|A\right|-1\in ℂ\right)\to \sum _{x\in A}\left(\left|A\right|-1\right)=\left|A\right|\left(\left|A\right|-1\right)$$
32	1 28 31	syl2anc	$$⊢\phi \to \sum _{x\in A}\left(\left|A\right|-1\right)=\left|A\right|\left(\left|A\right|-1\right)$$
33	30 32	eqtrd	$$⊢\phi \to \sum _{x\in A}\left(\left|A\right|-1\right)\cdot 1=\left|A\right|\left(\left|A\right|-1\right)$$
34	16 23 33	3eqtrd	$$⊢\phi \to \sum _{x\in A}\sum _{y\in B}1=\left|A\right|\left(\left|A\right|-1\right)$$
35	11 12 34	3eqtrd	$$⊢\phi \to \left|\bigcup _{x\in A}\bigcup _{y\in B}C\right|=\left|A\right|\left(\left|A\right|-1\right)$$