Metamath Proof Explorer

Theorem submod

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

Ref Expression
Hypotheses submod.h 
|- H = ( G |`s Y )
submod.o 
|- O = ( od ` G )
submod.p 
|- P = ( od ` H )
Assertion submod 
|- ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> ( O ` A ) = ( P ` A ) )

Proof

Step Hyp Ref Expression
1 submod.h 
 |-  H = ( G |`s Y )
2 submod.o 
 |-  O = ( od ` G )
3 submod.p 
 |-  P = ( od ` H )
4 simpll 
 |-  ( ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) /\ x e. NN ) -> Y e. ( SubMnd ` G ) )
5 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
6 5 adantl 
 |-  ( ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) /\ x e. NN ) -> x e. NN0 )
7 simplr 
 |-  ( ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) /\ x e. NN ) -> A e. Y )
8 eqid 
 |-  ( .g ` G ) = ( .g ` G )
9 eqid 
 |-  ( .g ` H ) = ( .g ` H )
10 8 1 9 submmulg 
 |-  ( ( Y e. ( SubMnd ` G ) /\ x e. NN0 /\ A e. Y ) -> ( x ( .g ` G ) A ) = ( x ( .g ` H ) A ) )
11 4 6 7 10 syl3anc 
 |-  ( ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) /\ x e. NN ) -> ( x ( .g ` G ) A ) = ( x ( .g ` H ) A ) )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 1 12 subm0 
 |-  ( Y e. ( SubMnd ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
14 13 ad2antrr 
 |-  ( ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) /\ x e. NN ) -> ( 0g ` G ) = ( 0g ` H ) )
15 11 14 eqeq12d 
 |-  ( ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) /\ x e. NN ) -> ( ( x ( .g ` G ) A ) = ( 0g ` G ) <-> ( x ( .g ` H ) A ) = ( 0g ` H ) ) )
16 15 rabbidva 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } )
17 eqeq1 
 |-  ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } -> ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = (/) <-> { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } = (/) ) )
18 infeq1 
 |-  ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } -> inf ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } , RR , < ) = inf ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } , RR , < ) )
19 17 18 ifbieq2d 
 |-  ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } -> if ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } , RR , < ) ) = if ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } , RR , < ) ) )
20 16 19 syl 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> if ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } , RR , < ) ) = if ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } , RR , < ) ) )
21 eqid 
 |-  ( Base ` G ) = ( Base ` G )
22 21 submss 
 |-  ( Y e. ( SubMnd ` G ) -> Y C_ ( Base ` G ) )
23 22 sselda 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> A e. ( Base ` G ) )
24 eqid 
 |-  { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) }
25 21 8 12 2 24 odval 
 |-  ( A e. ( Base ` G ) -> ( O ` A ) = if ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } , RR , < ) ) )
26 23 25 syl 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> ( O ` A ) = if ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` G ) A ) = ( 0g ` G ) } , RR , < ) ) )
27 simpr 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> A e. Y )
28 22 adantr 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> Y C_ ( Base ` G ) )
29 1 21 ressbas2 
 |-  ( Y C_ ( Base ` G ) -> Y = ( Base ` H ) )
30 28 29 syl 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> Y = ( Base ` H ) )
31 27 30 eleqtrd 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> A e. ( Base ` H ) )
32 eqid 
 |-  ( Base ` H ) = ( Base ` H )
33 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
34 eqid 
 |-  { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } = { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) }
35 32 9 33 3 34 odval 
 |-  ( A e. ( Base ` H ) -> ( P ` A ) = if ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } , RR , < ) ) )
36 31 35 syl 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> ( P ` A ) = if ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } = (/) , 0 , inf ( { x e. NN | ( x ( .g ` H ) A ) = ( 0g ` H ) } , RR , < ) ) )
37 20 26 36 3eqtr4d 
 |-  ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> ( O ` A ) = ( P ` A ) )