Metamath Proof Explorer

Theorem submarchi

Description: A submonoid is archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018)

Ref Expression
Assertion submarchi 
|- ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> ( W |`s A ) e. Archi )

Proof

Step Hyp Ref Expression
1 submrcl 
 |-  ( A e. ( SubMnd ` W ) -> W e. Mnd )
2 eqid 
 |-  ( Base ` W ) = ( Base ` W )
3 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
4 eqid 
 |-  ( .g ` W ) = ( .g ` W )
5 eqid 
 |-  ( le ` W ) = ( le ` W )
6 eqid 
 |-  ( lt ` W ) = ( lt ` W )
7 2 3 4 5 6 isarchi2 
 |-  ( ( W e. Toset /\ W e. Mnd ) -> ( W e. Archi <-> A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
8 1 7 sylan2 
 |-  ( ( W e. Toset /\ A e. ( SubMnd ` W ) ) -> ( W e. Archi <-> A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
9 8 biimpa 
 |-  ( ( ( W e. Toset /\ A e. ( SubMnd ` W ) ) /\ W e. Archi ) -> A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) )
10 9 an32s 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) )
11 eqid 
 |-  ( W |`s A ) = ( W |`s A )
12 11 submbas 
 |-  ( A e. ( SubMnd ` W ) -> A = ( Base ` ( W |`s A ) ) )
13 2 submss 
 |-  ( A e. ( SubMnd ` W ) -> A C_ ( Base ` W ) )
14 12 13 eqsstrrd 
 |-  ( A e. ( SubMnd ` W ) -> ( Base ` ( W |`s A ) ) C_ ( Base ` W ) )
15 ssralv 
 |-  ( ( Base ` ( W |`s A ) ) C_ ( Base ` W ) -> ( A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
16 15 ralimdv 
 |-  ( ( Base ` ( W |`s A ) ) C_ ( Base ` W ) -> ( A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. x e. ( Base ` W ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
17 ssralv 
 |-  ( ( Base ` ( W |`s A ) ) C_ ( Base ` W ) -> ( A. x e. ( Base ` W ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
18 16 17 syld 
 |-  ( ( Base ` ( W |`s A ) ) C_ ( Base ` W ) -> ( A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
19 14 18 syl 
 |-  ( A e. ( SubMnd ` W ) -> ( A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
20 19 adantl 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> ( A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) ) )
21 11 3 subm0 
 |-  ( A e. ( SubMnd ` W ) -> ( 0g ` W ) = ( 0g ` ( W |`s A ) ) )
22 21 ad2antrr 
 |-  ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) -> ( 0g ` W ) = ( 0g ` ( W |`s A ) ) )
23 11 5 ressle 
 |-  ( A e. ( SubMnd ` W ) -> ( le ` W ) = ( le ` ( W |`s A ) ) )
24 23 difeq1d 
 |-  ( A e. ( SubMnd ` W ) -> ( ( le ` W ) \ _I ) = ( ( le ` ( W |`s A ) ) \ _I ) )
25 5 6 pltfval 
 |-  ( W e. Mnd -> ( lt ` W ) = ( ( le ` W ) \ _I ) )
26 1 25 syl 
 |-  ( A e. ( SubMnd ` W ) -> ( lt ` W ) = ( ( le ` W ) \ _I ) )
27 11 submmnd 
 |-  ( A e. ( SubMnd ` W ) -> ( W |`s A ) e. Mnd )
28 eqid 
 |-  ( le ` ( W |`s A ) ) = ( le ` ( W |`s A ) )
29 eqid 
 |-  ( lt ` ( W |`s A ) ) = ( lt ` ( W |`s A ) )
30 28 29 pltfval 
 |-  ( ( W |`s A ) e. Mnd -> ( lt ` ( W |`s A ) ) = ( ( le ` ( W |`s A ) ) \ _I ) )
31 27 30 syl 
 |-  ( A e. ( SubMnd ` W ) -> ( lt ` ( W |`s A ) ) = ( ( le ` ( W |`s A ) ) \ _I ) )
32 24 26 31 3eqtr4d 
 |-  ( A e. ( SubMnd ` W ) -> ( lt ` W ) = ( lt ` ( W |`s A ) ) )
33 32 ad2antrr 
 |-  ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) -> ( lt ` W ) = ( lt ` ( W |`s A ) ) )
34 eqidd 
 |-  ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) -> x = x )
35 22 33 34 breq123d 
 |-  ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) -> ( ( 0g ` W ) ( lt ` W ) x <-> ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x ) )
36 eqidd 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> y = y )
37 23 ad3antrrr 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> ( le ` W ) = ( le ` ( W |`s A ) ) )
38 simplll 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> A e. ( SubMnd ` W ) )
39 simpr 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> n e. NN )
40 39 nnnn0d 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> n e. NN0 )
41 simpllr 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> x e. ( Base ` ( W |`s A ) ) )
42 38 12 syl 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> A = ( Base ` ( W |`s A ) ) )
43 41 42 eleqtrrd 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> x e. A )
44 eqid 
 |-  ( .g ` ( W |`s A ) ) = ( .g ` ( W |`s A ) )
45 4 11 44 submmulg 
 |-  ( ( A e. ( SubMnd ` W ) /\ n e. NN0 /\ x e. A ) -> ( n ( .g ` W ) x ) = ( n ( .g ` ( W |`s A ) ) x ) )
46 38 40 43 45 syl3anc 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> ( n ( .g ` W ) x ) = ( n ( .g ` ( W |`s A ) ) x ) )
47 36 37 46 breq123d 
 |-  ( ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) /\ n e. NN ) -> ( y ( le ` W ) ( n ( .g ` W ) x ) <-> y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) )
48 47 rexbidva 
 |-  ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) -> ( E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) <-> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) )
49 35 48 imbi12d 
 |-  ( ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) /\ y e. ( Base ` ( W |`s A ) ) ) -> ( ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) <-> ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
50 49 ralbidva 
 |-  ( ( A e. ( SubMnd ` W ) /\ x e. ( Base ` ( W |`s A ) ) ) -> ( A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) <-> A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
51 50 ralbidva 
 |-  ( A e. ( SubMnd ` W ) -> ( A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) <-> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
52 51 adantl 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> ( A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) <-> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
53 20 52 sylibd 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> ( A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( 0g ` W ) ( lt ` W ) x -> E. n e. NN y ( le ` W ) ( n ( .g ` W ) x ) ) -> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
54 10 53 mpd 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) )
55 resstos 
 |-  ( ( W e. Toset /\ A e. ( SubMnd ` W ) ) -> ( W |`s A ) e. Toset )
56 27 adantl 
 |-  ( ( W e. Toset /\ A e. ( SubMnd ` W ) ) -> ( W |`s A ) e. Mnd )
57 eqid 
 |-  ( Base ` ( W |`s A ) ) = ( Base ` ( W |`s A ) )
58 eqid 
 |-  ( 0g ` ( W |`s A ) ) = ( 0g ` ( W |`s A ) )
59 57 58 44 28 29 isarchi2 
 |-  ( ( ( W |`s A ) e. Toset /\ ( W |`s A ) e. Mnd ) -> ( ( W |`s A ) e. Archi <-> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
60 55 56 59 syl2anc 
 |-  ( ( W e. Toset /\ A e. ( SubMnd ` W ) ) -> ( ( W |`s A ) e. Archi <-> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
61 60 adantlr 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> ( ( W |`s A ) e. Archi <-> A. x e. ( Base ` ( W |`s A ) ) A. y e. ( Base ` ( W |`s A ) ) ( ( 0g ` ( W |`s A ) ) ( lt ` ( W |`s A ) ) x -> E. n e. NN y ( le ` ( W |`s A ) ) ( n ( .g ` ( W |`s A ) ) x ) ) ) )
62 54 61 mpbird 
 |-  ( ( ( W e. Toset /\ W e. Archi ) /\ A e. ( SubMnd ` W ) ) -> ( W |`s A ) e. Archi )