Metamath Proof Explorer

Theorem mulsproplem2

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and B itself is a surreal number. (Contributed by Scott Fenton, 4-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 ) )
mulsproplem2.1 
|- ( ph -> X e. ( _Old ` ( bday ` A ) ) )
mulsproplem2.2 
|- ( ph -> B e. No )
Assertion mulsproplem2 
|- ( ph -> ( X 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 mulsproplem2.1 
 |-  ( ph -> X e. ( _Old ` ( bday ` A ) ) )
3 mulsproplem2.2 
 |-  ( ph -> B e. No )
4 oldssno 
 |-  ( _Old ` ( bday ` A ) ) C_ No
5 4 2 sselid 
 |-  ( ph -> X e. No )
6 0sno 
 |-  0s e. No
7 6 a1i 
 |-  ( ph -> 0s e. No )
8 bday0s 
 |-  ( bday ` 0s ) = (/)
9 8 8 oveq12i 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) )
10 0elon 
 |-  (/) e. On
11 naddrid 
 |-  ( (/) e. On -> ( (/) +no (/) ) = (/) )
12 10 11 ax-mp 
 |-  ( (/) +no (/) ) = (/)
13 9 12 eqtri 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/)
14 13 13 uneq12i 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( (/) u. (/) )
15 un0 
 |-  ( (/) u. (/) ) = (/)
16 14 15 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/)
17 16 16 uneq12i 
 |-  ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( (/) u. (/) )
18 17 15 eqtri 
 |-  ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/)
19 18 uneq2i 
 |-  ( ( ( bday ` X ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` B ) ) u. (/) )
20 un0 
 |-  ( ( ( bday ` X ) +no ( bday ` B ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` B ) )
21 19 20 eqtri 
 |-  ( ( ( bday ` X ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` X ) +no ( bday ` B ) )
22 oldbdayim 
 |-  ( X e. ( _Old ` ( bday ` A ) ) -> ( bday ` X ) e. ( bday ` A ) )
23 2 22 syl 
 |-  ( ph -> ( bday ` X ) e. ( bday ` A ) )
24 bdayelon 
 |-  ( bday ` X ) e. On
25 bdayelon 
 |-  ( bday ` A ) e. On
26 bdayelon 
 |-  ( bday ` B ) e. On
27 naddel1 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
28 24 25 26 27 mp3an 
 |-  ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
29 23 28 sylib 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
30 elun1 
 |-  ( ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` B ) ) 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 ) ) ) ) ) )
31 29 30 syl 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` B ) ) 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 ) ) ) ) ) )
32 21 31 eqeltrid 
 |-  ( ph -> ( ( ( bday ` X ) +no ( bday ` B ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) 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 ) ) ) ) ) )
33 1 5 3 7 7 7 7 32 mulsproplem1 
 |-  ( ph -> ( ( X x.s B ) e. No /\ ( ( 0s  ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
34 33 simpld 
 |-  ( ph -> ( X x.s B ) e. No )