Theorem om0suclim

Description: Closed form expression of the value of ordinal multiplication for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.5 of Schloeder p. 4. See om0 , omsuc , and omlim . (Contributed by RP, 18-Jan-2025)

	Ref	Expression
Assertion	om0suclim	|- ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A .o B ) = (/) ) /\ ( ( B = suc C /\ C e. On ) -> ( A .o B ) = ( ( A .o C ) +o A ) ) /\ ( Lim B -> ( A .o B ) = U_ c e. B ( A .o c ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		om0	|- ( A e. On -> ( A .o (/) ) = (/) )
2		omsuc	|- ( ( A e. On /\ C e. On ) -> ( A .o suc C ) = ( ( A .o C ) +o A ) )
3		omlim	|- ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( A .o B ) = U_ c e. B ( A .o c ) )
4	3	anassrs	|- ( ( ( A e. On /\ B e. On ) /\ Lim B ) -> ( A .o B ) = U_ c e. B ( A .o c ) )
5	1 2 4	onov0suclim	|- ( ( A e. On /\ B e. On ) -> ( ( B = (/) -> ( A .o B ) = (/) ) /\ ( ( B = suc C /\ C e. On ) -> ( A .o B ) = ( ( A .o C ) +o A ) ) /\ ( Lim B -> ( A .o B ) = U_ c e. B ( A .o c ) ) ) )