Metamath Proof Explorer

Theorem om1

Description: Ordinal multiplication with 1. Proposition 8.18(2) of TakeutiZaring p. 63. Lemma 2.15 of Schloeder p. 5. (Contributed by NM, 29-Oct-1995)

		Ref	Expression
	Assertion	om1	$⊢ A \in On \to A \cdot_{𝑜} 1_{𝑜} = A$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
2	1	oveq2i	$⊢ A \cdot_{𝑜} 1_{𝑜} = A \cdot_{𝑜} suc \emptyset$
3		peano1	$⊢ \emptyset \in ω$
4		onmsuc	$⊢ (A \in On \land \emptyset \in ω) \to A \cdot_{𝑜} suc \emptyset = (A \cdot_{𝑜} \emptyset) +_{𝑜} A$
5	3 4	mpan2	$⊢ A \in On \to A \cdot_{𝑜} suc \emptyset = (A \cdot_{𝑜} \emptyset) +_{𝑜} A$
6	2 5	eqtrid	$⊢ A \in On \to A \cdot_{𝑜} 1_{𝑜} = (A \cdot_{𝑜} \emptyset) +_{𝑜} A$
7		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
8	7	oveq1d	$⊢ A \in On \to (A \cdot_{𝑜} \emptyset) +_{𝑜} A = \emptyset +_{𝑜} A$
9		oa0r	$⊢ A \in On \to \emptyset +_{𝑜} A = A$
10	6 8 9	3eqtrd	$⊢ A \in On \to A \cdot_{𝑜} 1_{𝑜} = A$