Metamath Proof Explorer

Theorem hashxpe

Description: The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023)

Ref Expression
Assertion hashxpe 
|- ( ( A e. V /\ B e. W ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A e. Fin /\ B e. Fin ) ) -> ( A e. Fin /\ B e. Fin ) )
2 hashxp 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
3 1 2 syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A e. Fin /\ B e. Fin ) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
4 nn0ssre 
 |-  NN0 C_ RR
5 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
6 4 5 sselid 
 |-  ( A e. Fin -> ( # ` A ) e. RR )
7 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
8 4 7 sselid 
 |-  ( B e. Fin -> ( # ` B ) e. RR )
9 6 8 anim12i 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) )
10 1 9 syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A e. Fin /\ B e. Fin ) ) -> ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) )
11 rexmul 
 |-  ( ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) -> ( ( # ` A ) *e ( # ` B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
12 10 11 syl 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A e. Fin /\ B e. Fin ) ) -> ( ( # ` A ) *e ( # ` B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
13 3 12 eqtr4d 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( A e. Fin /\ B e. Fin ) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
14 simpr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> B = (/) )
15 14 xpeq2d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( A X. B ) = ( A X. (/) ) )
16 xp0 
 |-  ( A X. (/) ) = (/)
17 15 16 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( A X. B ) = (/) )
18 17 fveq2d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( # ` ( A X. B ) ) = ( # ` (/) ) )
19 hash0 
 |-  ( # ` (/) ) = 0
20 18 19 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( # ` ( A X. B ) ) = 0 )
21 simpl 
 |-  ( ( A e. V /\ B e. W ) -> A e. V )
22 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
23 21 22 sylan 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) -> ( # ` A ) = +oo )
24 23 adantr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( # ` A ) = +oo )
25 14 fveq2d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( # ` B ) = ( # ` (/) ) )
26 25 19 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( # ` B ) = 0 )
27 24 26 oveq12d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( ( # ` A ) *e ( # ` B ) ) = ( +oo *e 0 ) )
28 pnfxr 
 |-  +oo e. RR*
29 xmul01 
 |-  ( +oo e. RR* -> ( +oo *e 0 ) = 0 )
30 28 29 ax-mp 
 |-  ( +oo *e 0 ) = 0
31 27 30 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( ( # ` A ) *e ( # ` B ) ) = 0 )
32 20 31 eqtr4d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B = (/) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
33 simpr 
 |-  ( ( A e. V /\ B e. W ) -> B e. W )
34 33 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> B e. W )
35 hashxrcl 
 |-  ( B e. W -> ( # ` B ) e. RR* )
36 34 35 syl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( # ` B ) e. RR* )
37 hashgt0 
 |-  ( ( B e. W /\ B =/= (/) ) -> 0 < ( # ` B ) )
38 34 37 sylancom 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> 0 < ( # ` B ) )
39 xmulpnf2 
 |-  ( ( ( # ` B ) e. RR* /\ 0 < ( # ` B ) ) -> ( +oo *e ( # ` B ) ) = +oo )
40 36 38 39 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( +oo *e ( # ` B ) ) = +oo )
41 23 adantr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( # ` A ) = +oo )
42 41 oveq1d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( ( # ` A ) *e ( # ` B ) ) = ( +oo *e ( # ` B ) ) )
43 21 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> A e. V )
44 43 34 xpexd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( A X. B ) e. _V )
45 simplr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> -. A e. Fin )
46 0fi 
 |-  (/) e. Fin
47 eleq1 
 |-  ( A = (/) -> ( A e. Fin <-> (/) e. Fin ) )
48 46 47 mpbiri 
 |-  ( A = (/) -> A e. Fin )
49 48 necon3bi 
 |-  ( -. A e. Fin -> A =/= (/) )
50 45 49 syl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> A =/= (/) )
51 simpr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> B =/= (/) )
52 ioran 
 |-  ( -. ( A = (/) \/ B = (/) ) <-> ( -. A = (/) /\ -. B = (/) ) )
53 xpeq0 
 |-  ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
54 53 necon3abii 
 |-  ( ( A X. B ) =/= (/) <-> -. ( A = (/) \/ B = (/) ) )
55 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
56 df-ne 
 |-  ( B =/= (/) <-> -. B = (/) )
57 55 56 anbi12i 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( -. A = (/) /\ -. B = (/) ) )
58 52 54 57 3bitr4i 
 |-  ( ( A X. B ) =/= (/) <-> ( A =/= (/) /\ B =/= (/) ) )
59 58 biimpri 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( A X. B ) =/= (/) )
60 50 51 59 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( A X. B ) =/= (/) )
61 45 intnanrd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> -. ( A e. Fin /\ B e. Fin ) )
62 pm4.61 
 |-  ( -. ( ( A X. B ) =/= (/) -> ( A e. Fin /\ B e. Fin ) ) <-> ( ( A X. B ) =/= (/) /\ -. ( A e. Fin /\ B e. Fin ) ) )
63 xpfir 
 |-  ( ( ( A X. B ) e. Fin /\ ( A X. B ) =/= (/) ) -> ( A e. Fin /\ B e. Fin ) )
64 63 ex 
 |-  ( ( A X. B ) e. Fin -> ( ( A X. B ) =/= (/) -> ( A e. Fin /\ B e. Fin ) ) )
65 64 con3i 
 |-  ( -. ( ( A X. B ) =/= (/) -> ( A e. Fin /\ B e. Fin ) ) -> -. ( A X. B ) e. Fin )
66 62 65 sylbir 
 |-  ( ( ( A X. B ) =/= (/) /\ -. ( A e. Fin /\ B e. Fin ) ) -> -. ( A X. B ) e. Fin )
67 60 61 66 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> -. ( A X. B ) e. Fin )
68 hashinf 
 |-  ( ( ( A X. B ) e. _V /\ -. ( A X. B ) e. Fin ) -> ( # ` ( A X. B ) ) = +oo )
69 44 67 68 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( # ` ( A X. B ) ) = +oo )
70 40 42 69 3eqtr4rd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) /\ B =/= (/) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
71 exmidne 
 |-  ( B = (/) \/ B =/= (/) )
72 71 a1i 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) -> ( B = (/) \/ B =/= (/) ) )
73 32 70 72 mpjaodan 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. A e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
74 73 adantlr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. ( A e. Fin /\ B e. Fin ) ) /\ -. A e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
75 simpr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> A = (/) )
76 75 xpeq1d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( A X. B ) = ( (/) X. B ) )
77 0xp 
 |-  ( (/) X. B ) = (/)
78 76 77 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( A X. B ) = (/) )
79 78 fveq2d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( # ` ( A X. B ) ) = ( # ` (/) ) )
80 79 19 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( # ` ( A X. B ) ) = 0 )
81 75 fveq2d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( # ` A ) = ( # ` (/) ) )
82 81 19 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( # ` A ) = 0 )
83 hashinf 
 |-  ( ( B e. W /\ -. B e. Fin ) -> ( # ` B ) = +oo )
84 33 83 sylan 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) -> ( # ` B ) = +oo )
85 84 adantr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( # ` B ) = +oo )
86 82 85 oveq12d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( ( # ` A ) *e ( # ` B ) ) = ( 0 *e +oo ) )
87 xmul02 
 |-  ( +oo e. RR* -> ( 0 *e +oo ) = 0 )
88 28 87 ax-mp 
 |-  ( 0 *e +oo ) = 0
89 86 88 eqtrdi 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( ( # ` A ) *e ( # ` B ) ) = 0 )
90 80 89 eqtr4d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A = (/) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
91 hashxrcl 
 |-  ( A e. V -> ( # ` A ) e. RR* )
92 91 ad3antrrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( # ` A ) e. RR* )
93 hashgt0 
 |-  ( ( A e. V /\ A =/= (/) ) -> 0 < ( # ` A ) )
94 93 ad4ant14 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> 0 < ( # ` A ) )
95 xmulpnf1 
 |-  ( ( ( # ` A ) e. RR* /\ 0 < ( # ` A ) ) -> ( ( # ` A ) *e +oo ) = +oo )
96 92 94 95 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( ( # ` A ) *e +oo ) = +oo )
97 84 adantr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( # ` B ) = +oo )
98 97 oveq2d 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( ( # ` A ) *e ( # ` B ) ) = ( ( # ` A ) *e +oo ) )
99 21 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> A e. V )
100 33 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> B e. W )
101 99 100 xpexd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( A X. B ) e. _V )
102 simpr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> A =/= (/) )
103 simplr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> -. B e. Fin )
104 eleq1 
 |-  ( B = (/) -> ( B e. Fin <-> (/) e. Fin ) )
105 46 104 mpbiri 
 |-  ( B = (/) -> B e. Fin )
106 105 necon3bi 
 |-  ( -. B e. Fin -> B =/= (/) )
107 103 106 syl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> B =/= (/) )
108 102 107 59 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( A X. B ) =/= (/) )
109 103 intnand 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> -. ( A e. Fin /\ B e. Fin ) )
110 108 109 66 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> -. ( A X. B ) e. Fin )
111 101 110 68 syl2anc 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( # ` ( A X. B ) ) = +oo )
112 96 98 111 3eqtr4rd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) /\ A =/= (/) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
113 exmidne 
 |-  ( A = (/) \/ A =/= (/) )
114 113 a1i 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) -> ( A = (/) \/ A =/= (/) ) )
115 90 112 114 mpjaodan 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. B e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
116 115 adantlr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ -. ( A e. Fin /\ B e. Fin ) ) /\ -. B e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
117 simpr 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. ( A e. Fin /\ B e. Fin ) ) -> -. ( A e. Fin /\ B e. Fin ) )
118 ianor 
 |-  ( -. ( A e. Fin /\ B e. Fin ) <-> ( -. A e. Fin \/ -. B e. Fin ) )
119 117 118 sylib 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. ( A e. Fin /\ B e. Fin ) ) -> ( -. A e. Fin \/ -. B e. Fin ) )
120 74 116 119 mpjaodan 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. ( A e. Fin /\ B e. Fin ) ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )
121 exmidd 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A e. Fin /\ B e. Fin ) \/ -. ( A e. Fin /\ B e. Fin ) ) )
122 13 120 121 mpjaodan 
 |-  ( ( A e. V /\ B e. W ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) *e ( # ` B ) ) )