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 2 oldnod 
 |-  ( ph -> X e. No )
5 0no 
 |-  0s e. No
6 5 a1i 
 |-  ( ph -> 0s e. No )
7 bday0 
 |-  ( bday ` 0s ) = (/)
8 7 7 oveq12i 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) )
9 0elon 
 |-  (/) e. On
10 naddrid 
 |-  ( (/) e. On -> ( (/) +no (/) ) = (/) )
11 9 10 ax-mp 
 |-  ( (/) +no (/) ) = (/)
12 8 11 eqtri 
 |-  ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/)
13 12 12 uneq12i 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( (/) u. (/) )
14 un0 
 |-  ( (/) u. (/) ) = (/)
15 13 14 eqtri 
 |-  ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/)
16 15 15 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. (/) )
17 16 14 eqtri 
 |-  ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/)
18 17 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. (/) )
19 un0 
 |-  ( ( ( bday ` X ) +no ( bday ` B ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` B ) )
20 18 19 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 ) )
21 oldbdayim 
 |-  ( X e. ( _Old ` ( bday ` A ) ) -> ( bday ` X ) e. ( bday ` A ) )
22 2 21 syl 
 |-  ( ph -> ( bday ` X ) e. ( bday ` A ) )
23 bdayon 
 |-  ( bday ` X ) e. On
24 bdayon 
 |-  ( bday ` A ) e. On
25 bdayon 
 |-  ( bday ` B ) e. On
26 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 ) ) ) )
27 23 24 25 26 mp3an 
 |-  ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
28 22 27 sylib 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
29 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 ) ) ) ) ) )
30 28 29 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 ) ) ) ) ) )
31 20 30 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 ) ) ) ) ) )
32 1 4 3 6 6 6 6 31 mulsproplem1 
 |-  ( ph -> ( ( X x.s B ) e. No /\ ( ( 0s  ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
33 32 simpld 
 |-  ( ph -> ( X x.s B ) e. No )