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 
|- ( ph -> A e. Fin )
fsumiun.2 
|- ( ( ph /\ x e. A ) -> B e. Fin )
fsumiun.3 
|- ( ph -> Disj_ x e. A B )
Assertion hashiun 
|- ( ph -> ( # ` U_ x e. A B ) = sum_ x e. A ( # ` B ) )

Proof

Step Hyp Ref Expression
1 fsumiun.1 
 |-  ( ph -> A e. Fin )
2 fsumiun.2 
 |-  ( ( ph /\ x e. A ) -> B e. Fin )
3 fsumiun.3 
 |-  ( ph -> Disj_ x e. A B )
4 1cnd 
 |-  ( ( ph /\ ( x e. A /\ k e. B ) ) -> 1 e. CC )
5 1 2 3 4 fsumiun 
 |-  ( ph -> sum_ k e. U_ x e. A B 1 = sum_ x e. A sum_ k e. B 1 )
6 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. Fin )
7 iunfi 
 |-  ( ( A e. Fin /\ A. x e. A B e. Fin ) -> U_ x e. A B e. Fin )
8 1 6 7 syl2anc 
 |-  ( ph -> U_ x e. A B e. Fin )
9 ax-1cn 
 |-  1 e. CC
10 fsumconst 
 |-  ( ( U_ x e. A B e. Fin /\ 1 e. CC ) -> sum_ k e. U_ x e. A B 1 = ( ( # ` U_ x e. A B ) x. 1 ) )
11 8 9 10 sylancl 
 |-  ( ph -> sum_ k e. U_ x e. A B 1 = ( ( # ` U_ x e. A B ) x. 1 ) )
12 hashcl 
 |-  ( U_ x e. A B e. Fin -> ( # ` U_ x e. A B ) e. NN0 )
13 nn0cn 
 |-  ( ( # ` U_ x e. A B ) e. NN0 -> ( # ` U_ x e. A B ) e. CC )
14 mulid1 
 |-  ( ( # ` U_ x e. A B ) e. CC -> ( ( # ` U_ x e. A B ) x. 1 ) = ( # ` U_ x e. A B ) )
15 8 12 13 14 4syl 
 |-  ( ph -> ( ( # ` U_ x e. A B ) x. 1 ) = ( # ` U_ x e. A B ) )
16 11 15 eqtrd 
 |-  ( ph -> sum_ k e. U_ x e. A B 1 = ( # ` U_ x e. A B ) )
17 fsumconst 
 |-  ( ( B e. Fin /\ 1 e. CC ) -> sum_ k e. B 1 = ( ( # ` B ) x. 1 ) )
18 2 9 17 sylancl 
 |-  ( ( ph /\ x e. A ) -> sum_ k e. B 1 = ( ( # ` B ) x. 1 ) )
19 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
20 nn0cn 
 |-  ( ( # ` B ) e. NN0 -> ( # ` B ) e. CC )
21 mulid1 
 |-  ( ( # ` B ) e. CC -> ( ( # ` B ) x. 1 ) = ( # ` B ) )
22 2 19 20 21 4syl 
 |-  ( ( ph /\ x e. A ) -> ( ( # ` B ) x. 1 ) = ( # ` B ) )
23 18 22 eqtrd 
 |-  ( ( ph /\ x e. A ) -> sum_ k e. B 1 = ( # ` B ) )
24 23 sumeq2dv 
 |-  ( ph -> sum_ x e. A sum_ k e. B 1 = sum_ x e. A ( # ` B ) )
25 5 16 24 3eqtr3d 
 |-  ( ph -> ( # ` U_ x e. A B ) = sum_ x e. A ( # ` B ) )