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