Metamath Proof Explorer

Theorem slemuld

Description: An ordering relationship for surreal multiplication. Compare theorem 8(iii) of Conway p. 19. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses slemuld.1 
|- ( ph -> A e. No )
slemuld.2 
|- ( ph -> B e. No )
slemuld.3 
|- ( ph -> C e. No )
slemuld.4 
|- ( ph -> D e. No )
slemuld.5 
|- ( ph -> A <_s B )
slemuld.6 
|- ( ph -> C <_s D )
Assertion slemuld 
|- ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )

Proof

Step Hyp Ref Expression
1 slemuld.1 
 |-  ( ph -> A e. No )
2 slemuld.2 
 |-  ( ph -> B e. No )
3 slemuld.3 
 |-  ( ph -> C e. No )
4 slemuld.4 
 |-  ( ph -> D e. No )
5 slemuld.5 
 |-  ( ph -> A <_s B )
6 slemuld.6 
 |-  ( ph -> C <_s D )
7 1 4 mulscld 
 |-  ( ph -> ( A x.s D ) e. No )
8 1 3 mulscld 
 |-  ( ph -> ( A x.s C ) e. No )
9 7 8 subscld 
 |-  ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) e. No )
10 9 adantr 
 |-  ( ( ph /\ ( A  ( ( A x.s D ) -s ( A x.s C ) ) e. No )
11 2 4 mulscld 
 |-  ( ph -> ( B x.s D ) e. No )
12 2 3 mulscld 
 |-  ( ph -> ( B x.s C ) e. No )
13 11 12 subscld 
 |-  ( ph -> ( ( B x.s D ) -s ( B x.s C ) ) e. No )
14 13 adantr 
 |-  ( ( ph /\ ( A  ( ( B x.s D ) -s ( B x.s C ) ) e. No )
15 1 adantr 
 |-  ( ( ph /\ ( A  A e. No )
16 2 adantr 
 |-  ( ( ph /\ ( A  B e. No )
17 3 adantr 
 |-  ( ( ph /\ ( A  C e. No )
18 4 adantr 
 |-  ( ( ph /\ ( A  D e. No )
19 simprl 
 |-  ( ( ph /\ ( A  A
20 simprr 
 |-  ( ( ph /\ ( A  C
21 15 16 17 18 19 20 sltmuld 
 |-  ( ( ph /\ ( A  ( ( A x.s D ) -s ( A x.s C ) )
22 10 14 21 sltled 
 |-  ( ( ph /\ ( A  ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
23 22 anassrs 
 |-  ( ( ( ph /\ A  ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
24 0sno 
 |-  0s e. No
25 slerflex 
 |-  ( 0s e. No -> 0s <_s 0s )
26 24 25 mp1i 
 |-  ( ph -> 0s <_s 0s )
27 subsid 
 |-  ( ( A x.s D ) e. No -> ( ( A x.s D ) -s ( A x.s D ) ) = 0s )
28 7 27 syl 
 |-  ( ph -> ( ( A x.s D ) -s ( A x.s D ) ) = 0s )
29 subsid 
 |-  ( ( B x.s D ) e. No -> ( ( B x.s D ) -s ( B x.s D ) ) = 0s )
30 11 29 syl 
 |-  ( ph -> ( ( B x.s D ) -s ( B x.s D ) ) = 0s )
31 26 28 30 3brtr4d 
 |-  ( ph -> ( ( A x.s D ) -s ( A x.s D ) ) <_s ( ( B x.s D ) -s ( B x.s D ) ) )
32 oveq2 
 |-  ( C = D -> ( A x.s C ) = ( A x.s D ) )
33 32 oveq2d 
 |-  ( C = D -> ( ( A x.s D ) -s ( A x.s C ) ) = ( ( A x.s D ) -s ( A x.s D ) ) )
34 oveq2 
 |-  ( C = D -> ( B x.s C ) = ( B x.s D ) )
35 34 oveq2d 
 |-  ( C = D -> ( ( B x.s D ) -s ( B x.s C ) ) = ( ( B x.s D ) -s ( B x.s D ) ) )
36 33 35 breq12d 
 |-  ( C = D -> ( ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) <-> ( ( A x.s D ) -s ( A x.s D ) ) <_s ( ( B x.s D ) -s ( B x.s D ) ) ) )
37 31 36 syl5ibrcom 
 |-  ( ph -> ( C = D -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) )
38 37 imp 
 |-  ( ( ph /\ C = D ) -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
39 38 adantlr 
 |-  ( ( ( ph /\ A  ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
40 sleloe 
 |-  ( ( C e. No /\ D e. No ) -> ( C <_s D <-> ( C
41 3 4 40 syl2anc 
 |-  ( ph -> ( C <_s D <-> ( C
42 6 41 mpbid 
 |-  ( ph -> ( C
43 42 adantr 
 |-  ( ( ph /\ A  ( C
44 23 39 43 mpjaodan 
 |-  ( ( ph /\ A  ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
45 slerflex 
 |-  ( ( ( B x.s D ) -s ( B x.s C ) ) e. No -> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
46 13 45 syl 
 |-  ( ph -> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
47 oveq1 
 |-  ( A = B -> ( A x.s D ) = ( B x.s D ) )
48 oveq1 
 |-  ( A = B -> ( A x.s C ) = ( B x.s C ) )
49 47 48 oveq12d 
 |-  ( A = B -> ( ( A x.s D ) -s ( A x.s C ) ) = ( ( B x.s D ) -s ( B x.s C ) ) )
50 49 breq1d 
 |-  ( A = B -> ( ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) <-> ( ( B x.s D ) -s ( B x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) )
51 46 50 syl5ibrcom 
 |-  ( ph -> ( A = B -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) ) )
52 51 imp 
 |-  ( ( ph /\ A = B ) -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )
53 sleloe 
 |-  ( ( A e. No /\ B e. No ) -> ( A <_s B <-> ( A
54 1 2 53 syl2anc 
 |-  ( ph -> ( A <_s B <-> ( A
55 5 54 mpbid 
 |-  ( ph -> ( A
56 44 52 55 mpjaodan 
 |-  ( ph -> ( ( A x.s D ) -s ( A x.s C ) ) <_s ( ( B x.s D ) -s ( B x.s C ) ) )