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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		peano2	⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω )
2		nnon	⊢ ( suc 𝐵 ∈ ω → suc 𝐵 ∈ On )
3	1 2	syl	⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ On )
4		omv	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
5	3 4	sylan2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
6	1	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → suc 𝐵 ∈ ω )
7	6	fvresd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
8	5 7	eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) )
9		ovex	⊢ ( 𝐴 ·o 𝐵 ) ∈ V
10		oveq1	⊢ ( 𝑥 = ( 𝐴 ·o 𝐵 ) → ( 𝑥 +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
11		eqid	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) )
12		ovex	⊢ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) ∈ V
13	10 11 12	fvmpt	⊢ ( ( 𝐴 ·o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
14	9 13	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 )
15		nnon	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
16		omv	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
17	15 16	sylan2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
18		fvres	⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
19	18	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
20	17 19	eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) )
21	20	fveq2d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
22	14 21	eqtr3id	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
23		frsuc	⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
24	23	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ 𝐵 ) ) )
25	22 24	eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ↾ ω ) ‘ suc 𝐵 ) )
26	8 25	eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )