Metamath Proof Explorer

Theorem mulscut

Description: Show the cut properties of surreal multiplication. (Contributed by Scott Fenton, 8-Mar-2025)

		Ref	Expression
	Hypotheses	mulscut.1	$⊢ φ \to A \in No$
		mulscut.2	$⊢ φ \to B \in No$
	Assertion	mulscut	Could not format assertion : No typesetting found for \|- ( ph -> ( ( A x.s B ) e. No /\ ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

Step	Hyp	Ref	Expression
1		mulscut.1	$⊢ φ \to A \in No$
2		mulscut.2	$⊢ φ \to B \in No$
3	1 2	mulscutlem	Could not format ( ph -> ( ( A x.s B ) e. No /\ ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) < ( ( A x.s B ) e. No /\ ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) <
4		biid	Could not format ( ( A x.s B ) e. No <-> ( A x.s B ) e. No ) : No typesetting found for \|- ( ( A x.s B ) e. No <-> ( A x.s B ) e. No ) with typecode \|-
5		mulsval2lem	Could not format { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } = { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } : No typesetting found for \|- { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } = { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } with typecode \|-
6		mulsval2lem	Could not format { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } = { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } : No typesetting found for \|- { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } = { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } with typecode \|-
7	5 6	uneq12i	Could not format ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) = ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) : No typesetting found for \|- ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) = ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) with typecode \|-
8	7	breq1i	Could not format ( ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) < ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) <
9		mulsval2lem	Could not format { c \| E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } = { l \| E. m e. ( _Left ` A ) E. n e. ( _Right ` B ) l = ( ( ( m x.s B ) +s ( A x.s n ) ) -s ( m x.s n ) ) } : No typesetting found for \|- { c \| E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } = { l \| E. m e. ( _Left ` A ) E. n e. ( _Right ` B ) l = ( ( ( m x.s B ) +s ( A x.s n ) ) -s ( m x.s n ) ) } with typecode \|-
10		mulsval2lem	Could not format { d \| E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } = { o \| E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) o = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } : No typesetting found for \|- { d \| E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } = { o \| E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) o = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } with typecode \|-
11	9 10	uneq12i	Could not format ( { c \| E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d \| E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) = ( { l \| E. m e. ( _Left ` A ) E. n e. ( _Right ` B ) l = ( ( ( m x.s B ) +s ( A x.s n ) ) -s ( m x.s n ) ) } u. { o \| E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) o = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) : No typesetting found for \|- ( { c \| E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) c = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d \| E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) d = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) = ( { l \| E. m e. ( _Left ` A ) E. n e. ( _Right ` B ) l = ( ( ( m x.s B ) +s ( A x.s n ) ) -s ( m x.s n ) ) } u. { o \| E. x e. ( _Right ` A ) E. y e. ( _Left ` B ) o = ( ( ( x x.s B ) +s ( A x.s y ) ) -s ( x x.s y ) ) } ) with typecode \|-
12	11	breq2i	Could not format ( { ( A x.s B ) } < ~~{ ( A x.s B ) } < ~~{ ( A x.s B ) } <~~~~
13	4 8 12	3anbi123i	Could not format ( ( ( A x.s B ) e. No /\ ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( A x.s B ) e. No /\ ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) < ( ( A x.s B ) e. No /\ ( { f \| E. g e. ( _Left ` A ) E. h e. ( _Left ` B ) f = ( ( ( g x.s B ) +s ( A x.s h ) ) -s ( g x.s h ) ) } u. { i \| E. j e. ( _Right ` A ) E. k e. ( _Right ` B ) i = ( ( ( j x.s B ) +s ( A x.s k ) ) -s ( j x.s k ) ) } ) <
14	3 13	sylibr	Could not format ( ph -> ( ( A x.s B ) e. No /\ ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( A x.s B ) e. No /\ ( { a \| E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b \| E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <