Metamath Proof Explorer

Theorem submarchi

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

Ref Expression
Assertion submarchi ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→W↾𝑠A∈Archi

Proof

Step Hyp Ref Expression
1 submrcl ⊢A∈SubMnd⁡W→W∈Mnd
2 eqid ⊢BaseW=BaseW
3 eqid ⊢0W=0W
4 eqid ⊢⋅W=⋅W
5 eqid ⊢≤W=≤W
6 eqid ⊢<W=<W
7 2 3 4 5 6 isarchi2 ⊢W∈Toset∧W∈Mnd→W∈Archi↔∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx
8 1 7 sylan2 ⊢W∈Toset∧A∈SubMnd⁡W→W∈Archi↔∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx
9 8 biimpa ⊢W∈Toset∧A∈SubMnd⁡W∧W∈Archi→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx
10 9 an32s ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx
11 eqid ⊢W↾𝑠A=W↾𝑠A
12 11 submbas ⊢A∈SubMnd⁡W→A=BaseW↾𝑠A
13 2 submss ⊢A∈SubMnd⁡W→A⊆BaseW
14 12 13 eqsstrrd ⊢A∈SubMnd⁡W→BaseW↾𝑠A⊆BaseW
15 ssralv ⊢BaseW↾𝑠A⊆BaseW→∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx
16 15 ralimdv ⊢BaseW↾𝑠A⊆BaseW→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀x∈BaseW∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx
17 ssralv ⊢BaseW↾𝑠A⊆BaseW→∀x∈BaseW∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx
18 16 17 syld ⊢BaseW↾𝑠A⊆BaseW→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx
19 14 18 syl ⊢A∈SubMnd⁡W→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx
20 19 adantl ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx
21 11 3 subm0 ⊢A∈SubMnd⁡W→0W=0W↾𝑠A
22 21 ad2antrr ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A→0W=0W↾𝑠A
23 11 5 ressle ⊢A∈SubMnd⁡W→≤W=≤W↾𝑠A
24 23 difeq1d ⊢A∈SubMnd⁡W→≤W∖I=≤W↾𝑠A∖I
25 5 6 pltfval ⊢W∈Mnd→<W=≤W∖I
26 1 25 syl ⊢A∈SubMnd⁡W→<W=≤W∖I
27 11 submmnd ⊢A∈SubMnd⁡W→W↾𝑠A∈Mnd
28 eqid ⊢≤W↾𝑠A=≤W↾𝑠A
29 eqid ⊢<W↾𝑠A=<W↾𝑠A
30 28 29 pltfval ⊢W↾𝑠A∈Mnd→<W↾𝑠A=≤W↾𝑠A∖I
31 27 30 syl ⊢A∈SubMnd⁡W→<W↾𝑠A=≤W↾𝑠A∖I
32 24 26 31 3eqtr4d ⊢A∈SubMnd⁡W→<W=<W↾𝑠A
33 32 ad2antrr ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A→<W=<W↾𝑠A
34 eqidd ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A→x=x
35 22 33 34 breq123d ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A→0W<Wx↔0W↾𝑠A<W↾𝑠Ax
36 eqidd ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→y=y
37 23 ad3antrrr ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→≤W=≤W↾𝑠A
38 simplll ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→A∈SubMnd⁡W
39 simpr ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→n∈ℕ
40 39 nnnn0d ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→n∈ℕ0
41 simpllr ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→x∈BaseW↾𝑠A
42 38 12 syl ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→A=BaseW↾𝑠A
43 41 42 eleqtrrd ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→x∈A
44 eqid ⊢⋅W↾𝑠A=⋅W↾𝑠A
45 4 11 44 submmulg ⊢A∈SubMnd⁡W∧n∈ℕ0∧x∈A→n⋅Wx=n⋅W↾𝑠Ax
46 38 40 43 45 syl3anc ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→n⋅Wx=n⋅W↾𝑠Ax
47 36 37 46 breq123d ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A∧n∈ℕ→y≤Wn⋅Wx↔y≤W↾𝑠An⋅W↾𝑠Ax
48 47 rexbidva ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A→∃n∈ℕy≤Wn⋅Wx↔∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
49 35 48 imbi12d ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A∧y∈BaseW↾𝑠A→0W<Wx→∃n∈ℕy≤Wn⋅Wx↔0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
50 49 ralbidva ⊢A∈SubMnd⁡W∧x∈BaseW↾𝑠A→∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx↔∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
51 50 ralbidva ⊢A∈SubMnd⁡W→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx↔∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
52 51 adantl ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W<Wx→∃n∈ℕy≤Wn⋅Wx↔∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
53 20 52 sylibd ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→∀x∈BaseW∀y∈BaseW0W<Wx→∃n∈ℕy≤Wn⋅Wx→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
54 10 53 mpd ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
55 resstos ⊢W∈Toset∧A∈SubMnd⁡W→W↾𝑠A∈Toset
56 27 adantl ⊢W∈Toset∧A∈SubMnd⁡W→W↾𝑠A∈Mnd
57 eqid ⊢BaseW↾𝑠A=BaseW↾𝑠A
58 eqid ⊢0W↾𝑠A=0W↾𝑠A
59 57 58 44 28 29 isarchi2 ⊢W↾𝑠A∈Toset∧W↾𝑠A∈Mnd→W↾𝑠A∈Archi↔∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
60 55 56 59 syl2anc ⊢W∈Toset∧A∈SubMnd⁡W→W↾𝑠A∈Archi↔∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
61 60 adantlr ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→W↾𝑠A∈Archi↔∀x∈BaseW↾𝑠A∀y∈BaseW↾𝑠A0W↾𝑠A<W↾𝑠Ax→∃n∈ℕy≤W↾𝑠An⋅W↾𝑠Ax
62 54 61 mpbird ⊢W∈Toset∧W∈Archi∧A∈SubMnd⁡W→W↾𝑠A∈Archi