Metamath Proof Explorer

Theorem submod

Description: The order of an element is the same in a submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015) (Proof shortened by AV, 5-Oct-2020)

Ref Expression
Hypotheses submod.h ⊢ H = G ↾ 𝑠 Y
submod.o ⊢ O = od ⁡ G
submod.p ⊢ P = od ⁡ H
Assertion submod ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → O ⁡ A = P ⁡ A

Proof

Step Hyp Ref Expression
1 submod.h ⊢ H = G ↾ 𝑠 Y
2 submod.o ⊢ O = od ⁡ G
3 submod.p ⊢ P = od ⁡ H
4 simpll ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y ∧ x ∈ ℕ → Y ∈ SubMnd ⁡ G
5 nnnn0 ⊢ x ∈ ℕ → x ∈ ℕ 0
6 5 adantl ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y ∧ x ∈ ℕ → x ∈ ℕ 0
7 simplr ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y ∧ x ∈ ℕ → A ∈ Y
8 eqid ⊢ ⋅ G = ⋅ G
9 eqid ⊢ ⋅ H = ⋅ H
10 8 1 9 submmulg ⊢ Y ∈ SubMnd ⁡ G ∧ x ∈ ℕ 0 ∧ A ∈ Y → x ⋅ G A = x ⋅ H A
11 4 6 7 10 syl3anc ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y ∧ x ∈ ℕ → x ⋅ G A = x ⋅ H A
12 eqid ⊢ 0 G = 0 G
13 1 12 subm0 ⊢ Y ∈ SubMnd ⁡ G → 0 G = 0 H
14 13 ad2antrr ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y ∧ x ∈ ℕ → 0 G = 0 H
15 11 14 eqeq12d ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y ∧ x ∈ ℕ → x ⋅ G A = 0 G ↔ x ⋅ H A = 0 H
16 15 rabbidva ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → x ∈ ℕ | x ⋅ G A = 0 G = x ∈ ℕ | x ⋅ H A = 0 H
17 eqeq1 ⊢ x ∈ ℕ | x ⋅ G A = 0 G = x ∈ ℕ | x ⋅ H A = 0 H → x ∈ ℕ | x ⋅ G A = 0 G = ∅ ↔ x ∈ ℕ | x ⋅ H A = 0 H = ∅
18 infeq1 ⊢ x ∈ ℕ | x ⋅ G A = 0 G = x ∈ ℕ | x ⋅ H A = 0 H → inf x ∈ ℕ | x ⋅ G A = 0 G ℝ < = inf x ∈ ℕ | x ⋅ H A = 0 H ℝ <
19 17 18 ifbieq2d ⊢ x ∈ ℕ | x ⋅ G A = 0 G = x ∈ ℕ | x ⋅ H A = 0 H → if x ∈ ℕ | x ⋅ G A = 0 G = ∅ 0 inf x ∈ ℕ | x ⋅ G A = 0 G ℝ < = if x ∈ ℕ | x ⋅ H A = 0 H = ∅ 0 inf x ∈ ℕ | x ⋅ H A = 0 H ℝ <
20 16 19 syl ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → if x ∈ ℕ | x ⋅ G A = 0 G = ∅ 0 inf x ∈ ℕ | x ⋅ G A = 0 G ℝ < = if x ∈ ℕ | x ⋅ H A = 0 H = ∅ 0 inf x ∈ ℕ | x ⋅ H A = 0 H ℝ <
21 eqid ⊢ Base G = Base G
22 21 submss ⊢ Y ∈ SubMnd ⁡ G → Y ⊆ Base G
23 22 sselda ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → A ∈ Base G
24 eqid ⊢ x ∈ ℕ | x ⋅ G A = 0 G = x ∈ ℕ | x ⋅ G A = 0 G
25 21 8 12 2 24 odval ⊢ A ∈ Base G → O ⁡ A = if x ∈ ℕ | x ⋅ G A = 0 G = ∅ 0 inf x ∈ ℕ | x ⋅ G A = 0 G ℝ <
26 23 25 syl ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → O ⁡ A = if x ∈ ℕ | x ⋅ G A = 0 G = ∅ 0 inf x ∈ ℕ | x ⋅ G A = 0 G ℝ <
27 simpr ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → A ∈ Y
28 22 adantr ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → Y ⊆ Base G
29 1 21 ressbas2 ⊢ Y ⊆ Base G → Y = Base H
30 28 29 syl ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → Y = Base H
31 27 30 eleqtrd ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → A ∈ Base H
32 eqid ⊢ Base H = Base H
33 eqid ⊢ 0 H = 0 H
34 eqid ⊢ x ∈ ℕ | x ⋅ H A = 0 H = x ∈ ℕ | x ⋅ H A = 0 H
35 32 9 33 3 34 odval ⊢ A ∈ Base H → P ⁡ A = if x ∈ ℕ | x ⋅ H A = 0 H = ∅ 0 inf x ∈ ℕ | x ⋅ H A = 0 H ℝ <
36 31 35 syl ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → P ⁡ A = if x ∈ ℕ | x ⋅ H A = 0 H = ∅ 0 inf x ∈ ℕ | x ⋅ H A = 0 H ℝ <
37 20 26 36 3eqtr4d ⊢ Y ∈ SubMnd ⁡ G ∧ A ∈ Y → O ⁡ A = P ⁡ A