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	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃* 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqtr3	⊢ ( ( ( 𝐴 ·s 𝑥 ) = 𝐵 ∧ ( 𝐴 ·s 𝑦 ) = 𝐵 ) → ( 𝐴 ·s 𝑥 ) = ( 𝐴 ·s 𝑦 ) )
2		simprl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) ∧ ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ) → 𝑥 ∈ No )
3		simprr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) ∧ ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ) → 𝑦 ∈ No )
4		simpll	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) ∧ ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ) → 𝐴 ∈ No )
5		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) ∧ ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ) → 𝐴 ≠ 0s )
6	2 3 4 5	mulscan1d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) ∧ ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ) → ( ( 𝐴 ·s 𝑥 ) = ( 𝐴 ·s 𝑦 ) ↔ 𝑥 = 𝑦 ) )
7	1 6	imbitrid	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) ∧ ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ) → ( ( ( 𝐴 ·s 𝑥 ) = 𝐵 ∧ ( 𝐴 ·s 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
8	7	ralrimivva	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( 𝐴 ·s 𝑥 ) = 𝐵 ∧ ( 𝐴 ·s 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
9		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·s 𝑥 ) = ( 𝐴 ·s 𝑦 ) )
10	9	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·s 𝑥 ) = 𝐵 ↔ ( 𝐴 ·s 𝑦 ) = 𝐵 ) )
11	10	rmo4	⊢ ( ∃* 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 𝐵 ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( 𝐴 ·s 𝑥 ) = 𝐵 ∧ ( 𝐴 ·s 𝑦 ) = 𝐵 ) → 𝑥 = 𝑦 ) )
12	8 11	sylibr	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃* 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 𝐵 )