Metamath Proof Explorer

Theorem archiabllem1b

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 13-Apr-2018)

Ref Expression
Hypotheses archiabllem.b 
|- B = ( Base ` W )
archiabllem.0 
|- .0. = ( 0g ` W )
archiabllem.e 
|- .<_ = ( le ` W )
archiabllem.t 
|- .< = ( lt ` W )
archiabllem.m 
|- .x. = ( .g ` W )
archiabllem.g 
|- ( ph -> W e. oGrp )
archiabllem.a 
|- ( ph -> W e. Archi )
archiabllem1.u 
|- ( ph -> U e. B )
archiabllem1.p 
|- ( ph -> .0. .< U )
archiabllem1.s 
|- ( ( ph /\ x e. B /\ .0. .< x ) -> U .<_ x )
Assertion archiabllem1b 
|- ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. U ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b 
 |-  B = ( Base ` W )
2 archiabllem.0 
 |-  .0. = ( 0g ` W )
3 archiabllem.e 
 |-  .<_ = ( le ` W )
4 archiabllem.t 
 |-  .< = ( lt ` W )
5 archiabllem.m 
 |-  .x. = ( .g ` W )
6 archiabllem.g 
 |-  ( ph -> W e. oGrp )
7 archiabllem.a 
 |-  ( ph -> W e. Archi )
8 archiabllem1.u 
 |-  ( ph -> U e. B )
9 archiabllem1.p 
 |-  ( ph -> .0. .< U )
10 archiabllem1.s 
 |-  ( ( ph /\ x e. B /\ .0. .< x ) -> U .<_ x )
11 0zd 
 |-  ( ( ( ph /\ y e. B ) /\ y = .0. ) -> 0 e. ZZ )
12 simpr 
 |-  ( ( ( ph /\ y e. B ) /\ y = .0. ) -> y = .0. )
13 1 2 5 mulg0 
 |-  ( U e. B -> ( 0 .x. U ) = .0. )
14 8 13 syl 
 |-  ( ph -> ( 0 .x. U ) = .0. )
15 14 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ y = .0. ) -> ( 0 .x. U ) = .0. )
16 12 15 eqtr4d 
 |-  ( ( ( ph /\ y e. B ) /\ y = .0. ) -> y = ( 0 .x. U ) )
17 oveq1 
 |-  ( n = 0 -> ( n .x. U ) = ( 0 .x. U ) )
18 17 rspceeqv 
 |-  ( ( 0 e. ZZ /\ y = ( 0 .x. U ) ) -> E. n e. ZZ y = ( n .x. U ) )
19 11 16 18 syl2anc 
 |-  ( ( ( ph /\ y e. B ) /\ y = .0. ) -> E. n e. ZZ y = ( n .x. U ) )
20 simplr 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> m e. NN )
21 20 nnzd 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> m e. ZZ )
22 21 znegcld 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> -u m e. ZZ )
23 8 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> U e. B )
24 23 ad2antrr 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> U e. B )
25 eqid 
 |-  ( invg ` W ) = ( invg ` W )
26 1 5 25 mulgnegnn 
 |-  ( ( m e. NN /\ U e. B ) -> ( -u m .x. U ) = ( ( invg ` W ) ` ( m .x. U ) ) )
27 20 24 26 syl2anc 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> ( -u m .x. U ) = ( ( invg ` W ) ` ( m .x. U ) ) )
28 simpr 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> ( ( invg ` W ) ` y ) = ( m .x. U ) )
29 28 fveq2d 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` y ) ) = ( ( invg ` W ) ` ( m .x. U ) ) )
30 6 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> W e. oGrp )
31 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
32 30 31 syl 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> W e. Grp )
33 simp2 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> y e. B )
34 1 25 grpinvinv 
 |-  ( ( W e. Grp /\ y e. B ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` y ) ) = y )
35 32 33 34 syl2anc 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` y ) ) = y )
36 35 ad2antrr 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> ( ( invg ` W ) ` ( ( invg ` W ) ` y ) ) = y )
37 27 29 36 3eqtr2rd 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> y = ( -u m .x. U ) )
38 oveq1 
 |-  ( n = -u m -> ( n .x. U ) = ( -u m .x. U ) )
39 38 rspceeqv 
 |-  ( ( -u m e. ZZ /\ y = ( -u m .x. U ) ) -> E. n e. ZZ y = ( n .x. U ) )
40 22 37 39 syl2anc 
 |-  ( ( ( ( ph /\ y e. B /\ y .< .0. ) /\ m e. NN ) /\ ( ( invg ` W ) ` y ) = ( m .x. U ) ) -> E. n e. ZZ y = ( n .x. U ) )
41 7 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> W e. Archi )
42 9 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> .0. .< U )
43 simp1 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> ph )
44 43 10 syl3an1 
 |-  ( ( ( ph /\ y e. B /\ y .< .0. ) /\ x e. B /\ .0. .< x ) -> U .<_ x )
45 1 25 grpinvcl 
 |-  ( ( W e. Grp /\ y e. B ) -> ( ( invg ` W ) ` y ) e. B )
46 32 33 45 syl2anc 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> ( ( invg ` W ) ` y ) e. B )
47 1 2 grpidcl 
 |-  ( W e. Grp -> .0. e. B )
48 32 47 syl 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> .0. e. B )
49 simp3 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> y .< .0. )
50 eqid 
 |-  ( +g ` W ) = ( +g ` W )
51 1 4 50 ogrpaddlt 
 |-  ( ( W e. oGrp /\ ( y e. B /\ .0. e. B /\ ( ( invg ` W ) ` y ) e. B ) /\ y .< .0. ) -> ( y ( +g ` W ) ( ( invg ` W ) ` y ) ) .< ( .0. ( +g ` W ) ( ( invg ` W ) ` y ) ) )
52 30 33 48 46 49 51 syl131anc 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> ( y ( +g ` W ) ( ( invg ` W ) ` y ) ) .< ( .0. ( +g ` W ) ( ( invg ` W ) ` y ) ) )
53 1 50 2 25 grprinv 
 |-  ( ( W e. Grp /\ y e. B ) -> ( y ( +g ` W ) ( ( invg ` W ) ` y ) ) = .0. )
54 32 33 53 syl2anc 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> ( y ( +g ` W ) ( ( invg ` W ) ` y ) ) = .0. )
55 1 50 2 grplid 
 |-  ( ( W e. Grp /\ ( ( invg ` W ) ` y ) e. B ) -> ( .0. ( +g ` W ) ( ( invg ` W ) ` y ) ) = ( ( invg ` W ) ` y ) )
56 32 46 55 syl2anc 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> ( .0. ( +g ` W ) ( ( invg ` W ) ` y ) ) = ( ( invg ` W ) ` y ) )
57 52 54 56 3brtr3d 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> .0. .< ( ( invg ` W ) ` y ) )
58 1 2 3 4 5 30 41 23 42 44 46 57 archiabllem1a 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> E. m e. NN ( ( invg ` W ) ` y ) = ( m .x. U ) )
59 40 58 r19.29a 
 |-  ( ( ph /\ y e. B /\ y .< .0. ) -> E. n e. ZZ y = ( n .x. U ) )
60 59 3expa 
 |-  ( ( ( ph /\ y e. B ) /\ y .< .0. ) -> E. n e. ZZ y = ( n .x. U ) )
61 nnssz 
 |-  NN C_ ZZ
62 6 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> W e. oGrp )
63 7 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> W e. Archi )
64 8 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> U e. B )
65 9 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> .0. .< U )
66 simp1 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> ph )
67 66 10 syl3an1 
 |-  ( ( ( ph /\ y e. B /\ .0. .< y ) /\ x e. B /\ .0. .< x ) -> U .<_ x )
68 simp2 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> y e. B )
69 simp3 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> .0. .< y )
70 1 2 3 4 5 62 63 64 65 67 68 69 archiabllem1a 
 |-  ( ( ph /\ y e. B /\ .0. .< y ) -> E. n e. NN y = ( n .x. U ) )
71 70 3expa 
 |-  ( ( ( ph /\ y e. B ) /\ .0. .< y ) -> E. n e. NN y = ( n .x. U ) )
72 ssrexv 
 |-  ( NN C_ ZZ -> ( E. n e. NN y = ( n .x. U ) -> E. n e. ZZ y = ( n .x. U ) ) )
73 61 71 72 mpsyl 
 |-  ( ( ( ph /\ y e. B ) /\ .0. .< y ) -> E. n e. ZZ y = ( n .x. U ) )
74 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
75 74 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
76 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
77 6 75 76 3syl 
 |-  ( ph -> W e. Toset )
78 77 adantr 
 |-  ( ( ph /\ y e. B ) -> W e. Toset )
79 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
80 6 31 47 3syl 
 |-  ( ph -> .0. e. B )
81 80 adantr 
 |-  ( ( ph /\ y e. B ) -> .0. e. B )
82 1 4 tlt3 
 |-  ( ( W e. Toset /\ y e. B /\ .0. e. B ) -> ( y = .0. \/ y .< .0. \/ .0. .< y ) )
83 78 79 81 82 syl3anc 
 |-  ( ( ph /\ y e. B ) -> ( y = .0. \/ y .< .0. \/ .0. .< y ) )
84 19 60 73 83 mpjao3dan 
 |-  ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. U ) )