Theorem om1om1r

Description: Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of Schloeder p. 5. See om1 and om1r for individual statements. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	om1om1r	|- ( A e. On -> ( ( 1o .o A ) = ( A .o 1o ) /\ ( A .o 1o ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		om1r	|- ( A e. On -> ( 1o .o A ) = A )
2		om1	|- ( A e. On -> ( A .o 1o ) = A )
3	1 2	eqtr4d	|- ( A e. On -> ( 1o .o A ) = ( A .o 1o ) )
4	3 2	jca	|- ( A e. On -> ( ( 1o .o A ) = ( A .o 1o ) /\ ( A .o 1o ) = A ) )