Metamath Proof Explorer


Theorem mulsunif

Description: Surreal multiplication has the uniformity property. That is, any cuts that define A and B can be used in the definition of ( A x.s B ) . Theorem 3.5 of Gonshor p. 18. (Contributed by Scott Fenton, 7-Mar-2025)

Ref Expression
Hypotheses mulsunif.1 φ L s R
mulsunif.2 φ M s S
mulsunif.3 φ A = L | s R
mulsunif.4 φ B = M | s S
Assertion mulsunif φ A s B = a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s | 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 mulsunif.1 φ L s R
2 mulsunif.2 φ M s S
3 mulsunif.3 φ A = L | s R
4 mulsunif.4 φ B = M | s S
5 1 2 3 4 mulsuniflem φ A s B = e | f L g M e = f s B + s A s g - s f s g h | i R j S h = i s B + s A s j - s i s j | s k | l L m S k = l s B + s A s m - s l s m n | o R x M n = o s B + s A s x - s o s x
6 mulsval2lem a | p L q M a = p s B + s A s q - s p s q = e | f L g M e = f s B + s A s g - s f s g
7 mulsval2lem b | r R s S b = r s B + s A s s - s r s s = h | i R j S h = i s B + s A s j - s i s j
8 6 7 uneq12i a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s = e | f L g M e = f s B + s A s g - s f s g h | i R j S h = i s B + s A s j - s i s j
9 mulsval2lem c | t L u S c = t s B + s A s u - s t s u = k | l L m S k = l s B + s A s m - s l s m
10 mulsval2lem d | v R w M d = v s B + s A s w - s v s w = n | o R x M n = o s B + s A s x - s o s x
11 9 10 uneq12i 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 = k | l L m S k = l s B + s A s m - s l s m n | o R x M n = o s B + s A s x - s o s x
12 8 11 oveq12i a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s | 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 = e | f L g M e = f s B + s A s g - s f s g h | i R j S h = i s B + s A s j - s i s j | s k | l L m S k = l s B + s A s m - s l s m n | o R x M n = o s B + s A s x - s o s x
13 5 12 eqtr4di φ A s B = a | p L q M a = p s B + s A s q - s p s q b | r R s S b = r s B + s A s s - s r s s | 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