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	Could not format assertion : No typesetting found for |- ( ( 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 ) ) } ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulsval	Could not format ( ( 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 ) ) } ) ) ) : No typesetting found for |- ( ( 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 ) ) } ) ) ) with typecode |-
2		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 ) ) } = { 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 ) ) } : 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 ) ) } = { 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 ) ) } with typecode |-
3		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 ) ) } = { 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 ) ) } : 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 ) ) } = { 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 ) ) } with typecode |-
4	2 3	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 ) ) } ) = ( { 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 ) ) } ) : 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 ) ) } ) = ( { 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 ) ) } ) with typecode |-
5		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 |-
6		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 |-
7	5 6	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 |-
8	4 7	oveq12i	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 ) ) } ) |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 ) ) } ) ) : 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 ) ) } ) |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 ) ) } ) ) with typecode |-
9	1 8	eqtr4di	Could not format ( ( 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 ) ) } ) ) ) : No typesetting found for |- ( ( 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 ) ) } ) ) ) with typecode |-