This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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