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 ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )