This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulrid ⊢ ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ ℂ → ( ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) · 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 mulrid ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℂ → ( ( ♯ ‘ 𝐵 ) · 1 ) = ( ♯ ‘ 𝐵 ) )
22 2 19 20 21 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) · 1 ) = ( ♯ ‘ 𝐵 ) )
23 18 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝐵 1 = ( ♯ ‘ 𝐵 ) )
24 23 sumeq2dv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 1 = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝐵 ) )
25 5 16 24 3eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝐵 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝐵 ) )