Metamath Proof Explorer

Theorem divsmo

Description: Uniqueness of surreal inversion. Given a non-zero surreal A , there is at most one surreal giving a particular product. (Contributed by Scott Fenton, 10-Mar-2025)

		Ref	Expression
	Assertion	divsmo	$⊢ (A \in No \land A \neq 0_{s}) \to \exists^{*} x \in No A \cdot_{s} x = B$

Proof

Step	Hyp	Ref	Expression
1		eqtr3	$⊢ (A \cdot_{s} x = B \land A \cdot_{s} y = B) \to A \cdot_{s} x = A \cdot_{s} y$
2		simprl	$⊢ ((A \in No \land A \neq 0_{s}) \land (x \in No \land y \in No)) \to x \in No$
3		simprr	$⊢ ((A \in No \land A \neq 0_{s}) \land (x \in No \land y \in No)) \to y \in No$
4		simpll	$⊢ ((A \in No \land A \neq 0_{s}) \land (x \in No \land y \in No)) \to A \in No$
5		simplr	$⊢ ((A \in No \land A \neq 0_{s}) \land (x \in No \land y \in No)) \to A \neq 0_{s}$
6	2 3 4 5	mulscan1d	$⊢ ((A \in No \land A \neq 0_{s}) \land (x \in No \land y \in No)) \to (A \cdot_{s} x = A \cdot_{s} y \leftrightarrow x = y)$
7	1 6	imbitrid	$⊢ ((A \in No \land A \neq 0_{s}) \land (x \in No \land y \in No)) \to ((A \cdot_{s} x = B \land A \cdot_{s} y = B) \to x = y)$
8	7	ralrimivva	$⊢ (A \in No \land A \neq 0_{s}) \to \forall x \in No \forall y \in No ((A \cdot_{s} x = B \land A \cdot_{s} y = B) \to x = y)$
9		oveq2	$⊢ x = y \to A \cdot_{s} x = A \cdot_{s} y$
10	9	eqeq1d	$⊢ x = y \to (A \cdot_{s} x = B \leftrightarrow A \cdot_{s} y = B)$
11	10	rmo4	$⊢ \exists^{*} x \in No A \cdot_{s} x = B \leftrightarrow \forall x \in No \forall y \in No ((A \cdot_{s} x = B \land A \cdot_{s} y = B) \to x = y)$
12	8 11	sylibr	$⊢ (A \in No \land A \neq 0_{s}) \to \exists^{*} x \in No A \cdot_{s} x = B$