Metamath Proof Explorer

Theorem omsuc

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

		Ref	Expression
	Assertion	omsuc	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} suc B = (A \cdot_{𝑜} B) +_{𝑜} A$

Proof

Step	Hyp	Ref	Expression
1		rdgsuc	$⊢ B \in On \to rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (suc B) = (x \in V ⟼ x +_{𝑜} A) (rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B))$
2	1	adantl	$⊢ (A \in On \land B \in On) \to rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (suc B) = (x \in V ⟼ x +_{𝑜} A) (rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B))$
3		onsuc	$⊢ B \in On \to suc B \in On$
4		omv	$⊢ (A \in On \land suc B \in On) \to A \cdot_{𝑜} suc B = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (suc B)$
5	3 4	sylan2	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} suc B = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (suc B)$
6		ovex	$⊢ A \cdot_{𝑜} B \in V$
7		oveq1	$⊢ x = A \cdot_{𝑜} B \to x +_{𝑜} A = (A \cdot_{𝑜} B) +_{𝑜} A$
8		eqid	$⊢ (x \in V ⟼ x +_{𝑜} A) = (x \in V ⟼ x +_{𝑜} A)$
9		ovex	$⊢ (A \cdot_{𝑜} B) +_{𝑜} A \in V$
10	7 8 9	fvmpt	$⊢ A \cdot_{𝑜} B \in V \to (x \in V ⟼ x +_{𝑜} A) (A \cdot_{𝑜} B) = (A \cdot_{𝑜} B) +_{𝑜} A$
11	6 10	ax-mp	$⊢ (x \in V ⟼ x +_{𝑜} A) (A \cdot_{𝑜} B) = (A \cdot_{𝑜} B) +_{𝑜} A$
12		omv	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B = rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B)$
13	12	fveq2d	$⊢ (A \in On \land B \in On) \to (x \in V ⟼ x +_{𝑜} A) (A \cdot_{𝑜} B) = (x \in V ⟼ x +_{𝑜} A) (rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B))$
14	11 13	eqtr3id	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B) +_{𝑜} A = (x \in V ⟼ x +_{𝑜} A) (rec ((x \in V ⟼ x +_{𝑜} A), \emptyset) (B))$
15	2 5 14	3eqtr4d	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} suc B = (A \cdot_{𝑜} B) +_{𝑜} A$