Metamath Proof Explorer


Theorem mulslid

Description: Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion mulslid A No 1 s s A = A

Proof

Step Hyp Ref Expression
1 1sno 1 s No
2 mulscom 1 s No A No 1 s s A = A s 1 s
3 1 2 mpan A No 1 s s A = A s 1 s
4 mulsrid A No A s 1 s = A
5 3 4 eqtrd A No 1 s s A = A