Theorem precsexlem1

Description: Lemma for surreal reciprocals. Calculate the value of the recursive left function at zero. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	precsexlem.1	|- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
	precsexlem.2	|- L = ( 1st o. F )
	precsexlem.3	|- R = ( 2nd o. F )
Assertion	precsexlem1	|- ( L ` (/) ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		precsexlem.1	|- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
2		precsexlem.2	|- L = ( 1st o. F )
3		precsexlem.3	|- R = ( 2nd o. F )
4	2	fveq1i	|- ( L ` (/) ) = ( ( 1st o. F ) ` (/) )
5		rdgfnon	|- rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) Fn On
6	1	fneq1i	|- ( F Fn On <-> rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) Fn On )
7	5 6	mpbir	|- F Fn On
8		0elon	|- (/) e. On
9		fvco2	|- ( ( F Fn On /\ (/) e. On ) -> ( ( 1st o. F ) ` (/) ) = ( 1st ` ( F ` (/) ) ) )
10	7 8 9	mp2an	|- ( ( 1st o. F ) ` (/) ) = ( 1st ` ( F ` (/) ) )
11	1	fveq1i	|- ( F ` (/) ) = ( rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) ` (/) )
12		opex	|- <. { 0s } , (/) >. e. _V
13	12	rdg0	|- ( rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) ` (/) ) = <. { 0s } , (/) >.
14	11 13	eqtri	|- ( F ` (/) ) = <. { 0s } , (/) >.
15	14	fveq2i	|- ( 1st ` ( F ` (/) ) ) = ( 1st ` <. { 0s } , (/) >. )
16		snex	|- { 0s } e. _V
17		0ex	|- (/) e. _V
18	16 17	op1st	|- ( 1st ` <. { 0s } , (/) >. ) = { 0s }
19	15 18	eqtri	|- ( 1st ` ( F ` (/) ) ) = { 0s }
20	4 10 19	3eqtri	|- ( L ` (/) ) = { 0s }