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 \in V \land B \in W) \to \|A \times B\| = \|A\| \cdot_{𝑒} \|B\|$

Proof

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

Metamath Proof Explorer

Theorem hashxpe

Proof