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	⊢ ( 𝐴 ∈ On → ( ( 1o ·o 𝐴 ) = ( 𝐴 ·o 1o ) ∧ ( 𝐴 ·o 1o ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		om1r	⊢ ( 𝐴 ∈ On → ( 1o ·o 𝐴 ) = 𝐴 )
2		om1	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o 1o ) = 𝐴 )
3	1 2	eqtr4d	⊢ ( 𝐴 ∈ On → ( 1o ·o 𝐴 ) = ( 𝐴 ·o 1o ) )
4	3 2	jca	⊢ ( 𝐴 ∈ On → ( ( 1o ·o 𝐴 ) = ( 𝐴 ·o 1o ) ∧ ( 𝐴 ·o 1o ) = 𝐴 ) )