Theorem hashxp

Description: The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012)

	Ref	Expression
Assertion	hashxp	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq2	⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( 𝐴 × 𝐵 ) = ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) )
2	1	fveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) )
3		fveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) )
4	3	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) )
5	2 4	eqeq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) ) )
6	5	imbi2d	⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) ) ) )
7		0fin	⊢ ∅ ∈ Fin
8	7	elimel	⊢ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ∈ Fin
9	8	hashxplem	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) )
10	6 9	dedth	⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ) )
11	10	impcom	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )