Theorem mulsproplem10

Description: Lemma for surreal multiplication. State the cut properties of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	No typesetting found for |- ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
	mulsproplem9.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsproplem9.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	mulsproplem10	Could not format assertion : No typesetting found for |- ( ph -> ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	Could not format ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
2		mulsproplem9.1	$$⊢\phi \to A\in \mathrm{No}$$
3		mulsproplem9.2	$$⊢\phi \to B\in \mathrm{No}$$
4	1 2 3	mulsproplem9	Could not format ( ph -> ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
5		scutcut	Could not format ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
6	4 5	syl	Could not format ( ph -> ( ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
7		mulsval	Could not format ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
8	2 3 7	syl2anc	Could not format ( ph -> ( A x.s B ) = ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ph -> ( A x.s B ) = ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
9	8	eleq1d	Could not format ( ph -> ( ( A x.s B ) e. No <-> ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No ) ) : No typesetting found for |- ( ph -> ( ( A x.s B ) e. No <-> ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No ) ) with typecode |-
10	8	sneqd	Could not format ( ph -> { ( A x.s B ) } = { ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) } ) : No typesetting found for |- ( ph -> { ( A x.s B ) } = { ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) } ) with typecode |-
11	10	breq2d	Could not format ( ph -> ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
12	10	breq1d	Could not format ( ph -> ( { ( A x.s B ) } < { ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) } < ( { ( A x.s B ) } < { ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) } <
13	9 11 12	3anbi123d	Could not format ( ph -> ( ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { i | E. t e. ( _Left ` A ) E. u e. ( _Right ` B ) i = ( ( ( t x.s B ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { j | E. v e. ( _Right ` A ) E. w e. ( _Left ` B ) j = ( ( ( v x.s B ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
14	6 13	mpbird	Could not format ( ph -> ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <