Theorem hash2iun1dif1

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

	Ref	Expression
Hypotheses	hash2iun1dif1.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	hash2iun1dif1.b	⊢ 𝐵 = ( 𝐴 ∖ { 𝑥 } )
	hash2iun1dif1.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Fin )
	hash2iun1dif1.da	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 )
	hash2iun1dif1.db	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Disj 𝑦 ∈ 𝐵 𝐶 )
	hash2iun1dif1.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ♯ ‘ 𝐶 ) = 1 )
Assertion	hash2iun1dif1	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ) = ( ( ♯ ‘ 𝐴 ) · ( ( ♯ ‘ 𝐴 ) − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hash2iun1dif1.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		hash2iun1dif1.b	⊢ 𝐵 = ( 𝐴 ∖ { 𝑥 } )
3		hash2iun1dif1.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Fin )
4		hash2iun1dif1.da	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 )
5		hash2iun1dif1.db	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Disj 𝑦 ∈ 𝐵 𝐶 )
6		hash2iun1dif1.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ♯ ‘ 𝐶 ) = 1 )
7		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
8	1 7	syl	⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ∈ Fin )
10	2 9	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
11	1 10 3 4 5	hash2iun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ) = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ( ♯ ‘ 𝐶 ) )
12	6	2sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ( ♯ ‘ 𝐶 ) = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 1 )
13		1cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 1 ∈ ℂ )
14		fsumconst	⊢ ( ( 𝐵 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑦 ∈ 𝐵 1 = ( ( ♯ ‘ 𝐵 ) · 1 ) )
15	10 13 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑦 ∈ 𝐵 1 = ( ( ♯ ‘ 𝐵 ) · 1 ) )
16	15	sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 1 = Σ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝐵 ) · 1 ) )
17	2	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( 𝐴 ∖ { 𝑥 } ) )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 𝐴 ∖ { 𝑥 } ) ) )
19		hashdifsn	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝑥 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
20	1 19	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ { 𝑥 } ) ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
21	18 20	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
22	21	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) · 1 ) = ( ( ( ♯ ‘ 𝐴 ) − 1 ) · 1 ) )
23	22	sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝐵 ) · 1 ) = Σ 𝑥 ∈ 𝐴 ( ( ( ♯ ‘ 𝐴 ) − 1 ) · 1 ) )
24		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
25	1 24	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
26	25	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
27		peano2cnm	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℂ → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℂ )
28	26 27	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℂ )
29	28	mulid1d	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) · 1 ) = ( ( ♯ ‘ 𝐴 ) − 1 ) )
30	29	sumeq2sdv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ( ♯ ‘ 𝐴 ) − 1 ) · 1 ) = Σ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝐴 ) − 1 ) )
31		fsumconst	⊢ ( ( 𝐴 ∈ Fin ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℂ ) → Σ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝐴 ) − 1 ) = ( ( ♯ ‘ 𝐴 ) · ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
32	1 28 31	syl2anc	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ♯ ‘ 𝐴 ) − 1 ) = ( ( ♯ ‘ 𝐴 ) · ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
33	30 32	eqtrd	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ( ♯ ‘ 𝐴 ) − 1 ) · 1 ) = ( ( ♯ ‘ 𝐴 ) · ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
34	16 23 33	3eqtrd	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 1 = ( ( ♯ ‘ 𝐴 ) · ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
35	11 12 34	3eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ) = ( ( ♯ ‘ 𝐴 ) · ( ( ♯ ‘ 𝐴 ) − 1 ) ) )