Theorem divs1

Description: A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Assertion	divs1	⊢ ( 𝐴 ∈ No → ( 𝐴 /su 1s ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mulslid	⊢ ( 𝐴 ∈ No → ( 1s ·s 𝐴 ) = 𝐴 )
2		1sno	⊢ 1s ∈ No
3		1sne0s	⊢ 1s ≠ 0s
4	2 3	pm3.2i	⊢ ( 1s ∈ No ∧ 1s ≠ 0s )
5		mulslid	⊢ ( 1s ∈ No → ( 1s ·s 1s ) = 1s )
6	2 5	ax-mp	⊢ ( 1s ·s 1s ) = 1s
7		oveq2	⊢ ( 𝑥 = 1s → ( 1s ·s 𝑥 ) = ( 1s ·s 1s ) )
8	7	eqeq1d	⊢ ( 𝑥 = 1s → ( ( 1s ·s 𝑥 ) = 1s ↔ ( 1s ·s 1s ) = 1s ) )
9	8	rspcev	⊢ ( ( 1s ∈ No ∧ ( 1s ·s 1s ) = 1s ) → ∃ 𝑥 ∈ No ( 1s ·s 𝑥 ) = 1s )
10	2 6 9	mp2an	⊢ ∃ 𝑥 ∈ No ( 1s ·s 𝑥 ) = 1s
11		divsmulw	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐴 ∈ No ∧ ( 1s ∈ No ∧ 1s ≠ 0s ) ) ∧ ∃ 𝑥 ∈ No ( 1s ·s 𝑥 ) = 1s ) → ( ( 𝐴 /su 1s ) = 𝐴 ↔ ( 1s ·s 𝐴 ) = 𝐴 ) )
12	10 11	mpan2	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ∈ No ∧ ( 1s ∈ No ∧ 1s ≠ 0s ) ) → ( ( 𝐴 /su 1s ) = 𝐴 ↔ ( 1s ·s 𝐴 ) = 𝐴 ) )
13	4 12	mp3an3	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ∈ No ) → ( ( 𝐴 /su 1s ) = 𝐴 ↔ ( 1s ·s 𝐴 ) = 𝐴 ) )
14	13	anidms	⊢ ( 𝐴 ∈ No → ( ( 𝐴 /su 1s ) = 𝐴 ↔ ( 1s ·s 𝐴 ) = 𝐴 ) )
15	1 14	mpbird	⊢ ( 𝐴 ∈ No → ( 𝐴 /su 1s ) = 𝐴 )