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⋅GA=x⋅HA
11 4 6 7 10 syl3anc ⊢Y∈SubMnd⁡G∧A∈Y∧x∈ℕ→x⋅GA=x⋅HA
12 eqid ⊢0G=0G
13 1 12 subm0 ⊢Y∈SubMnd⁡G→0G=0H
14 13 ad2antrr ⊢Y∈SubMnd⁡G∧A∈Y∧x∈ℕ→0G=0H
15 11 14 eqeq12d ⊢Y∈SubMnd⁡G∧A∈Y∧x∈ℕ→x⋅GA=0G↔x⋅HA=0H
16 15 rabbidva ⊢Y∈SubMnd⁡G∧A∈Y→x∈ℕ|x⋅GA=0G=x∈ℕ|x⋅HA=0H
17 eqeq1 ⊢x∈ℕ|x⋅GA=0G=x∈ℕ|x⋅HA=0H→x∈ℕ|x⋅GA=0G=∅↔x∈ℕ|x⋅HA=0H=∅
18 infeq1 ⊢x∈ℕ|x⋅GA=0G=x∈ℕ|x⋅HA=0H→supx∈ℕ|x⋅GA=0Gℝ<=supx∈ℕ|x⋅HA=0Hℝ<
19 17 18 ifbieq2d ⊢x∈ℕ|x⋅GA=0G=x∈ℕ|x⋅HA=0H→ifx∈ℕ|x⋅GA=0G=∅0supx∈ℕ|x⋅GA=0Gℝ<=ifx∈ℕ|x⋅HA=0H=∅0supx∈ℕ|x⋅HA=0Hℝ<
20 16 19 syl ⊢Y∈SubMnd⁡G∧A∈Y→ifx∈ℕ|x⋅GA=0G=∅0supx∈ℕ|x⋅GA=0Gℝ<=ifx∈ℕ|x⋅HA=0H=∅0supx∈ℕ|x⋅HA=0Hℝ<
21 eqid ⊢BaseG=BaseG
22 21 submss ⊢Y∈SubMnd⁡G→Y⊆BaseG
23 22 sselda ⊢Y∈SubMnd⁡G∧A∈Y→A∈BaseG
24 eqid ⊢x∈ℕ|x⋅GA=0G=x∈ℕ|x⋅GA=0G
25 21 8 12 2 24 odval ⊢A∈BaseG→O⁡A=ifx∈ℕ|x⋅GA=0G=∅0supx∈ℕ|x⋅GA=0Gℝ<
26 23 25 syl ⊢Y∈SubMnd⁡G∧A∈Y→O⁡A=ifx∈ℕ|x⋅GA=0G=∅0supx∈ℕ|x⋅GA=0Gℝ<
27 simpr ⊢Y∈SubMnd⁡G∧A∈Y→A∈Y
28 22 adantr ⊢Y∈SubMnd⁡G∧A∈Y→Y⊆BaseG
29 1 21 ressbas2 ⊢Y⊆BaseG→Y=BaseH
30 28 29 syl ⊢Y∈SubMnd⁡G∧A∈Y→Y=BaseH
31 27 30 eleqtrd ⊢Y∈SubMnd⁡G∧A∈Y→A∈BaseH
32 eqid ⊢BaseH=BaseH
33 eqid ⊢0H=0H
34 eqid ⊢x∈ℕ|x⋅HA=0H=x∈ℕ|x⋅HA=0H
35 32 9 33 3 34 odval ⊢A∈BaseH→P⁡A=ifx∈ℕ|x⋅HA=0H=∅0supx∈ℕ|x⋅HA=0Hℝ<
36 31 35 syl ⊢Y∈SubMnd⁡G∧A∈Y→P⁡A=ifx∈ℕ|x⋅HA=0H=∅0supx∈ℕ|x⋅HA=0Hℝ<
37 20 26 36 3eqtr4d ⊢Y∈SubMnd⁡G∧A∈Y→O⁡A=P⁡A