# Metamath Proof Explorer

## Theorem onmsuc

Description: Multiplication with successor. Theorem 4J(A2) of Enderton p. 80. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion onmsuc ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\mathrm{suc}{B}=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}$

### Proof

Step Hyp Ref Expression
1 peano2 ${⊢}{B}\in \mathrm{\omega }\to \mathrm{suc}{B}\in \mathrm{\omega }$
2 nnon ${⊢}\mathrm{suc}{B}\in \mathrm{\omega }\to \mathrm{suc}{B}\in \mathrm{On}$
3 1 2 syl ${⊢}{B}\in \mathrm{\omega }\to \mathrm{suc}{B}\in \mathrm{On}$
4 omv ${⊢}\left({A}\in \mathrm{On}\wedge \mathrm{suc}{B}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\mathrm{suc}{B}=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left(\mathrm{suc}{B}\right)$
5 3 4 sylan2 ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\mathrm{suc}{B}=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left(\mathrm{suc}{B}\right)$
6 1 adantl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \mathrm{suc}{B}\in \mathrm{\omega }$
7 6 fvresd ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left(\mathrm{suc}{B}\right)$
8 5 7 eqtr4d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\mathrm{suc}{B}=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)$
9 ovex ${⊢}{A}{\cdot }_{𝑜}{B}\in \mathrm{V}$
10 oveq1 ${⊢}{x}={A}{\cdot }_{𝑜}{B}\to {x}{+}_{𝑜}{A}=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}$
11 eqid ${⊢}\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)=\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)$
12 ovex ${⊢}\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}\in \mathrm{V}$
13 10 11 12 fvmpt ${⊢}{A}{\cdot }_{𝑜}{B}\in \mathrm{V}\to \left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left({A}{\cdot }_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}$
14 9 13 ax-mp ${⊢}\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left({A}{\cdot }_{𝑜}{B}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}$
15 nnon ${⊢}{B}\in \mathrm{\omega }\to {B}\in \mathrm{On}$
16 omv ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}{B}=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left({B}\right)$
17 15 16 sylan2 ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{B}=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left({B}\right)$
18 fvres ${⊢}{B}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left({B}\right)$
19 18 adantl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)=\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)\left({B}\right)$
20 17 19 eqtr4d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{B}=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)$
21 20 fveq2d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left({A}{\cdot }_{𝑜}{B}\right)=\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)\right)$
22 14 21 syl5eqr ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}=\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)\right)$
23 frsuc ${⊢}{B}\in \mathrm{\omega }\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)=\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)\right)$
24 23 adantl ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)=\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right)\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left({B}\right)\right)$
25 22 24 eqtr4d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to \left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}=\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}{+}_{𝑜}{A}\right),\varnothing \right)↾}_{\mathrm{\omega }}\right)\left(\mathrm{suc}{B}\right)$
26 8 25 eqtr4d ${⊢}\left({A}\in \mathrm{On}\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\mathrm{suc}{B}=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}{A}$