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