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 ⊢ Base W = Base W
3 eqid ⊢ 0 W = 0 W
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 ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
8 1 7 sylan2 ⊢ W ∈ Toset ∧ A ∈ SubMnd ⁡ W → W ∈ Archi ↔ ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
9 8 biimpa ⊢ W ∈ Toset ∧ A ∈ SubMnd ⁡ W ∧ W ∈ Archi → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
10 9 an32s ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
11 eqid ⊢ W ↾ 𝑠 A = W ↾ 𝑠 A
12 11 submbas ⊢ A ∈ SubMnd ⁡ W → A = Base W ↾ 𝑠 A
13 2 submss ⊢ A ∈ SubMnd ⁡ W → A ⊆ Base W
14 12 13 eqsstrrd ⊢ A ∈ SubMnd ⁡ W → Base W ↾ 𝑠 A ⊆ Base W
15 ssralv ⊢ Base W ↾ 𝑠 A ⊆ Base W → ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
16 15 ralimdv ⊢ Base W ↾ 𝑠 A ⊆ Base W → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ x ∈ Base W ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
17 ssralv ⊢ Base W ↾ 𝑠 A ⊆ Base W → ∀ x ∈ Base W ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
18 16 17 syld ⊢ Base W ↾ 𝑠 A ⊆ Base W → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
19 14 18 syl ⊢ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
20 19 adantl ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x
21 11 3 subm0 ⊢ A ∈ SubMnd ⁡ W → 0 W = 0 W ↾ 𝑠 A
22 21 ad2antrr ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A → 0 W = 0 W ↾ 𝑠 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 ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A → < W = < W ↾ 𝑠 A
34 eqidd ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A → x = x
35 22 33 34 breq123d ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A → 0 W < W x ↔ 0 W ↾ 𝑠 A < W ↾ 𝑠 A x
36 eqidd ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → y = y
37 23 ad3antrrr ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → ≤ W = ≤ W ↾ 𝑠 A
38 simplll ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → A ∈ SubMnd ⁡ W
39 simpr ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → n ∈ ℕ
40 39 nnnn0d ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → n ∈ ℕ 0
41 simpllr ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → x ∈ Base W ↾ 𝑠 A
42 38 12 syl ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → A = Base W ↾ 𝑠 A
43 41 42 eleqtrrd ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → x ∈ A
44 eqid ⊢ ⋅ W ↾ 𝑠 A = ⋅ W ↾ 𝑠 A
45 4 11 44 submmulg ⊢ A ∈ SubMnd ⁡ W ∧ n ∈ ℕ 0 ∧ x ∈ A → n ⋅ W x = n ⋅ W ↾ 𝑠 A x
46 38 40 43 45 syl3anc ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → n ⋅ W x = n ⋅ W ↾ 𝑠 A x
47 36 37 46 breq123d ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A ∧ n ∈ ℕ → y ≤ W n ⋅ W x ↔ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
48 47 rexbidva ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A → ∃ n ∈ ℕ y ≤ W n ⋅ W x ↔ ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
49 35 48 imbi12d ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A ∧ y ∈ Base W ↾ 𝑠 A → 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x ↔ 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
50 49 ralbidva ⊢ A ∈ SubMnd ⁡ W ∧ x ∈ Base W ↾ 𝑠 A → ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x ↔ ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
51 50 ralbidva ⊢ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x ↔ ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
52 51 adantl ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x ↔ ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
53 20 52 sylibd ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ∀ y ∈ Base W 0 W < W x → ∃ n ∈ ℕ y ≤ W n ⋅ W x → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
54 10 53 mpd ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
55 resstos ⊢ W ∈ Toset ∧ A ∈ SubMnd ⁡ W → W ↾ 𝑠 A ∈ Toset
56 27 adantl ⊢ W ∈ Toset ∧ A ∈ SubMnd ⁡ W → W ↾ 𝑠 A ∈ Mnd
57 eqid ⊢ Base W ↾ 𝑠 A = Base W ↾ 𝑠 A
58 eqid ⊢ 0 W ↾ 𝑠 A = 0 W ↾ 𝑠 A
59 57 58 44 28 29 isarchi2 ⊢ W ↾ 𝑠 A ∈ Toset ∧ W ↾ 𝑠 A ∈ Mnd → W ↾ 𝑠 A ∈ Archi ↔ ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
60 55 56 59 syl2anc ⊢ W ∈ Toset ∧ A ∈ SubMnd ⁡ W → W ↾ 𝑠 A ∈ Archi ↔ ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
61 60 adantlr ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → W ↾ 𝑠 A ∈ Archi ↔ ∀ x ∈ Base W ↾ 𝑠 A ∀ y ∈ Base W ↾ 𝑠 A 0 W ↾ 𝑠 A < W ↾ 𝑠 A x → ∃ n ∈ ℕ y ≤ W ↾ 𝑠 A n ⋅ W ↾ 𝑠 A x
62 54 61 mpbird ⊢ W ∈ Toset ∧ W ∈ Archi ∧ A ∈ SubMnd ⁡ W → W ↾ 𝑠 A ∈ Archi