Metamath Proof Explorer


Theorem omsuc

Description: Multiplication with successor. Definition 8.15 of TakeutiZaring p. 62. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion omsuc
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )

Proof

Step Hyp Ref Expression
1 rdgsuc
 |-  ( B e. On -> ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) )
2 1 adantl
 |-  ( ( A e. On /\ B e. On ) -> ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) )
3 suceloni
 |-  ( B e. On -> suc B e. On )
4 omv
 |-  ( ( A e. On /\ suc B e. On ) -> ( A .o suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) )
5 3 4 sylan2
 |-  ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` suc B ) )
6 ovex
 |-  ( A .o B ) e. _V
7 oveq1
 |-  ( x = ( A .o B ) -> ( x +o A ) = ( ( A .o B ) +o A ) )
8 eqid
 |-  ( x e. _V |-> ( x +o A ) ) = ( x e. _V |-> ( x +o A ) )
9 ovex
 |-  ( ( A .o B ) +o A ) e. _V
10 7 8 9 fvmpt
 |-  ( ( A .o B ) e. _V -> ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( A .o B ) +o A ) )
11 6 10 ax-mp
 |-  ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( A .o B ) +o A )
12 omv
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
13 12 fveq2d
 |-  ( ( A e. On /\ B e. On ) -> ( ( x e. _V |-> ( x +o A ) ) ` ( A .o B ) ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) )
14 11 13 eqtr3id
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) +o A ) = ( ( x e. _V |-> ( x +o A ) ) ` ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) ) )
15 2 5 14 3eqtr4d
 |-  ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )