Theorem mulscut

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

	Ref	Expression
Hypotheses	mulscut.1	|- ( ph -> A e. No )
	mulscut.2	|- ( ph -> B e. No )
Assertion	mulscut	|- ( 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	|- ( ph -> A e. No )
2		mulscut.2	|- ( ph -> B e. No )
3	1 2	mulscutlem	|- ( 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 ) ) } ) <
4		biid	|- ( ( A x.s B ) e. No <-> ( A x.s B ) e. No )
5		mulsval2lem	|- { 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 ) ) }
6		mulsval2lem	|- { 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 ) ) }
7	5 6	uneq12i	|- ( { 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 ) ) } )
8	7	breq1i	|- ( ( { 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 ) ) } ) <
9		mulsval2lem	|- { 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 ) ) }
10		mulsval2lem	|- { 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 ) ) }
11	9 10	uneq12i	|- ( { 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 ) ) } )
12	11	breq2i	|- ( { ( A x.s B ) } < { ( A x.s B ) } <
13	4 8 12	3anbi123i	|- ( ( ( 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 ) ) } ) <
14	3 13	sylibr	|- ( 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 ) ) } ) <