Metamath Proof Explorer

Theorem nmulval

Description: Show the value of natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026)

		Ref	Expression
	Assertion	nmulval	\|- ( ( A e. On /\ B e. On ) -> ( A .no B ) = \|^\| { x e. On \| A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )

Proof

Step	Hyp	Ref	Expression
1		nmulprop	\|- ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = \|^\| { x e. On \| A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )
2	1	simprd	\|- ( ( A e. On /\ B e. On ) -> ( A .no B ) = \|^\| { x e. On \| A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )

Step

Hyp

Ref

Expression

nmulprop

 |-  ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) )

simprd

 |-  ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } )