Metamath Proof Explorer

Theorem mulsproplem4

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and a member of the old set of B 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 ) )
mulsproplem4.1 
|- ( ph -> X e. ( _Old ` ( bday ` A ) ) )
mulsproplem4.2 
|- ( ph -> Y e. ( _Old ` ( bday ` B ) ) )
Assertion mulsproplem4 
|- ( ph -> ( X x.s Y ) 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 mulsproplem4.1 
 |-  ( ph -> X e. ( _Old ` ( bday ` A ) ) )
3 mulsproplem4.2 
 |-  ( ph -> Y e. ( _Old ` ( bday ` B ) ) )
4 2 oldnod 
 |-  ( ph -> X e. No )
5 3 oldnod 
 |-  ( ph -> Y e. No )
6 0no 
 |-  0s e. No
7 6 a1i 
 |-  ( ph -> 0s e. No )
8 bday0 
 |-  ( 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 ` Y ) ) 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 ` Y ) ) u. (/) )
20 un0 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` Y ) )
21 19 20 eqtri 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ` Y ) )
22 oldbdayim 
 |-  ( X e. ( _Old ` ( bday ` A ) ) -> ( bday ` X ) e. ( bday ` A ) )
23 2 22 syl 
 |-  ( ph -> ( bday ` X ) e. ( bday ` A ) )
24 oldbdayim 
 |-  ( Y e. ( _Old ` ( bday ` B ) ) -> ( bday ` Y ) e. ( bday ` B ) )
25 3 24 syl 
 |-  ( ph -> ( bday ` Y ) e. ( bday ` B ) )
26 bdayon 
 |-  ( bday ` A ) e. On
27 bdayon 
 |-  ( bday ` B ) e. On
28 naddel12 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` X ) e. ( bday ` A ) /\ ( bday ` Y ) e. ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) )
29 26 27 28 mp2an 
 |-  ( ( ( bday ` X ) e. ( bday ` A ) /\ ( bday ` Y ) e. ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
30 23 25 29 syl2anc 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) )
31 elun1 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) 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 30 31 syl 
 |-  ( ph -> ( ( bday ` X ) +no ( bday ` Y ) ) 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 21 32 eqeltrid 
 |-  ( ph -> ( ( ( bday ` X ) +no ( bday ` Y ) ) 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 ) ) ) ) ) )
34 1 4 5 7 7 7 7 33 mulsproplem1 
 |-  ( ph -> ( ( X x.s Y ) e. No /\ ( ( 0s  ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
35 34 simpld 
 |-  ( ph -> ( X x.s Y ) e. No )