Metamath Proof Explorer

Theorem isarchiofld

Description: Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018)

Ref Expression
Hypotheses isarchiofld.b 
|- B = ( Base ` W )
isarchiofld.h 
|- H = ( ZRHom ` W )
isarchiofld.l 
|- .< = ( lt ` W )
Assertion isarchiofld 
|- ( W e. oField -> ( W e. Archi <-> A. x e. B E. n e. NN x .< ( H ` n ) ) )

Proof

Step Hyp Ref Expression
1 isarchiofld.b 
 |-  B = ( Base ` W )
2 isarchiofld.h 
 |-  H = ( ZRHom ` W )
3 isarchiofld.l 
 |-  .< = ( lt ` W )
4 isofld 
 |-  ( W e. oField <-> ( W e. Field /\ W e. oRing ) )
5 4 simprbi 
 |-  ( W e. oField -> W e. oRing )
6 orngogrp 
 |-  ( W e. oRing -> W e. oGrp )
7 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
8 eqid 
 |-  ( .g ` W ) = ( .g ` W )
9 1 7 3 8 isarchi3 
 |-  ( W e. oGrp -> ( W e. Archi <-> A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) ) )
10 5 6 9 3syl 
 |-  ( W e. oField -> ( W e. Archi <-> A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) ) )
11 orngring 
 |-  ( W e. oRing -> W e. Ring )
12 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
13 1 12 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. B )
14 5 11 13 3syl 
 |-  ( W e. oField -> ( 1r ` W ) e. B )
15 breq2 
 |-  ( y = ( 1r ` W ) -> ( ( 0g ` W ) .< y <-> ( 0g ` W ) .< ( 1r ` W ) ) )
16 oveq2 
 |-  ( y = ( 1r ` W ) -> ( n ( .g ` W ) y ) = ( n ( .g ` W ) ( 1r ` W ) ) )
17 16 breq2d 
 |-  ( y = ( 1r ` W ) -> ( x .< ( n ( .g ` W ) y ) <-> x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
18 17 rexbidv 
 |-  ( y = ( 1r ` W ) -> ( E. n e. NN x .< ( n ( .g ` W ) y ) <-> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
19 15 18 imbi12d 
 |-  ( y = ( 1r ` W ) -> ( ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) <-> ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) ) )
20 19 ralbidv 
 |-  ( y = ( 1r ` W ) -> ( A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) <-> A. x e. B ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) ) )
21 20 rspcv 
 |-  ( ( 1r ` W ) e. B -> ( A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) -> A. x e. B ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) ) )
22 14 21 syl 
 |-  ( W e. oField -> ( A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) -> A. x e. B ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) ) )
23 7 12 3 ofldlt1 
 |-  ( W e. oField -> ( 0g ` W ) .< ( 1r ` W ) )
24 pm5.5 
 |-  ( ( 0g ` W ) .< ( 1r ` W ) -> ( ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) <-> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
25 23 24 syl 
 |-  ( W e. oField -> ( ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) <-> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
26 25 ralbidv 
 |-  ( W e. oField -> ( A. x e. B ( ( 0g ` W ) .< ( 1r ` W ) -> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) <-> A. x e. B E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
27 22 26 sylibd 
 |-  ( W e. oField -> ( A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) -> A. x e. B E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
28 5 11 syl 
 |-  ( W e. oField -> W e. Ring )
29 nnz 
 |-  ( n e. NN -> n e. ZZ )
30 2 8 12 zrhmulg 
 |-  ( ( W e. Ring /\ n e. ZZ ) -> ( H ` n ) = ( n ( .g ` W ) ( 1r ` W ) ) )
31 28 29 30 syl2an 
 |-  ( ( W e. oField /\ n e. NN ) -> ( H ` n ) = ( n ( .g ` W ) ( 1r ` W ) ) )
32 31 breq2d 
 |-  ( ( W e. oField /\ n e. NN ) -> ( x .< ( H ` n ) <-> x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
33 32 rexbidva 
 |-  ( W e. oField -> ( E. n e. NN x .< ( H ` n ) <-> E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
34 33 ralbidv 
 |-  ( W e. oField -> ( A. x e. B E. n e. NN x .< ( H ` n ) <-> A. x e. B E. n e. NN x .< ( n ( .g ` W ) ( 1r ` W ) ) ) )
35 27 34 sylibrd 
 |-  ( W e. oField -> ( A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) -> A. x e. B E. n e. NN x .< ( H ` n ) ) )
36 nfv 
 |-  F/ x W e. oField
37 nfra1 
 |-  F/ x A. x e. B E. n e. NN x .< ( H ` n )
38 36 37 nfan 
 |-  F/ x ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) )
39 nfv 
 |-  F/ x y e. B
40 38 39 nfan 
 |-  F/ x ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ y e. B )
41 28 ad3antrrr 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> W e. Ring )
42 simplrr 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> x e. B )
43 simplrl 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> y e. B )
44 simpr 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( 0g ` W ) .< y )
45 simplll 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> W e. oField )
46 ringgrp 
 |-  ( W e. Ring -> W e. Grp )
47 1 7 grpidcl 
 |-  ( W e. Grp -> ( 0g ` W ) e. B )
48 41 46 47 3syl 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( 0g ` W ) e. B )
49 3 pltne 
 |-  ( ( W e. oField /\ ( 0g ` W ) e. B /\ y e. B ) -> ( ( 0g ` W ) .< y -> ( 0g ` W ) =/= y ) )
50 45 48 43 49 syl3anc 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( ( 0g ` W ) .< y -> ( 0g ` W ) =/= y ) )
51 44 50 mpd 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( 0g ` W ) =/= y )
52 51 necomd 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> y =/= ( 0g ` W ) )
53 4 simplbi 
 |-  ( W e. oField -> W e. Field )
54 isfld 
 |-  ( W e. Field <-> ( W e. DivRing /\ W e. CRing ) )
55 54 simplbi 
 |-  ( W e. Field -> W e. DivRing )
56 53 55 syl 
 |-  ( W e. oField -> W e. DivRing )
57 eqid 
 |-  ( Unit ` W ) = ( Unit ` W )
58 1 57 7 drngunit 
 |-  ( W e. DivRing -> ( y e. ( Unit ` W ) <-> ( y e. B /\ y =/= ( 0g ` W ) ) ) )
59 45 56 58 3syl 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( y e. ( Unit ` W ) <-> ( y e. B /\ y =/= ( 0g ` W ) ) ) )
60 43 52 59 mpbir2and 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> y e. ( Unit ` W ) )
61 eqid 
 |-  ( /r ` W ) = ( /r ` W )
62 1 57 61 dvrcl 
 |-  ( ( W e. Ring /\ x e. B /\ y e. ( Unit ` W ) ) -> ( x ( /r ` W ) y ) e. B )
63 41 42 60 62 syl3anc 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( x ( /r ` W ) y ) e. B )
64 breq1 
 |-  ( x = z -> ( x .< ( H ` n ) <-> z .< ( H ` n ) ) )
65 64 rexbidv 
 |-  ( x = z -> ( E. n e. NN x .< ( H ` n ) <-> E. n e. NN z .< ( H ` n ) ) )
66 65 cbvralvw 
 |-  ( A. x e. B E. n e. NN x .< ( H ` n ) <-> A. z e. B E. n e. NN z .< ( H ` n ) )
67 66 bilani 
 |-  ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) -> A. z e. B E. n e. NN z .< ( H ` n ) )
68 67 ad2antrr 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> A. z e. B E. n e. NN z .< ( H ` n ) )
69 breq1 
 |-  ( z = ( x ( /r ` W ) y ) -> ( z .< ( H ` n ) <-> ( x ( /r ` W ) y ) .< ( H ` n ) ) )
70 69 rexbidv 
 |-  ( z = ( x ( /r ` W ) y ) -> ( E. n e. NN z .< ( H ` n ) <-> E. n e. NN ( x ( /r ` W ) y ) .< ( H ` n ) ) )
71 70 rspcv 
 |-  ( ( x ( /r ` W ) y ) e. B -> ( A. z e. B E. n e. NN z .< ( H ` n ) -> E. n e. NN ( x ( /r ` W ) y ) .< ( H ` n ) ) )
72 63 68 71 sylc 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> E. n e. NN ( x ( /r ` W ) y ) .< ( H ` n ) )
73 eqid 
 |-  ( .r ` W ) = ( .r ` W )
74 simp-4l 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> W e. oField )
75 74 5 syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> W e. oRing )
76 74 28 syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> W e. Ring )
77 simp-4r 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( y e. B /\ x e. B ) )
78 77 simprd 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> x e. B )
79 77 simpld 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> y e. B )
80 simpllr 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( 0g ` W ) .< y )
81 76 46 47 3syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( 0g ` W ) e. B )
82 74 81 79 49 syl3anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( 0g ` W ) .< y -> ( 0g ` W ) =/= y ) )
83 80 82 mpd 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( 0g ` W ) =/= y )
84 83 necomd 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> y =/= ( 0g ` W ) )
85 74 56 58 3syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( y e. ( Unit ` W ) <-> ( y e. B /\ y =/= ( 0g ` W ) ) ) )
86 79 84 85 mpbir2and 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> y e. ( Unit ` W ) )
87 76 78 86 62 syl3anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( x ( /r ` W ) y ) e. B )
88 simplr 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> n e. NN )
89 74 88 31 syl2anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( H ` n ) = ( n ( .g ` W ) ( 1r ` W ) ) )
90 76 46 syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> W e. Grp )
91 88 29 syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> n e. ZZ )
92 76 13 syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( 1r ` W ) e. B )
93 1 8 mulgcl 
 |-  ( ( W e. Grp /\ n e. ZZ /\ ( 1r ` W ) e. B ) -> ( n ( .g ` W ) ( 1r ` W ) ) e. B )
94 90 91 92 93 syl3anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( n ( .g ` W ) ( 1r ` W ) ) e. B )
95 89 94 eqeltrd 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( H ` n ) e. B )
96 74 56 syl 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> W e. DivRing )
97 simpr 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( x ( /r ` W ) y ) .< ( H ` n ) )
98 1 73 7 75 87 95 79 3 96 97 80 orngrmullt 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( x ( /r ` W ) y ) ( .r ` W ) y ) .< ( ( H ` n ) ( .r ` W ) y ) )
99 1 57 61 73 dvrcan1 
 |-  ( ( W e. Ring /\ x e. B /\ y e. ( Unit ` W ) ) -> ( ( x ( /r ` W ) y ) ( .r ` W ) y ) = x )
100 76 78 86 99 syl3anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( x ( /r ` W ) y ) ( .r ` W ) y ) = x )
101 89 oveq1d 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( H ` n ) ( .r ` W ) y ) = ( ( n ( .g ` W ) ( 1r ` W ) ) ( .r ` W ) y ) )
102 1 8 73 mulgass2 
 |-  ( ( W e. Ring /\ ( n e. ZZ /\ ( 1r ` W ) e. B /\ y e. B ) ) -> ( ( n ( .g ` W ) ( 1r ` W ) ) ( .r ` W ) y ) = ( n ( .g ` W ) ( ( 1r ` W ) ( .r ` W ) y ) ) )
103 76 91 92 79 102 syl13anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( n ( .g ` W ) ( 1r ` W ) ) ( .r ` W ) y ) = ( n ( .g ` W ) ( ( 1r ` W ) ( .r ` W ) y ) ) )
104 1 73 12 ringlidm 
 |-  ( ( W e. Ring /\ y e. B ) -> ( ( 1r ` W ) ( .r ` W ) y ) = y )
105 76 79 104 syl2anc 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( 1r ` W ) ( .r ` W ) y ) = y )
106 105 oveq2d 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( n ( .g ` W ) ( ( 1r ` W ) ( .r ` W ) y ) ) = ( n ( .g ` W ) y ) )
107 101 103 106 3eqtrd 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> ( ( H ` n ) ( .r ` W ) y ) = ( n ( .g ` W ) y ) )
108 98 100 107 3brtr3d 
 |-  ( ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) /\ ( x ( /r ` W ) y ) .< ( H ` n ) ) -> x .< ( n ( .g ` W ) y ) )
109 108 ex 
 |-  ( ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) /\ n e. NN ) -> ( ( x ( /r ` W ) y ) .< ( H ` n ) -> x .< ( n ( .g ` W ) y ) ) )
110 109 reximdva 
 |-  ( ( ( W e. oField /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( E. n e. NN ( x ( /r ` W ) y ) .< ( H ` n ) -> E. n e. NN x .< ( n ( .g ` W ) y ) ) )
111 110 adantllr 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> ( E. n e. NN ( x ( /r ` W ) y ) .< ( H ` n ) -> E. n e. NN x .< ( n ( .g ` W ) y ) ) )
112 72 111 mpd 
 |-  ( ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) /\ ( 0g ` W ) .< y ) -> E. n e. NN x .< ( n ( .g ` W ) y ) )
113 112 ex 
 |-  ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ ( y e. B /\ x e. B ) ) -> ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) )
114 113 expr 
 |-  ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ y e. B ) -> ( x e. B -> ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) ) )
115 40 114 ralrimi 
 |-  ( ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) /\ y e. B ) -> A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) )
116 115 ralrimiva 
 |-  ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) -> A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) )
117 116 ex 
 |-  ( W e. oField -> ( A. x e. B E. n e. NN x .< ( H ` n ) -> A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) ) )
118 35 117 impbid 
 |-  ( W e. oField -> ( A. y e. B A. x e. B ( ( 0g ` W ) .< y -> E. n e. NN x .< ( n ( .g ` W ) y ) ) <-> A. x e. B E. n e. NN x .< ( H ` n ) ) )
119 10 118 bitrd 
 |-  ( W e. oField -> ( W e. Archi <-> A. x e. B E. n e. NN x .< ( H ` n ) ) )