This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( 𝐺 ↾s 𝑌 )
submod.o ⊢ 𝑂 = ( od ‘ 𝐺 )
submod.p ⊢ 𝑃 = ( od ‘ 𝐻 )
Assertion submod ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 submod.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑌 )
2 submod.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 submod.p ⊢ 𝑃 = ( od ‘ 𝐻 )
4 simpll ⊢ ( ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ ℕ ) → 𝑌 ∈ ( SubMnd ‘ 𝐺 ) )
5 nnnn0 ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 )
6 5 adantl ⊢ ( ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ0 )
7 simplr ⊢ ( ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ ℕ ) → 𝐴 ∈ 𝑌 )
8 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9 eqid ⊢ ( .g ‘ 𝐻 ) = ( .g ‘ 𝐻 )
10 8 1 9 submmulg ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑥 ∈ ℕ0 ∧ 𝐴 ∈ 𝑌 ) → ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) )
11 4 6 7 10 syl3anc ⊢ ( ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) )
12 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13 1 12 subm0 ⊢ ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
14 13 ad2antrr ⊢ ( ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ ℕ ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
15 11 14 eqeq12d ⊢ ( ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) ↔ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) ) )
16 15 rabbidva ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } )
17 eqeq1 ⊢ ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } → ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = ∅ ↔ { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } = ∅ ) )
18 infeq1 ⊢ ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } → inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } , ℝ , < ) = inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } , ℝ , < ) )
19 17 18 ifbieq2d ⊢ ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } → if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } , ℝ , < ) ) = if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } , ℝ , < ) ) )
20 16 19 syl ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } , ℝ , < ) ) = if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } , ℝ , < ) ) )
21 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
22 21 submss ⊢ ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) → 𝑌 ⊆ ( Base ‘ 𝐺 ) )
23 22 sselda ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
24 eqid ⊢ { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) }
25 21 8 12 2 24 odval ⊢ ( 𝐴 ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ 𝐴 ) = if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } , ℝ , < ) ) )
26 23 25 syl ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) = ( 0g ‘ 𝐺 ) } , ℝ , < ) ) )
27 simpr ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐴 ∈ 𝑌 )
28 22 adantr ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → 𝑌 ⊆ ( Base ‘ 𝐺 ) )
29 1 21 ressbas2 ⊢ ( 𝑌 ⊆ ( Base ‘ 𝐺 ) → 𝑌 = ( Base ‘ 𝐻 ) )
30 28 29 syl ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → 𝑌 = ( Base ‘ 𝐻 ) )
31 27 30 eleqtrd ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝐻 ) )
32 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
33 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
34 eqid ⊢ { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) }
35 32 9 33 3 34 odval ⊢ ( 𝐴 ∈ ( Base ‘ 𝐻 ) → ( 𝑃 ‘ 𝐴 ) = if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } , ℝ , < ) ) )
36 31 35 syl ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑃 ‘ 𝐴 ) = if ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } = ∅ , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑥 ( .g ‘ 𝐻 ) 𝐴 ) = ( 0g ‘ 𝐻 ) } , ℝ , < ) ) )
37 20 26 36 3eqtr4d ⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )