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	$$⊢\phi \to L{\ll }_{s}R$$
	mulsunif.2	$$⊢\phi \to M{\ll }_{s}S$$
	mulsunif.3	$$⊢\phi \to A=L{|}_{s}R$$
	mulsunif.4	$$⊢\phi \to B=M{|}_{s}S$$
Assertion	mulsunif	Could not format assertion : No typesetting found for |- ( 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 ) ) } ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulsunif.1	$$⊢\phi \to L{\ll }_{s}R$$
2		mulsunif.2	$$⊢\phi \to M{\ll }_{s}S$$
3		mulsunif.3	$$⊢\phi \to A=L{|}_{s}R$$
4		mulsunif.4	$$⊢\phi \to B=M{|}_{s}S$$
5	1 2 3 4	mulsuniflem	Could not format ( 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 ) ) } ) ) ) : No typesetting found for |- ( 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 ) ) } ) ) ) with typecode |-
6		mulsval2lem	Could not format { 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 ) ) } : No typesetting found for |- { 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 ) ) } with typecode |-
7		mulsval2lem	Could not format { 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 ) ) } : No typesetting found for |- { 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 ) ) } with typecode |-
8	6 7	uneq12i	Could not format ( { 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 ) ) } ) : No typesetting found for |- ( { 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 ) ) } ) with typecode |-
9		mulsval2lem	Could not format { 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 ) ) } : No typesetting found for |- { 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 ) ) } with typecode |-
10		mulsval2lem	Could not format { 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 ) ) } : No typesetting found for |- { 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 ) ) } with typecode |-
11	9 10	uneq12i	Could not format ( { 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 ) ) } ) : No typesetting found for |- ( { 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 ) ) } ) with typecode |-
12	8 11	oveq12i	Could not format ( ( { 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 ) ) } ) ) : No typesetting found for |- ( ( { 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 ) ) } ) ) with typecode |-
13	5 12	eqtr4di	Could not format ( 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 ) ) } ) ) ) : No typesetting found for |- ( 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 ) ) } ) ) ) with typecode |-