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 simpr 
 |-  ( ( W e. oField /\ A. x e. B E. n e. NN x .< ( H ` n ) ) -> A. x e. B E. n e. NN x .< ( H ` n ) )
65 breq1 
 |-  ( x = z -> ( x .< ( H ` n ) <-> z .< ( H ` n ) ) )
66 65 rexbidv 
 |-  ( x = z -> ( E. n e. NN x .< ( H ` n ) <-> E. n e. NN z .< ( H ` n ) ) )
67 66 cbvralvw 
 |-  ( A. x e. B E. n e. NN x .< ( H ` n ) <-> A. z e. B E. n e. NN z .< ( H ` n ) )
68 64 67 sylib 
 |-  ( ( 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 ) )
69 68 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 ) )
70 breq1 
 |-  ( z = ( x ( /r ` W ) y ) -> ( z .< ( H ` n ) <-> ( x ( /r ` W ) y ) .< ( H ` n ) ) )
71 70 rexbidv 
 |-  ( z = ( x ( /r ` W ) y ) -> ( E. n e. NN z .< ( H ` n ) <-> E. n e. NN ( x ( /r ` W ) y ) .< ( H ` n ) ) )
72 71 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 ) ) )
73 63 69 72 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 ) )
74 eqid 
 |-  ( .r ` W ) = ( .r ` W )
75 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 )
76 75 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 )
77 75 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 )
78 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 ) )
79 78 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 )
80 78 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 )
81 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 )
82 77 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 )
83 75 82 80 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 ) )
84 81 83 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 )
85 84 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 ) )
86 75 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 ) ) ) )
87 80 85 86 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 ) )
88 77 79 87 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 )
89 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 )
90 75 89 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 ) ) )
91 77 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 )
92 89 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 )
93 77 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 )
94 1 8 mulgcl 
 |-  ( ( W e. Grp /\ n e. ZZ /\ ( 1r ` W ) e. B ) -> ( n ( .g ` W ) ( 1r ` W ) ) e. B )
95 91 92 93 94 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 )
96 90 95 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 )
97 75 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 )
98 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 ) )
99 1 74 7 76 88 96 80 3 97 98 81 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 ) )
100 1 57 61 74 dvrcan1 
 |-  ( ( W e. Ring /\ x e. B /\ y e. ( Unit ` W ) ) -> ( ( x ( /r ` W ) y ) ( .r ` W ) y ) = x )
101 77 79 87 100 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 )
102 90 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 ) )
103 1 8 74 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 ) ) )
104 77 92 93 80 103 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 ) ) )
105 1 74 12 ringlidm 
 |-  ( ( W e. Ring /\ y e. B ) -> ( ( 1r ` W ) ( .r ` W ) y ) = y )
106 77 80 105 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 )
107 106 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 ) )
108 102 104 107 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 ) )
109 99 101 108 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 ) )
110 109 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 ) ) )
111 110 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 ) ) )
112 111 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 ) ) )
113 73 112 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 ) )
114 113 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 ) ) )
115 114 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 ) ) ) )
116 40 115 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 ) ) )
117 116 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 ) ) )
118 117 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 ) ) ) )
119 35 118 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 ) ) )
120 10 119 bitrd 
 |-  ( W e. oField -> ( W e. Archi <-> A. x e. B E. n e. NN x .< ( H ` n ) ) )