Theorem hashnnm

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

	Ref	Expression
Assertion	hashnnm	|- ( ( A e. _om /\ B e. _om ) -> ( # ` ( A .o B ) ) = ( ( # ` A ) x. ( # ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		nnon	|- ( B e. _om -> B e. On )
3		omxpen	|- ( ( A e. On /\ B e. On ) -> ( A .o B ) ~~ ( A X. B ) )
4	1 2 3	syl2an	|- ( ( A e. _om /\ B e. _om ) -> ( A .o B ) ~~ ( A X. B ) )
5		hasheni	|- ( ( A .o B ) ~~ ( A X. B ) -> ( # ` ( A .o B ) ) = ( # ` ( A X. B ) ) )
6	4 5	syl	|- ( ( A e. _om /\ B e. _om ) -> ( # ` ( A .o B ) ) = ( # ` ( A X. B ) ) )
7		nnfi	|- ( A e. _om -> A e. Fin )
8		nnfi	|- ( B e. _om -> B e. Fin )
9		hashxp	|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
10	7 8 9	syl2an	|- ( ( A e. _om /\ B e. _om ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
11	6 10	eqtrd	|- ( ( A e. _om /\ B e. _om ) -> ( # ` ( A .o B ) ) = ( ( # ` A ) x. ( # ` B ) ) )