Metamath Proof Explorer

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 \in On \to (1_{𝑜} \cdot_{𝑜} A = A \cdot_{𝑜} 1_{𝑜} \land A \cdot_{𝑜} 1_{𝑜} = A)$

Proof

Step	Hyp	Ref	Expression
1		om1r	$⊢ A \in On \to 1_{𝑜} \cdot_{𝑜} A = A$
2		om1	$⊢ A \in On \to A \cdot_{𝑜} 1_{𝑜} = A$
3	1 2	eqtr4d	$⊢ A \in On \to 1_{𝑜} \cdot_{𝑜} A = A \cdot_{𝑜} 1_{𝑜}$
4	3 2	jca	$⊢ A \in On \to (1_{𝑜} \cdot_{𝑜} A = A \cdot_{𝑜} 1_{𝑜} \land A \cdot_{𝑜} 1_{𝑜} = A)$