Metamath Proof Explorer

Theorem precsexlemcbv

Description: Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025)

Ref Expression
Hypothesis 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 } , (/) >. )
Assertion precsexlemcbv 
|- F = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 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 fveq2 
 |-  ( p = q -> ( 1st ` p ) = ( 1st ` q ) )
3 fveq2 
 |-  ( p = q -> ( 2nd ` p ) = ( 2nd ` q ) )
4 3 csbeq1d 
 |-  ( p = q -> [_ ( 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 . = [_ ( 2nd ` q ) / 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 . )
5 2 4 csbeq12dv 
 |-  ( p = q -> [_ ( 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 . = [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / 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 . )
6 rexeq 
 |-  ( r = s -> ( E. yR e. r a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> E. yR e. s a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
7 6 rexbidv 
 |-  ( r = s -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
8 7 abbidv 
 |-  ( r = s -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
9 8 uneq2d 
 |-  ( r = s -> ( { 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
10 9 uneq2d 
 |-  ( r = s -> ( 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
11 id 
 |-  ( r = s -> r = s )
12 rexeq 
 |-  ( r = s -> ( E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
13 12 rexbidv 
 |-  ( r = s -> ( E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
14 13 abbidv 
 |-  ( r = s -> { a | E. xR e. ( _Right ` A ) E. yR e. r a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { a | E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } )
15 14 uneq2d 
 |-  ( r = s -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
16 11 15 uneq12d 
 |-  ( r = s -> ( r u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
17 10 16 opeq12d 
 |-  ( r = s -> <. ( 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 . = <. ( 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 . )
18 eqeq1 
 |-  ( a = b -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
19 18 2rexbidv 
 |-  ( a = b -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. l b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
20 oveq1 
 |-  ( xR = zR -> ( xR -s A ) = ( zR -s A ) )
21 20 oveq1d 
 |-  ( xR = zR -> ( ( xR -s A ) x.s yL ) = ( ( zR -s A ) x.s yL ) )
22 21 oveq2d 
 |-  ( xR = zR -> ( 1s +s ( ( xR -s A ) x.s yL ) ) = ( 1s +s ( ( zR -s A ) x.s yL ) ) )
23 id 
 |-  ( xR = zR -> xR = zR )
24 22 23 oveq12d 
 |-  ( xR = zR -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) )
25 24 eqeq2d 
 |-  ( xR = zR -> ( b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) ) )
26 oveq2 
 |-  ( yL = w -> ( ( zR -s A ) x.s yL ) = ( ( zR -s A ) x.s w ) )
27 26 oveq2d 
 |-  ( yL = w -> ( 1s +s ( ( zR -s A ) x.s yL ) ) = ( 1s +s ( ( zR -s A ) x.s w ) ) )
28 27 oveq1d 
 |-  ( yL = w -> ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) )
29 28 eqeq2d 
 |-  ( yL = w -> ( b = ( ( 1s +s ( ( zR -s A ) x.s yL ) ) /su zR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) )
30 25 29 cbvrex2vw 
 |-  ( E. xR e. ( _Right ` A ) E. yL e. l b = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) )
31 19 30 bitrdi 
 |-  ( a = b -> ( E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) )
32 31 cbvabv 
 |-  { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } = { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) }
33 eqeq1 
 |-  ( a = b -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> b = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
34 33 2rexbidv 
 |-  ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
35 oveq1 
 |-  ( xL = zL -> ( xL -s A ) = ( zL -s A ) )
36 35 oveq1d 
 |-  ( xL = zL -> ( ( xL -s A ) x.s yR ) = ( ( zL -s A ) x.s yR ) )
37 36 oveq2d 
 |-  ( xL = zL -> ( 1s +s ( ( xL -s A ) x.s yR ) ) = ( 1s +s ( ( zL -s A ) x.s yR ) ) )
38 id 
 |-  ( xL = zL -> xL = zL )
39 37 38 oveq12d 
 |-  ( xL = zL -> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) )
40 39 eqeq2d 
 |-  ( xL = zL -> ( b = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) ) )
41 oveq2 
 |-  ( yR = t -> ( ( zL -s A ) x.s yR ) = ( ( zL -s A ) x.s t ) )
42 41 oveq2d 
 |-  ( yR = t -> ( 1s +s ( ( zL -s A ) x.s yR ) ) = ( 1s +s ( ( zL -s A ) x.s t ) ) )
43 42 oveq1d 
 |-  ( yR = t -> ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) = ( ( 1s +s ( ( zL -s A ) x.s t ) ) /su zL ) )
44 43 eqeq2d 
 |-  ( yR = t -> ( b = ( ( 1s +s ( ( zL -s A ) x.s yR ) ) /su zL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s t ) ) /su zL ) ) )
45 40 44 cbvrex2vw 
 |-  ( E. xL e. { x e. ( _Left ` A ) | 0s  E. zL e. { x e. ( _Left ` A ) | 0s
46 breq2 
 |-  ( x = z -> ( 0s  0s
47 46 cbvrabv 
 |-  { x e. ( _Left ` A ) | 0s
48 47 rexeqi 
 |-  ( E. zL e. { x e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
49 45 48 bitri 
 |-  ( E. xL e. { x e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
50 34 49 bitrdi 
 |-  ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
51 50 cbvabv 
 |-  { a | E. xL e. { x e. ( _Left ` A ) | 0s
52 32 51 uneq12i 
 |-  ( { 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
53 52 uneq2i 
 |-  ( 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
54 eqeq1 
 |-  ( a = b -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> b = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) )
55 54 2rexbidv 
 |-  ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
56 35 oveq1d 
 |-  ( xL = zL -> ( ( xL -s A ) x.s yL ) = ( ( zL -s A ) x.s yL ) )
57 56 oveq2d 
 |-  ( xL = zL -> ( 1s +s ( ( xL -s A ) x.s yL ) ) = ( 1s +s ( ( zL -s A ) x.s yL ) ) )
58 57 38 oveq12d 
 |-  ( xL = zL -> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) )
59 58 eqeq2d 
 |-  ( xL = zL -> ( b = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) ) )
60 oveq2 
 |-  ( yL = w -> ( ( zL -s A ) x.s yL ) = ( ( zL -s A ) x.s w ) )
61 60 oveq2d 
 |-  ( yL = w -> ( 1s +s ( ( zL -s A ) x.s yL ) ) = ( 1s +s ( ( zL -s A ) x.s w ) ) )
62 61 oveq1d 
 |-  ( yL = w -> ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) )
63 62 eqeq2d 
 |-  ( yL = w -> ( b = ( ( 1s +s ( ( zL -s A ) x.s yL ) ) /su zL ) <-> b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) )
64 59 63 cbvrex2vw 
 |-  ( E. xL e. { x e. ( _Left ` A ) | 0s  E. zL e. { x e. ( _Left ` A ) | 0s
65 47 rexeqi 
 |-  ( E. zL e. { x e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
66 64 65 bitri 
 |-  ( E. xL e. { x e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
67 55 66 bitrdi 
 |-  ( a = b -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
68 67 cbvabv 
 |-  { a | E. xL e. { x e. ( _Left ` A ) | 0s
69 eqeq1 
 |-  ( a = b -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
70 69 2rexbidv 
 |-  ( a = b -> ( E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. s b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
71 20 oveq1d 
 |-  ( xR = zR -> ( ( xR -s A ) x.s yR ) = ( ( zR -s A ) x.s yR ) )
72 71 oveq2d 
 |-  ( xR = zR -> ( 1s +s ( ( xR -s A ) x.s yR ) ) = ( 1s +s ( ( zR -s A ) x.s yR ) ) )
73 72 23 oveq12d 
 |-  ( xR = zR -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) )
74 73 eqeq2d 
 |-  ( xR = zR -> ( b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) ) )
75 oveq2 
 |-  ( yR = t -> ( ( zR -s A ) x.s yR ) = ( ( zR -s A ) x.s t ) )
76 75 oveq2d 
 |-  ( yR = t -> ( 1s +s ( ( zR -s A ) x.s yR ) ) = ( 1s +s ( ( zR -s A ) x.s t ) ) )
77 76 oveq1d 
 |-  ( yR = t -> ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) )
78 77 eqeq2d 
 |-  ( yR = t -> ( b = ( ( 1s +s ( ( zR -s A ) x.s yR ) ) /su zR ) <-> b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) )
79 74 78 cbvrex2vw 
 |-  ( E. xR e. ( _Right ` A ) E. yR e. s b = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) )
80 70 79 bitrdi 
 |-  ( a = b -> ( E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) ) )
81 80 cbvabv 
 |-  { a | E. xR e. ( _Right ` A ) E. yR e. s a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } = { b | E. zR e. ( _Right ` A ) E. t e. s b = ( ( 1s +s ( ( zR -s A ) x.s t ) ) /su zR ) }
82 68 81 uneq12i 
 |-  ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
83 82 uneq2i 
 |-  ( s u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
84 53 83 opeq12i 
 |-  <. ( 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 . = <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s .
85 17 84 eqtrdi 
 |-  ( r = s -> <. ( 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 . = <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . )
86 85 cbvcsbv 
 |-  [_ ( 2nd ` q ) / 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 . = [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s .
87 86 csbeq2i 
 |-  [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / 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 . = [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s .
88 id 
 |-  ( l = m -> l = m )
89 rexeq 
 |-  ( l = m -> ( E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) <-> E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) )
90 89 rexbidv 
 |-  ( l = m -> ( E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) <-> E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) ) )
91 90 abbidv 
 |-  ( l = m -> { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } = { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } )
92 91 uneq1d 
 |-  ( l = m -> ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s
93 88 92 uneq12d 
 |-  ( l = m -> ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s
94 rexeq 
 |-  ( l = m -> ( E. w e. l b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) <-> E. w e. m b = ( ( 1s +s ( ( zL -s A ) x.s w ) ) /su zL ) ) )
95 94 rexbidv 
 |-  ( l = m -> ( E. zL e. { z e. ( _Left ` A ) | 0s  E. zL e. { z e. ( _Left ` A ) | 0s
96 95 abbidv 
 |-  ( l = m -> { b | E. zL e. { z e. ( _Left ` A ) | 0s
97 96 uneq1d 
 |-  ( l = m -> ( { b | E. zL e. { z e. ( _Left ` A ) | 0s
98 97 uneq2d 
 |-  ( l = m -> ( s u. ( { b | E. zL e. { z e. ( _Left ` A ) | 0s
99 93 98 opeq12d 
 |-  ( l = m -> <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . )
100 99 csbeq2dv 
 |-  ( l = m -> [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . )
101 100 cbvcsbv 
 |-  [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / s ]_ <. ( l u. ( { b | E. zR e. ( _Right ` A ) E. w e. l b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s .
102 87 101 eqtri 
 |-  [_ ( 1st ` q ) / l ]_ [_ ( 2nd ` q ) / 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 . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s .
103 5 102 eqtrdi 
 |-  ( p = q -> [_ ( 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 . = [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . )
104 103 cbvmptv 
 |-  ( 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 . ) = ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . )
105 rdgeq1 
 |-  ( ( 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 . ) = ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) -> 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 } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) )
106 104 105 ax-mp 
 |-  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 } , (/) >. ) = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
107 1 106 eqtri 
 |-  F = rec ( ( q e. _V |-> [_ ( 1st ` q ) / m ]_ [_ ( 2nd ` q ) / s ]_ <. ( m u. ( { b | E. zR e. ( _Right ` A ) E. w e. m b = ( ( 1s +s ( ( zR -s A ) x.s w ) ) /su zR ) } u. { b | E. zL e. { z e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )