Theorem hashnna

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

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

Proof

Step	Hyp	Ref	Expression
1		hashgval2	|- ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2	1	hashgadd	|- ( ( A e. _om /\ B e. _om ) -> ( ( # |` _om ) ` ( A +o B ) ) = ( ( ( # |` _om ) ` A ) + ( ( # |` _om ) ` B ) ) )
3		nnacl	|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
4	3	fvresd	|- ( ( A e. _om /\ B e. _om ) -> ( ( # |` _om ) ` ( A +o B ) ) = ( # ` ( A +o B ) ) )
5		fvres	|- ( A e. _om -> ( ( # |` _om ) ` A ) = ( # ` A ) )
6		fvres	|- ( B e. _om -> ( ( # |` _om ) ` B ) = ( # ` B ) )
7	5 6	oveqan12d	|- ( ( A e. _om /\ B e. _om ) -> ( ( ( # |` _om ) ` A ) + ( ( # |` _om ) ` B ) ) = ( ( # ` A ) + ( # ` B ) ) )
8	2 4 7	3eqtr3d	|- ( ( A e. _om /\ B e. _om ) -> ( # ` ( A +o B ) ) = ( ( # ` A ) + ( # ` B ) ) )