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

Proof

Step	Hyp	Ref	Expression
1		rdgsuc	⊢ ( 𝐵 ∈ On → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
2	1	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
3		suceloni	⊢ ( 𝐵 ∈ On → suc 𝐵 ∈ On )
4		omv	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
5	3 4	sylan2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ suc 𝐵 ) )
6		ovex	⊢ ( 𝐴 ·o 𝐵 ) ∈ V
7		oveq1	⊢ ( 𝑥 = ( 𝐴 ·o 𝐵 ) → ( 𝑥 +o 𝐴 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
8		eqid	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) )
9		ovex	⊢ ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) ∈ V
10	7 8 9	fvmpt	⊢ ( ( 𝐴 ·o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )
11	6 10	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 )
12		omv	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
13	12	fveq2d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( 𝐴 ·o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
14	11 13	syl5eqr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) ‘ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ) )
15	2 5 14	3eqtr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o suc 𝐵 ) = ( ( 𝐴 ·o 𝐵 ) +o 𝐴 ) )