Metamath Proof Explorer

Theorem precsexlem9

Description: Lemma for surreal reciprocal. Show that the product of A and a left element is less than one and the product of A and a right element is greater than one. (Contributed by Scott Fenton, 14-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 )
precsexlem.4 
|- ( ph -> A e. No )
precsexlem.5 
|- ( ph -> 0s
precsexlem.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
Assertion precsexlem9 
|- ( ( ph /\ I e. _om ) -> ( A. b e. ( L ` I ) ( A x.s b )

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 precsexlem.4 
 |-  ( ph -> A e. No )
5 precsexlem.5 
 |-  ( ph -> 0s
6 precsexlem.6 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
7 fveq2 
 |-  ( i = (/) -> ( L ` i ) = ( L ` (/) ) )
8 7 raleqdv 
 |-  ( i = (/) -> ( A. b e. ( L ` i ) ( A x.s b )  A. b e. ( L ` (/) ) ( A x.s b )
9 fveq2 
 |-  ( i = (/) -> ( R ` i ) = ( R ` (/) ) )
10 9 raleqdv 
 |-  ( i = (/) -> ( A. c e. ( R ` i ) 1s  A. c e. ( R ` (/) ) 1s
11 8 10 anbi12d 
 |-  ( i = (/) -> ( ( A. b e. ( L ` i ) ( A x.s b )  ( A. b e. ( L ` (/) ) ( A x.s b )
12 11 imbi2d 
 |-  ( i = (/) -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b )  ( ph -> ( A. b e. ( L ` (/) ) ( A x.s b )
13 fveq2 
 |-  ( i = j -> ( L ` i ) = ( L ` j ) )
14 13 raleqdv 
 |-  ( i = j -> ( A. b e. ( L ` i ) ( A x.s b )  A. b e. ( L ` j ) ( A x.s b )
15 fveq2 
 |-  ( i = j -> ( R ` i ) = ( R ` j ) )
16 15 raleqdv 
 |-  ( i = j -> ( A. c e. ( R ` i ) 1s  A. c e. ( R ` j ) 1s
17 14 16 anbi12d 
 |-  ( i = j -> ( ( A. b e. ( L ` i ) ( A x.s b )  ( A. b e. ( L ` j ) ( A x.s b )
18 17 imbi2d 
 |-  ( i = j -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b )  ( ph -> ( A. b e. ( L ` j ) ( A x.s b )
19 fveq2 
 |-  ( i = suc j -> ( L ` i ) = ( L ` suc j ) )
20 19 raleqdv 
 |-  ( i = suc j -> ( A. b e. ( L ` i ) ( A x.s b )  A. b e. ( L ` suc j ) ( A x.s b )
21 fveq2 
 |-  ( i = suc j -> ( R ` i ) = ( R ` suc j ) )
22 21 raleqdv 
 |-  ( i = suc j -> ( A. c e. ( R ` i ) 1s  A. c e. ( R ` suc j ) 1s
23 20 22 anbi12d 
 |-  ( i = suc j -> ( ( A. b e. ( L ` i ) ( A x.s b )  ( A. b e. ( L ` suc j ) ( A x.s b )
24 oveq2 
 |-  ( b = r -> ( A x.s b ) = ( A x.s r ) )
25 24 breq1d 
 |-  ( b = r -> ( ( A x.s b )  ( A x.s r )
26 25 cbvralvw 
 |-  ( A. b e. ( L ` suc j ) ( A x.s b )  A. r e. ( L ` suc j ) ( A x.s r )
27 oveq2 
 |-  ( c = s -> ( A x.s c ) = ( A x.s s ) )
28 27 breq2d 
 |-  ( c = s -> ( 1s  1s
29 28 cbvralvw 
 |-  ( A. c e. ( R ` suc j ) 1s  A. s e. ( R ` suc j ) 1s
30 26 29 anbi12i 
 |-  ( ( A. b e. ( L ` suc j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
31 23 30 bitrdi 
 |-  ( i = suc j -> ( ( A. b e. ( L ` i ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
32 31 imbi2d 
 |-  ( i = suc j -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b )  ( ph -> ( A. r e. ( L ` suc j ) ( A x.s r )
33 fveq2 
 |-  ( i = I -> ( L ` i ) = ( L ` I ) )
34 33 raleqdv 
 |-  ( i = I -> ( A. b e. ( L ` i ) ( A x.s b )  A. b e. ( L ` I ) ( A x.s b )
35 fveq2 
 |-  ( i = I -> ( R ` i ) = ( R ` I ) )
36 35 raleqdv 
 |-  ( i = I -> ( A. c e. ( R ` i ) 1s  A. c e. ( R ` I ) 1s
37 34 36 anbi12d 
 |-  ( i = I -> ( ( A. b e. ( L ` i ) ( A x.s b )  ( A. b e. ( L ` I ) ( A x.s b )
38 37 imbi2d 
 |-  ( i = I -> ( ( ph -> ( A. b e. ( L ` i ) ( A x.s b )  ( ph -> ( A. b e. ( L ` I ) ( A x.s b )
39 muls01 
 |-  ( A e. No -> ( A x.s 0s ) = 0s )
40 4 39 syl 
 |-  ( ph -> ( A x.s 0s ) = 0s )
41 0slt1s 
 |-  0s
42 40 41 eqbrtrdi 
 |-  ( ph -> ( A x.s 0s )
43 1 2 3 precsexlem1 
 |-  ( L ` (/) ) = { 0s }
44 43 raleqi 
 |-  ( A. b e. ( L ` (/) ) ( A x.s b )  A. b e. { 0s } ( A x.s b )
45 0sno 
 |-  0s e. No
46 45 elexi 
 |-  0s e. _V
47 oveq2 
 |-  ( b = 0s -> ( A x.s b ) = ( A x.s 0s ) )
48 47 breq1d 
 |-  ( b = 0s -> ( ( A x.s b )  ( A x.s 0s )
49 46 48 ralsn 
 |-  ( A. b e. { 0s } ( A x.s b )  ( A x.s 0s )
50 44 49 bitri 
 |-  ( A. b e. ( L ` (/) ) ( A x.s b )  ( A x.s 0s )
51 42 50 sylibr 
 |-  ( ph -> A. b e. ( L ` (/) ) ( A x.s b )
52 ral0 
 |-  A. c e. (/) 1s
53 1 2 3 precsexlem2 
 |-  ( R ` (/) ) = (/)
54 53 raleqi 
 |-  ( A. c e. ( R ` (/) ) 1s  A. c e. (/) 1s
55 52 54 mpbir 
 |-  A. c e. ( R ` (/) ) 1s
56 51 55 jctir 
 |-  ( ph -> ( A. b e. ( L ` (/) ) ( A x.s b )
57 1 2 3 precsexlem4 
 |-  ( j e. _om -> ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
58 57 3ad2ant2 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
59 58 eleq2d 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r e. ( L ` suc j ) <-> r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
60 elun 
 |-  ( r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( r e. ( L ` j ) \/ r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
61 elun 
 |-  ( r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
62 vex 
 |-  r e. _V
63 eqeq1 
 |-  ( a = r -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
64 63 2rexbidv 
 |-  ( a = r -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
65 62 64 elab 
 |-  ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
66 eqeq1 
 |-  ( a = r -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
67 66 2rexbidv 
 |-  ( a = r -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
68 62 67 elab 
 |-  ( r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
69 65 68 orbi12i 
 |-  ( ( r e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
70 61 69 bitri 
 |-  ( r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
71 70 orbi2i 
 |-  ( ( r e. ( L ` j ) \/ r e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
72 60 71 bitri 
 |-  ( r e. ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
73 59 72 bitrdi 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r e. ( L ` suc j ) <-> ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s
74 simp3l 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. b e. ( L ` j ) ( A x.s b )
75 25 rspccv 
 |-  ( A. b e. ( L ` j ) ( A x.s b )  ( r e. ( L ` j ) -> ( A x.s r )
76 74 75 syl 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r e. ( L ` j ) -> ( A x.s r )
77 4 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
78 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
79 1sno 
 |-  1s e. No
80 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
81 rightssno 
 |-  ( _Right ` A ) C_ No
82 81 sseli 
 |-  ( xR e. ( _Right ` A ) -> xR e. No )
83 82 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. No )
84 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
85 83 84 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A ) e. No )
86 85 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A ) e. No )
87 1 2 3 4 5 6 precsexlem8 
 |-  ( ( ph /\ j e. _om ) -> ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) )
88 87 simpld 
 |-  ( ( ph /\ j e. _om ) -> ( L ` j ) C_ No )
89 88 3adant3 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( L ` j ) C_ No )
90 89 sselda 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yL e. No )
91 90 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yL e. No )
92 86 91 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s yL ) e. No )
93 80 92 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xR -s A ) x.s yL ) ) e. No )
94 83 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. No )
95 45 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s e. No )
96 5 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
97 96 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
98 rightgt 
 |-  ( xR e. ( _Right ` A ) -> A
99 98 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A
100 95 84 83 97 99 slttrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
101 100 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR =/= 0s )
102 101 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR =/= 0s )
103 breq2 
 |-  ( xO = xR -> ( 0s  0s
104 oveq1 
 |-  ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) )
105 104 eqeq1d 
 |-  ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) )
106 105 rexbidv 
 |-  ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) )
107 103 106 imbi12d 
 |-  ( xO = xR -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xR x.s y ) = 1s ) ) )
108 6 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
109 108 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
110 elun2 
 |-  ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
111 110 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
112 107 109 111 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 0s  E. y e. No ( xR x.s y ) = 1s ) )
113 100 112 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xR x.s y ) = 1s )
114 113 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xR x.s y ) = 1s )
115 78 93 94 102 114 divsasswd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
116 oveq2 
 |-  ( b = yL -> ( A x.s b ) = ( A x.s yL ) )
117 116 breq1d 
 |-  ( b = yL -> ( ( A x.s b )  ( A x.s yL )
118 117 rspccva 
 |-  ( ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
119 74 118 sylan 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
120 119 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
121 78 91 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL ) e. No )
122 84 83 posdifsd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A  0s
123 99 122 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
124 123 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
125 121 80 86 124 sltmul2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s yL )  ( ( xR -s A ) x.s ( A x.s yL ) )
126 120 125 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s ( A x.s yL ) )
127 86 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s 1s ) = ( xR -s A ) )
128 126 127 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s ( A x.s yL ) )
129 86 121 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s ( A x.s yL ) ) e. No )
130 78 129 94 sltaddsub2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) )  ( ( xR -s A ) x.s ( A x.s yL ) )
131 128 130 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) )
132 78 80 92 addsdid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) )
133 78 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
134 78 86 91 muls12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( ( xR -s A ) x.s yL ) ) = ( ( xR -s A ) x.s ( A x.s yL ) ) )
135 133 134 oveq12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) )
136 132 135 eqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) )
137 94 mulslidd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xR ) = xR )
138 131 136 137 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) )
139 78 93 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) e. No )
140 100 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
141 139 80 94 140 114 sltdivmul2wd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) )
142 138 141 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR )
143 115 142 eqbrtrrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
144 oveq2 
 |-  ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) )
145 144 breq1d 
 |-  ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( ( A x.s r )  ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )
146 143 145 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r )
147 146 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r )
148 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
149 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
150 leftssno 
 |-  ( _Left ` A ) C_ No
151 elrabi 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( _Left ` A ) )
152 151 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. ( _Left ` A ) )
153 150 152 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. No )
154 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
155 153 154 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A ) e. No )
156 155 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A ) e. No )
157 87 simprd 
 |-  ( ( ph /\ j e. _om ) -> ( R ` j ) C_ No )
158 157 3adant3 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( R ` j ) C_ No )
159 158 sselda 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yR e. No )
160 159 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yR e. No )
161 156 160 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s yR ) e. No )
162 149 161 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xL -s A ) x.s yR ) ) e. No )
163 153 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. No )
164 breq2 
 |-  ( x = xL -> ( 0s  0s
165 164 elrab 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  ( xL e. ( _Left ` A ) /\ 0s
166 165 simprbi 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  0s
167 166 adantl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
168 167 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL =/= 0s )
169 168 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL =/= 0s )
170 breq2 
 |-  ( xO = xL -> ( 0s  0s
171 oveq1 
 |-  ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) )
172 171 eqeq1d 
 |-  ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) )
173 172 rexbidv 
 |-  ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) )
174 170 173 imbi12d 
 |-  ( xO = xL -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xL x.s y ) = 1s ) ) )
175 108 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
176 elun1 
 |-  ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
177 152 176 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
178 174 175 177 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 0s  E. y e. No ( xL x.s y ) = 1s ) )
179 167 178 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xL x.s y ) = 1s )
180 179 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xL x.s y ) = 1s )
181 148 162 163 169 180 divsasswd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
182 154 153 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL ) e. No )
183 182 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL ) e. No )
184 183 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s 1s ) = ( A -s xL ) )
185 simp3r 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. c e. ( R ` j ) 1s
186 oveq2 
 |-  ( c = yR -> ( A x.s c ) = ( A x.s yR ) )
187 186 breq2d 
 |-  ( c = yR -> ( 1s  1s
188 187 rspccva 
 |-  ( ( A. c e. ( R ` j ) 1s  1s
189 185 188 sylan 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
190 189 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
191 148 160 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yR ) e. No )
192 leftlt 
 |-  ( xL e. ( _Left ` A ) -> xL
193 152 192 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL
194 153 154 posdifsd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL  0s
195 193 194 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
196 195 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
197 149 191 183 196 sltmul2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s  ( ( A -s xL ) x.s 1s )
198 190 197 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s 1s )
199 184 198 eqbrtrrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL )
200 153 154 negsubsdi2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) ) = ( A -s xL ) )
201 200 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) ) = ( A -s xL ) )
202 156 191 mulnegs1d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) )
203 200 oveq1d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) )
204 203 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) )
205 202 204 eqtr3d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) )
206 199 201 205 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) )
207 156 191 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s ( A x.s yR ) ) e. No )
208 207 156 sltnegd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( ( xL -s A ) x.s ( A x.s yR ) )  ( -us ` ( xL -s A ) )
209 206 208 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s ( A x.s yR ) )
210 148 207 163 sltaddsub2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) )  ( ( xL -s A ) x.s ( A x.s yR ) )
211 209 210 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) )
212 148 149 161 addsdid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) )
213 148 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
214 148 156 160 muls12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( ( xL -s A ) x.s yR ) ) = ( ( xL -s A ) x.s ( A x.s yR ) ) )
215 213 214 oveq12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) )
216 212 215 eqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) )
217 163 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL x.s 1s ) = xL )
218 211 216 217 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) )
219 148 162 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) e. No )
220 167 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
221 219 149 163 220 180 sltdivmulwd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) )
222 218 221 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL )
223 181 222 eqbrtrrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) )
224 oveq2 
 |-  ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) )
225 224 breq1d 
 |-  ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( ( A x.s r )  ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) )
226 223 225 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r )
227 226 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( E. xL e. { x e. ( _Left ` A ) | 0s  ( A x.s r )
228 147 227 jaod 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s  ( A x.s r )
229 76 228 jaod 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) | 0s  ( A x.s r )
230 73 229 sylbid 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( r e. ( L ` suc j ) -> ( A x.s r )
231 230 ralrimiv 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. r e. ( L ` suc j ) ( A x.s r )
232 1 2 3 precsexlem5 
 |-  ( j e. _om -> ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
233 232 3ad2ant2 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
234 233 eleq2d 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s e. ( R ` suc j ) <-> s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
235 elun 
 |-  ( s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( s e. ( R ` j ) \/ s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
236 elun 
 |-  ( s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
237 vex 
 |-  s e. _V
238 eqeq1 
 |-  ( a = s -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) )
239 238 2rexbidv 
 |-  ( a = s -> ( E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
240 237 239 elab 
 |-  ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  E. xL e. { x e. ( _Left ` A ) | 0s
241 eqeq1 
 |-  ( a = s -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
242 241 2rexbidv 
 |-  ( a = s -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
243 237 242 elab 
 |-  ( s e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) )
244 240 243 orbi12i 
 |-  ( ( s e. { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( E. xL e. { x e. ( _Left ` A ) | 0s
245 236 244 bitri 
 |-  ( s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( E. xL e. { x e. ( _Left ` A ) | 0s
246 245 orbi2i 
 |-  ( ( s e. ( R ` j ) \/ s e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s
247 235 246 bitri 
 |-  ( s e. ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s  ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s
248 234 247 bitrdi 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s e. ( R ` suc j ) <-> ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s
249 28 rspccv 
 |-  ( A. c e. ( R ` j ) 1s  ( s e. ( R ` j ) -> 1s
250 185 249 syl 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s e. ( R ` j ) -> 1s
251 119 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL )
252 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
253 90 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yL e. No )
254 252 253 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yL ) e. No )
255 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
256 182 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A -s xL ) e. No )
257 195 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
258 254 255 256 257 sltmul2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s yL )  ( ( A -s xL ) x.s ( A x.s yL ) )
259 251 258 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s ( A x.s yL ) )
260 256 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s 1s ) = ( A -s xL ) )
261 259 260 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A -s xL ) x.s ( A x.s yL ) )
262 155 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A ) e. No )
263 262 254 mulnegs1d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) )
264 200 oveq1d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) )
265 264 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) )
266 263 265 eqtr3d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) )
267 200 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( xL -s A ) ) = ( A -s xL ) )
268 261 266 267 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )
269 262 254 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s ( A x.s yL ) ) e. No )
270 262 269 sltnegd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A )  ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )
271 268 270 mpbird 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xL -s A )
272 153 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL e. No )
273 272 252 269 sltsubadd2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A )  xL
274 271 273 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL
275 272 mulslidd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xL ) = xL )
276 262 253 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xL -s A ) x.s yL ) e. No )
277 252 255 276 addsdid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) )
278 252 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
279 252 262 253 muls12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( ( xL -s A ) x.s yL ) ) = ( ( xL -s A ) x.s ( A x.s yL ) ) )
280 278 279 oveq12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) )
281 277 280 eqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) )
282 274 275 281 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xL )
283 255 276 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xL -s A ) x.s yL ) ) e. No )
284 252 283 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) e. No )
285 167 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
286 179 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xL x.s y ) = 1s )
287 255 284 272 285 286 sltmuldivwd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( 1s x.s xL )  1s
288 282 287 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
289 168 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xL =/= 0s )
290 252 283 272 289 286 divsasswd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) )
291 288 290 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
292 oveq2 
 |-  ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) )
293 292 breq2d 
 |-  ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( 1s  1s
294 291 293 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> 1s
295 294 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( E. xL e. { x e. ( _Left ` A ) | 0s  1s
296 85 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A ) e. No )
297 296 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s 1s ) = ( xR -s A ) )
298 189 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
299 79 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s e. No )
300 77 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A e. No )
301 159 adantrl 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  yR e. No )
302 300 301 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s yR ) e. No )
303 123 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
304 299 302 296 303 sltmul2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s  ( ( xR -s A ) x.s 1s )
305 298 304 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s 1s )
306 297 305 eqbrtrrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( xR -s A )
307 83 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR e. No )
308 296 302 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s ( A x.s yR ) ) e. No )
309 307 300 308 sltsubadd2d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A )  xR
310 306 309 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR
311 307 mulslidd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xR ) = xR )
312 296 301 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( xR -s A ) x.s yR ) e. No )
313 300 299 312 addsdid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) )
314 300 mulsridd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s 1s ) = A )
315 300 296 301 muls12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( ( xR -s A ) x.s yR ) ) = ( ( xR -s A ) x.s ( A x.s yR ) ) )
316 314 315 oveq12d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) )
317 313 316 eqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) )
318 310 311 317 3brtr4d 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s x.s xR )
319 299 312 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( 1s +s ( ( xR -s A ) x.s yR ) ) e. No )
320 300 319 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) e. No )
321 100 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  0s
322 113 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  E. y e. No ( xR x.s y ) = 1s )
323 299 320 307 321 322 sltmuldivwd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( 1s x.s xR )  1s
324 318 323 mpbid 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
325 101 adantrr 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  xR =/= 0s )
326 300 319 307 325 322 divsasswd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
327 324 326 breqtrd 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  1s
328 oveq2 
 |-  ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) )
329 328 breq2d 
 |-  ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( 1s  1s
330 327 329 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s
331 330 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s
332 295 331 jaod 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( E. xL e. { x e. ( _Left ` A ) | 0s  1s
333 250 332 jaod 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) | 0s  1s
334 248 333 sylbid 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( s e. ( R ` suc j ) -> 1s
335 334 ralrimiv 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  A. s e. ( R ` suc j ) 1s
336 231 335 jca 
 |-  ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
337 336 3exp 
 |-  ( ph -> ( j e. _om -> ( ( A. b e. ( L ` j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
338 337 com12 
 |-  ( j e. _om -> ( ph -> ( ( A. b e. ( L ` j ) ( A x.s b )  ( A. r e. ( L ` suc j ) ( A x.s r )
339 338 a2d 
 |-  ( j e. _om -> ( ( ph -> ( A. b e. ( L ` j ) ( A x.s b )  ( ph -> ( A. r e. ( L ` suc j ) ( A x.s r )
340 12 18 32 38 56 339 finds 
 |-  ( I e. _om -> ( ph -> ( A. b e. ( L ` I ) ( A x.s b )
341 340 impcom 
 |-  ( ( ph /\ I e. _om ) -> ( A. b e. ( L ` I ) ( A x.s b )