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 
|- ( ph -> L <
mulsunif.2 
|- ( ph -> M <
mulsunif.3 
|- ( ph -> A = ( L |s R ) )
mulsunif.4 
|- ( ph -> B = ( M |s S ) )
Assertion mulsunif 
|- ( ph -> ( A x.s B ) = ( ( { a | E. p e. L E. q e. M a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. R E. s e. S b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. L E. u e. S c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. R E. w e. M d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) )

Proof

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