Theorem mulsproplem11

Description: Lemma for surreal multiplication. Under the inductive hypothesis, demonstrate closure of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	|- ( 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	|- ( ph -> A e. No )
	mulsproplem9.2	|- ( ph -> B e. No )
Assertion	mulsproplem11	|- ( ph -> ( A x.s B ) e. No )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	|- ( 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 ) )
2		mulsproplem9.1	|- ( ph -> A e. No )
3		mulsproplem9.2	|- ( ph -> B e. No )
4	1 2 3	mulsproplem10	|- ( 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 ) ) } ) <
5	4	simp1d	|- ( ph -> ( A x.s B ) e. No )