Theorem om1

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

	Ref	Expression
Assertion	om1	|- ( A e. On -> ( A .o 1o ) = A )

Proof

Step	Hyp	Ref	Expression
1		df-1o	|- 1o = suc (/)
2	1	oveq2i	|- ( A .o 1o ) = ( A .o suc (/) )
3		peano1	|- (/) e. _om
4		onmsuc	|- ( ( A e. On /\ (/) e. _om ) -> ( A .o suc (/) ) = ( ( A .o (/) ) +o A ) )
5	3 4	mpan2	|- ( A e. On -> ( A .o suc (/) ) = ( ( A .o (/) ) +o A ) )
6	2 5	syl5eq	|- ( A e. On -> ( A .o 1o ) = ( ( A .o (/) ) +o A ) )
7		om0	|- ( A e. On -> ( A .o (/) ) = (/) )
8	7	oveq1d	|- ( A e. On -> ( ( A .o (/) ) +o A ) = ( (/) +o A ) )
9		oa0r	|- ( A e. On -> ( (/) +o A ) = A )
10	6 8 9	3eqtrd	|- ( A e. On -> ( A .o 1o ) = A )