Metamath Proof Explorer

Theorem mulscan2d

Description: Cancellation of surreal multiplication when the right term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses mulscan2d.1 
|- ( ph -> A e. No )
mulscan2d.2 
|- ( ph -> B e. No )
mulscan2d.3 
|- ( ph -> C e. No )
mulscan2d.4 
|- ( ph -> C =/= 0s )
Assertion mulscan2d 
|- ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 mulscan2d.1 
 |-  ( ph -> A e. No )
2 mulscan2d.2 
 |-  ( ph -> B e. No )
3 mulscan2d.3 
 |-  ( ph -> C e. No )
4 mulscan2d.4 
 |-  ( ph -> C =/= 0s )
5 0sno 
 |-  0s e. No
6 sltneg 
 |-  ( ( C e. No /\ 0s e. No ) -> ( C  ( -us ` 0s )
7 3 5 6 sylancl 
 |-  ( ph -> ( C  ( -us ` 0s )
8 negs0s 
 |-  ( -us ` 0s ) = 0s
9 8 breq1i 
 |-  ( ( -us ` 0s )  0s
10 7 9 bitrdi 
 |-  ( ph -> ( C  0s
11 1 3 mulnegs2d 
 |-  ( ph -> ( A x.s ( -us ` C ) ) = ( -us ` ( A x.s C ) ) )
12 2 3 mulnegs2d 
 |-  ( ph -> ( B x.s ( -us ` C ) ) = ( -us ` ( B x.s C ) ) )
13 11 12 eqeq12d 
 |-  ( ph -> ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) ) )
14 1 3 mulscld 
 |-  ( ph -> ( A x.s C ) e. No )
15 2 3 mulscld 
 |-  ( ph -> ( B x.s C ) e. No )
16 negs11 
 |-  ( ( ( A x.s C ) e. No /\ ( B x.s C ) e. No ) -> ( ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) <-> ( A x.s C ) = ( B x.s C ) ) )
17 14 15 16 syl2anc 
 |-  ( ph -> ( ( -us ` ( A x.s C ) ) = ( -us ` ( B x.s C ) ) <-> ( A x.s C ) = ( B x.s C ) ) )
18 13 17 bitrd 
 |-  ( ph -> ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( A x.s C ) = ( B x.s C ) ) )
19 18 adantr 
 |-  ( ( ph /\ 0s  ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> ( A x.s C ) = ( B x.s C ) ) )
20 1 adantr 
 |-  ( ( ph /\ 0s  A e. No )
21 2 adantr 
 |-  ( ( ph /\ 0s  B e. No )
22 3 negscld 
 |-  ( ph -> ( -us ` C ) e. No )
23 22 adantr 
 |-  ( ( ph /\ 0s  ( -us ` C ) e. No )
24 simpr 
 |-  ( ( ph /\ 0s  0s
25 20 21 23 24 mulscan2dlem 
 |-  ( ( ph /\ 0s  ( ( A x.s ( -us ` C ) ) = ( B x.s ( -us ` C ) ) <-> A = B ) )
26 19 25 bitr3d 
 |-  ( ( ph /\ 0s  ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )
27 10 26 sylbida 
 |-  ( ( ph /\ C  ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )
28 1 adantr 
 |-  ( ( ph /\ 0s  A e. No )
29 2 adantr 
 |-  ( ( ph /\ 0s  B e. No )
30 3 adantr 
 |-  ( ( ph /\ 0s  C e. No )
31 simpr 
 |-  ( ( ph /\ 0s  0s
32 28 29 30 31 mulscan2dlem 
 |-  ( ( ph /\ 0s  ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )
33 slttrine 
 |-  ( ( C e. No /\ 0s e. No ) -> ( C =/= 0s <-> ( C
34 3 5 33 sylancl 
 |-  ( ph -> ( C =/= 0s <-> ( C
35 4 34 mpbid 
 |-  ( ph -> ( C
36 27 32 35 mpjaodan 
 |-  ( ph -> ( ( A x.s C ) = ( B x.s C ) <-> A = B ) )