Metamath Proof Explorer

Theorem hash2iun1dif1

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

Ref Expression
Hypotheses hash2iun1dif1.a 
|- ( ph -> A e. Fin )
hash2iun1dif1.b 
|- B = ( A \ { x } )
hash2iun1dif1.c 
|- ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )
hash2iun1dif1.da 
|- ( ph -> Disj_ x e. A U_ y e. B C )
hash2iun1dif1.db 
|- ( ( ph /\ x e. A ) -> Disj_ y e. B C )
hash2iun1dif1.1 
|- ( ( ph /\ x e. A /\ y e. B ) -> ( # ` C ) = 1 )
Assertion hash2iun1dif1 
|- ( ph -> ( # ` U_ x e. A U_ y e. B C ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 hash2iun1dif1.a 
 |-  ( ph -> A e. Fin )
2 hash2iun1dif1.b 
 |-  B = ( A \ { x } )
3 hash2iun1dif1.c 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )
4 hash2iun1dif1.da 
 |-  ( ph -> Disj_ x e. A U_ y e. B C )
5 hash2iun1dif1.db 
 |-  ( ( ph /\ x e. A ) -> Disj_ y e. B C )
6 hash2iun1dif1.1 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> ( # ` C ) = 1 )
7 diffi 
 |-  ( A e. Fin -> ( A \ { x } ) e. Fin )
8 1 7 syl 
 |-  ( ph -> ( A \ { x } ) e. Fin )
9 8 adantr 
 |-  ( ( ph /\ x e. A ) -> ( A \ { x } ) e. Fin )
10 2 9 eqeltrid 
 |-  ( ( ph /\ x e. A ) -> B e. Fin )
11 1 10 3 4 5 hash2iun 
 |-  ( ph -> ( # ` U_ x e. A U_ y e. B C ) = sum_ x e. A sum_ y e. B ( # ` C ) )
12 6 2sumeq2dv 
 |-  ( ph -> sum_ x e. A sum_ y e. B ( # ` C ) = sum_ x e. A sum_ y e. B 1 )
13 1cnd 
 |-  ( ( ph /\ x e. A ) -> 1 e. CC )
14 fsumconst 
 |-  ( ( B e. Fin /\ 1 e. CC ) -> sum_ y e. B 1 = ( ( # ` B ) x. 1 ) )
15 10 13 14 syl2anc 
 |-  ( ( ph /\ x e. A ) -> sum_ y e. B 1 = ( ( # ` B ) x. 1 ) )
16 15 sumeq2dv 
 |-  ( ph -> sum_ x e. A sum_ y e. B 1 = sum_ x e. A ( ( # ` B ) x. 1 ) )
17 2 a1i 
 |-  ( ( ph /\ x e. A ) -> B = ( A \ { x } ) )
18 17 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( # ` B ) = ( # ` ( A \ { x } ) ) )
19 hashdifsn 
 |-  ( ( A e. Fin /\ x e. A ) -> ( # ` ( A \ { x } ) ) = ( ( # ` A ) - 1 ) )
20 1 19 sylan 
 |-  ( ( ph /\ x e. A ) -> ( # ` ( A \ { x } ) ) = ( ( # ` A ) - 1 ) )
21 18 20 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( # ` B ) = ( ( # ` A ) - 1 ) )
22 21 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( # ` B ) x. 1 ) = ( ( ( # ` A ) - 1 ) x. 1 ) )
23 22 sumeq2dv 
 |-  ( ph -> sum_ x e. A ( ( # ` B ) x. 1 ) = sum_ x e. A ( ( ( # ` A ) - 1 ) x. 1 ) )
24 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
25 1 24 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
26 25 nn0cnd 
 |-  ( ph -> ( # ` A ) e. CC )
27 peano2cnm 
 |-  ( ( # ` A ) e. CC -> ( ( # ` A ) - 1 ) e. CC )
28 26 27 syl 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. CC )
29 28 mulridd 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) x. 1 ) = ( ( # ` A ) - 1 ) )
30 29 sumeq2sdv 
 |-  ( ph -> sum_ x e. A ( ( ( # ` A ) - 1 ) x. 1 ) = sum_ x e. A ( ( # ` A ) - 1 ) )
31 fsumconst 
 |-  ( ( A e. Fin /\ ( ( # ` A ) - 1 ) e. CC ) -> sum_ x e. A ( ( # ` A ) - 1 ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )
32 1 28 31 syl2anc 
 |-  ( ph -> sum_ x e. A ( ( # ` A ) - 1 ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )
33 30 32 eqtrd 
 |-  ( ph -> sum_ x e. A ( ( ( # ` A ) - 1 ) x. 1 ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )
34 16 23 33 3eqtrd 
 |-  ( ph -> sum_ x e. A sum_ y e. B 1 = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )
35 11 12 34 3eqtrd 
 |-  ( ph -> ( # ` U_ x e. A U_ y e. B C ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )