Metamath Proof Explorer


Theorem ssltmul2

Description: One surreal set less-than relationship for cuts of A and B . (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses ssltmul2.1 φ L s R
ssltmul2.2 φ M s S
ssltmul2.3 φ A = L | s R
ssltmul2.4 φ B = M | s S
Assertion ssltmul2 φ A s B s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w

Proof

Step Hyp Ref Expression
1 ssltmul2.1 φ L s R
2 ssltmul2.2 φ M s S
3 ssltmul2.3 φ A = L | s R
4 ssltmul2.4 φ B = M | s S
5 snex A s B V
6 5 a1i φ A s B V
7 eqid t L , u S t s B + s A s u - s t s u = t L , u S t s B + s A s u - s t s u
8 7 rnmpo ran t L , u S t s B + s A s u - s t s u = c | t L u S c = t s B + s A s u - s t s u
9 ssltex1 L s R L V
10 1 9 syl φ L V
11 ssltex2 M s S S V
12 2 11 syl φ S V
13 7 mpoexg L V S V t L , u S t s B + s A s u - s t s u V
14 10 12 13 syl2anc φ t L , u S t s B + s A s u - s t s u V
15 rnexg t L , u S t s B + s A s u - s t s u V ran t L , u S t s B + s A s u - s t s u V
16 14 15 syl φ ran t L , u S t s B + s A s u - s t s u V
17 8 16 eqeltrrid φ c | t L u S c = t s B + s A s u - s t s u V
18 eqid v R , w M v s B + s A s w - s v s w = v R , w M v s B + s A s w - s v s w
19 18 rnmpo ran v R , w M v s B + s A s w - s v s w = d | v R w M d = v s B + s A s w - s v s w
20 ssltex2 L s R R V
21 1 20 syl φ R V
22 ssltex1 M s S M V
23 2 22 syl φ M V
24 18 mpoexg R V M V v R , w M v s B + s A s w - s v s w V
25 21 23 24 syl2anc φ v R , w M v s B + s A s w - s v s w V
26 rnexg v R , w M v s B + s A s w - s v s w V ran v R , w M v s B + s A s w - s v s w V
27 25 26 syl φ ran v R , w M v s B + s A s w - s v s w V
28 19 27 eqeltrrid φ d | v R w M d = v s B + s A s w - s v s w V
29 17 28 unexd φ c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w V
30 1 scutcld φ L | s R No
31 3 30 eqeltrd φ A No
32 2 scutcld φ M | s S No
33 4 32 eqeltrd φ B No
34 31 33 mulscld φ A s B No
35 34 snssd φ A s B No
36 ssltss1 L s R L No
37 1 36 syl φ L No
38 37 adantr φ t L u S L No
39 simprl φ t L u S t L
40 38 39 sseldd φ t L u S t No
41 33 adantr φ t L u S B No
42 40 41 mulscld φ t L u S t s B No
43 31 adantr φ t L u S A No
44 ssltss2 M s S S No
45 2 44 syl φ S No
46 45 adantr φ t L u S S No
47 simprr φ t L u S u S
48 46 47 sseldd φ t L u S u No
49 43 48 mulscld φ t L u S A s u No
50 42 49 addscld φ t L u S t s B + s A s u No
51 40 48 mulscld φ t L u S t s u No
52 50 51 subscld φ t L u S t s B + s A s u - s t s u No
53 eleq1 c = t s B + s A s u - s t s u c No t s B + s A s u - s t s u No
54 52 53 syl5ibrcom φ t L u S c = t s B + s A s u - s t s u c No
55 54 rexlimdvva φ t L u S c = t s B + s A s u - s t s u c No
56 55 abssdv φ c | t L u S c = t s B + s A s u - s t s u No
57 ssltss2 L s R R No
58 1 57 syl φ R No
59 58 adantr φ v R w M R No
60 simprl φ v R w M v R
61 59 60 sseldd φ v R w M v No
62 33 adantr φ v R w M B No
63 61 62 mulscld φ v R w M v s B No
64 31 adantr φ v R w M A No
65 ssltss1 M s S M No
66 2 65 syl φ M No
67 66 adantr φ v R w M M No
68 simprr φ v R w M w M
69 67 68 sseldd φ v R w M w No
70 64 69 mulscld φ v R w M A s w No
71 63 70 addscld φ v R w M v s B + s A s w No
72 61 69 mulscld φ v R w M v s w No
73 71 72 subscld φ v R w M v s B + s A s w - s v s w No
74 eleq1 d = v s B + s A s w - s v s w d No v s B + s A s w - s v s w No
75 73 74 syl5ibrcom φ v R w M d = v s B + s A s w - s v s w d No
76 75 rexlimdvva φ v R w M d = v s B + s A s w - s v s w d No
77 76 abssdv φ d | v R w M d = v s B + s A s w - s v s w No
78 56 77 unssd φ c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w No
79 elun y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w y c | t L u S c = t s B + s A s u - s t s u y d | v R w M d = v s B + s A s w - s v s w
80 vex y V
81 eqeq1 c = y c = t s B + s A s u - s t s u y = t s B + s A s u - s t s u
82 81 2rexbidv c = y t L u S c = t s B + s A s u - s t s u t L u S y = t s B + s A s u - s t s u
83 80 82 elab y c | t L u S c = t s B + s A s u - s t s u t L u S y = t s B + s A s u - s t s u
84 eqeq1 d = y d = v s B + s A s w - s v s w y = v s B + s A s w - s v s w
85 84 2rexbidv d = y v R w M d = v s B + s A s w - s v s w v R w M y = v s B + s A s w - s v s w
86 80 85 elab y d | v R w M d = v s B + s A s w - s v s w v R w M y = v s B + s A s w - s v s w
87 83 86 orbi12i y c | t L u S c = t s B + s A s u - s t s u y d | v R w M d = v s B + s A s w - s v s w t L u S y = t s B + s A s u - s t s u v R w M y = v s B + s A s w - s v s w
88 79 87 bitri y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w t L u S y = t s B + s A s u - s t s u v R w M y = v s B + s A s w - s v s w
89 scutcut L s R L | s R No L s L | s R L | s R s R
90 1 89 syl φ L | s R No L s L | s R L | s R s R
91 90 simp2d φ L s L | s R
92 91 adantr φ t L u S L s L | s R
93 ovex L | s R V
94 93 snid L | s R L | s R
95 3 94 eqeltrdi φ A L | s R
96 95 adantr φ t L u S A L | s R
97 92 39 96 ssltsepcd φ t L u S t < s A
98 scutcut M s S M | s S No M s M | s S M | s S s S
99 2 98 syl φ M | s S No M s M | s S M | s S s S
100 99 simp3d φ M | s S s S
101 100 adantr φ t L u S M | s S s S
102 ovex M | s S V
103 102 snid M | s S M | s S
104 4 103 eqeltrdi φ B M | s S
105 104 adantr φ t L u S B M | s S
106 101 105 47 ssltsepcd φ t L u S B < s u
107 40 43 41 48 97 106 sltmuld φ t L u S t s u - s t s B < s A s u - s A s B
108 34 adantr φ t L u S A s B No
109 51 42 49 108 sltsubsub2bd φ t L u S t s u - s t s B < s A s u - s A s B A s B - s A s u < s t s B - s t s u
110 42 51 subscld φ t L u S t s B - s t s u No
111 108 49 110 sltsubaddd φ t L u S A s B - s A s u < s t s B - s t s u A s B < s t s B - s t s u + s A s u
112 109 111 bitrd φ t L u S t s u - s t s B < s A s u - s A s B A s B < s t s B - s t s u + s A s u
113 107 112 mpbid φ t L u S A s B < s t s B - s t s u + s A s u
114 42 49 51 addsubsd φ t L u S t s B + s A s u - s t s u = t s B - s t s u + s A s u
115 113 114 breqtrrd φ t L u S A s B < s t s B + s A s u - s t s u
116 breq2 y = t s B + s A s u - s t s u A s B < s y A s B < s t s B + s A s u - s t s u
117 115 116 syl5ibrcom φ t L u S y = t s B + s A s u - s t s u A s B < s y
118 117 rexlimdvva φ t L u S y = t s B + s A s u - s t s u A s B < s y
119 90 simp3d φ L | s R s R
120 119 adantr φ v R w M L | s R s R
121 95 adantr φ v R w M A L | s R
122 120 121 60 ssltsepcd φ v R w M A < s v
123 99 simp2d φ M s M | s S
124 123 adantr φ v R w M M s M | s S
125 104 adantr φ v R w M B M | s S
126 124 68 125 ssltsepcd φ v R w M w < s B
127 64 61 69 62 122 126 sltmuld φ v R w M A s B - s A s w < s v s B - s v s w
128 34 adantr φ v R w M A s B No
129 63 72 subscld φ v R w M v s B - s v s w No
130 128 70 129 sltsubaddd φ v R w M A s B - s A s w < s v s B - s v s w A s B < s v s B - s v s w + s A s w
131 127 130 mpbid φ v R w M A s B < s v s B - s v s w + s A s w
132 63 70 72 addsubsd φ v R w M v s B + s A s w - s v s w = v s B - s v s w + s A s w
133 131 132 breqtrrd φ v R w M A s B < s v s B + s A s w - s v s w
134 breq2 y = v s B + s A s w - s v s w A s B < s y A s B < s v s B + s A s w - s v s w
135 133 134 syl5ibrcom φ v R w M y = v s B + s A s w - s v s w A s B < s y
136 135 rexlimdvva φ v R w M y = v s B + s A s w - s v s w A s B < s y
137 118 136 jaod φ t L u S y = t s B + s A s u - s t s u v R w M y = v s B + s A s w - s v s w A s B < s y
138 88 137 biimtrid φ y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w A s B < s y
139 velsn x A s B x = A s B
140 breq1 x = A s B x < s y A s B < s y
141 140 imbi2d x = A s B y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w x < s y y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w A s B < s y
142 139 141 sylbi x A s B y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w x < s y y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w A s B < s y
143 138 142 syl5ibrcom φ x A s B y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w x < s y
144 143 3imp φ x A s B y c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w x < s y
145 6 29 35 78 144 ssltd φ A s B s c | t L u S c = t s B + s A s u - s t s u d | v R w M d = v s B + s A s w - s v s w