Metamath Proof Explorer


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 eqtrid
 |-  ( 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 )