Theorem mulsval2

Description: The value of surreal multiplication, expressed with fewer distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025)

	Ref	Expression
Assertion	mulsval2	|- ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { 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 ) ) } ) |s ( { 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 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulsval	|- ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. k e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s k ) ) -s ( i x.s k ) ) } ) |s ( { 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 ) ) } ) ) )
2		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 ) ) } = { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) }
3		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 ) ) } = { h | E. i e. ( _Right ` A ) E. k e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s k ) ) -s ( i x.s k ) ) }
4	2 3	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 ) ) } ) = ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. k e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s k ) ) -s ( i x.s k ) ) } )
5		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 ) ) }
6		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 ) ) }
7	5 6	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 ) ) } )
8	4 7	oveq12i	|- ( ( { 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 ) ) } ) |s ( { 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 ) ) } ) ) = ( ( { e | E. f e. ( _Left ` A ) E. g e. ( _Left ` B ) e = ( ( ( f x.s B ) +s ( A x.s g ) ) -s ( f x.s g ) ) } u. { h | E. i e. ( _Right ` A ) E. k e. ( _Right ` B ) h = ( ( ( i x.s B ) +s ( A x.s k ) ) -s ( i x.s k ) ) } ) |s ( { 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 ) ) } ) )
9	1 8	eqtr4di	|- ( ( A e. No /\ B e. No ) -> ( A x.s B ) = ( ( { 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 ) ) } ) |s ( { 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 ) ) } ) ) )