hashnnm

Description: The # function on _om preserves multiplication. (Contributed by Eric Schmidt, 7-Jul-2026)

		Ref	Expression
	Assertion	hashnnm	$⊢ (A \in ω \land B \in ω) \to \|A \cdot_{𝑜} B\| = \|A\| \|B\|$

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		nnon	$⊢ B \in ω \to B \in On$
3		omxpen	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B) \approx (A \times B)$
4	1 2 3	syl2an	$⊢ (A \in ω \land B \in ω) \to (A \cdot_{𝑜} B) \approx (A \times B)$
5		hasheni	$⊢ (A \cdot_{𝑜} B) \approx (A \times B) \to \|A \cdot_{𝑜} B\| = \|A \times B\|$
6	4 5	syl	$⊢ (A \in ω \land B \in ω) \to \|A \cdot_{𝑜} B\| = \|A \times B\|$
7		nnfi	$⊢ A \in ω \to A \in Fin$
8		nnfi	$⊢ B \in ω \to B \in Fin$
9		hashxp	$⊢ (A \in Fin \land B \in Fin) \to \|A \times B\| = \|A\| \|B\|$
10	7 8 9	syl2an	$⊢ (A \in ω \land B \in ω) \to \|A \times B\| = \|A\| \|B\|$
11	6 10	eqtrd	$⊢ (A \in ω \land B \in ω) \to \|A \cdot_{𝑜} B\| = \|A\| \|B\|$

Metamath Proof Explorer