Metamath Proof Explorer

Theorem expsval

Description: The value of surreal exponentiation. (Contributed by Scott Fenton, 24-Jul-2025)

Ref Expression
Assertion expsval 
|- ( ( A e. No /\ B e. ZZ_s ) -> ( A ^su B ) = if ( B = 0s , 1s , if ( 0s

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( x = A -> 1s = 1s )
2 eqidd 
 |-  ( x = A -> x.s = x.s )
3 sneq 
 |-  ( x = A -> { x } = { A } )
4 3 xpeq2d 
 |-  ( x = A -> ( NN_s X. { x } ) = ( NN_s X. { A } ) )
5 1 2 4 seqseq123d 
 |-  ( x = A -> seq_s 1s ( x.s , ( NN_s X. { x } ) ) = seq_s 1s ( x.s , ( NN_s X. { A } ) ) )
6 5 fveq1d 
 |-  ( x = A -> ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` y ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` y ) )
7 5 fveq1d 
 |-  ( x = A -> ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` ( -us ` y ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) )
8 7 oveq2d 
 |-  ( x = A -> ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` ( -us ` y ) ) ) = ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) ) )
9 6 8 ifeq12d 
 |-  ( x = A -> if ( 0s
10 9 ifeq2d 
 |-  ( x = A -> if ( y = 0s , 1s , if ( 0s
11 eqeq1 
 |-  ( y = B -> ( y = 0s <-> B = 0s ) )
12 breq2 
 |-  ( y = B -> ( 0s  0s
13 fveq2 
 |-  ( y = B -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` y ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` B ) )
14 2fveq3 
 |-  ( y = B -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` B ) ) )
15 14 oveq2d 
 |-  ( y = B -> ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) ) = ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` B ) ) ) )
16 12 13 15 ifbieq12d 
 |-  ( y = B -> if ( 0s
17 11 16 ifbieq2d 
 |-  ( y = B -> if ( y = 0s , 1s , if ( 0s
18 df-exps 
 |-  ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s
19 1sno 
 |-  1s e. No
20 19 elexi 
 |-  1s e. _V
21 fvex 
 |-  ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` B ) e. _V
22 ovex 
 |-  ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` B ) ) ) e. _V
23 21 22 ifex 
 |-  if ( 0s
24 20 23 ifex 
 |-  if ( B = 0s , 1s , if ( 0s
25 10 17 18 24 ovmpo 
 |-  ( ( A e. No /\ B e. ZZ_s ) -> ( A ^su B ) = if ( B = 0s , 1s , if ( 0s