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	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumiun.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
	fsumiun.3	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
Assertion	hashiun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fsumiun.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fsumiun.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
3		fsumiun.3	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
4		1cnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 1 ∈ ℂ )
5	1 2 3 4	fsumiun	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 1 = Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 1 )
6	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
7		iunfi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
8	1 6 7	syl2anc	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
9		ax-1cn	⊢ 1 ∈ ℂ
10		fsumconst	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 1 = ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) · 1 ) )
11	8 9 10	sylancl	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 1 = ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) · 1 ) )
12		hashcl	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ ℕ0 )
13		nn0cn	⊢ ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ ℕ0 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ ℂ )
14		mulid1	⊢ ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ ℂ → ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) · 1 ) = ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
15	8 12 13 14	4syl	⊢ ( 𝜑 → ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) · 1 ) = ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
16	11 15	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 1 = ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
17		fsumconst	⊢ ( ( 𝐵 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ 𝐵 1 = ( ( ♯ ‘ 𝐵 ) · 1 ) )
18	2 9 17	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 1 = ( ( ♯ ‘ 𝐵 ) · 1 ) )
19		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
20		nn0cn	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
21		mulid1	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℂ → ( ( ♯ ‘ 𝐵 ) · 1 ) = ( ♯ ‘ 𝐵 ) )
22	2 19 20 21	4syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) · 1 ) = ( ♯ ‘ 𝐵 ) )
23	18 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 1 = ( ♯ ‘ 𝐵 ) )
24	23	sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 1 = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝐵 ) )
25	5 16 24	3eqtr3d	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝐵 ) )