Metamath Proof Explorer

Theorem subgmulg

Description: A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses subgmulgcl.t 
|- .x. = ( .g ` G )
subgmulg.h 
|- H = ( G |`s S )
subgmulg.t 
|- .xb = ( .g ` H )
Assertion subgmulg 
|- ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) = ( N .xb X ) )

Proof

Step Hyp Ref Expression
1 subgmulgcl.t 
 |-  .x. = ( .g ` G )
2 subgmulg.h 
 |-  H = ( G |`s S )
3 subgmulg.t 
 |-  .xb = ( .g ` H )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 2 4 subg0 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
6 5 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( 0g ` G ) = ( 0g ` H ) )
7 6 ifeq1d 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
8 eqid 
 |-  ( +g ` G ) = ( +g ` G )
9 2 8 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
10 9 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( +g ` G ) = ( +g ` H ) )
11 10 seqeq2d 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) )
12 11 adantr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) )
13 12 fveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) )
14 13 ifeq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) = if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) )
15 simp2 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> N e. ZZ )
16 15 zred 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> N e. RR )
17 0re 
 |-  0 e. RR
18 axlttri 
 |-  ( ( N e. RR /\ 0 e. RR ) -> ( N < 0 <-> -. ( N = 0 \/ 0 < N ) ) )
19 16 17 18 sylancl 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N < 0 <-> -. ( N = 0 \/ 0 < N ) ) )
20 ioran 
 |-  ( -. ( N = 0 \/ 0 < N ) <-> ( -. N = 0 /\ -. 0 < N ) )
21 19 20 bitrdi 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N < 0 <-> ( -. N = 0 /\ -. 0 < N ) ) )
22 21 biimpar 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> N < 0 )
23 simpl1 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> S e. ( SubGrp ` G ) )
24 15 adantr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> N e. ZZ )
25 24 znegcld 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> -u N e. ZZ )
26 16 lt0neg1d 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N < 0 <-> 0 < -u N ) )
27 26 biimpa 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> 0 < -u N )
28 elnnz 
 |-  ( -u N e. NN <-> ( -u N e. ZZ /\ 0 < -u N ) )
29 25 27 28 sylanbrc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> -u N e. NN )
30 eqid 
 |-  ( Base ` G ) = ( Base ` G )
31 30 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
32 31 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> S C_ ( Base ` G ) )
33 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> X e. S )
34 32 33 sseldd 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> X e. ( Base ` G ) )
35 34 adantr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> X e. ( Base ` G ) )
36 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
37 30 8 1 36 mulgnn 
 |-  ( ( -u N e. NN /\ X e. ( Base ` G ) ) -> ( -u N .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) )
38 29 35 37 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( -u N .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) )
39 33 adantr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> X e. S )
40 1 subgmulgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ -u N e. ZZ /\ X e. S ) -> ( -u N .x. X ) e. S )
41 23 25 39 40 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( -u N .x. X ) e. S )
42 38 41 eqeltrrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) e. S )
43 eqid 
 |-  ( invg ` G ) = ( invg ` G )
44 eqid 
 |-  ( invg ` H ) = ( invg ` H )
45 2 43 44 subginv 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) e. S ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) )
46 23 42 45 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ N < 0 ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) )
47 22 46 syldan 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) )
48 11 adantr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) )
49 48 fveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) )
50 49 fveq2d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( ( invg ` H ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) )
51 47 50 eqtrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ ( -. N = 0 /\ -. 0 < N ) ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) )
52 51 anassrs 
 |-  ( ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) /\ -. 0 < N ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) )
53 52 ifeq2da 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) = if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) )
54 14 53 eqtrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) /\ -. N = 0 ) -> if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) = if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) )
55 54 ifeq2da 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
56 7 55 eqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
57 30 8 4 43 1 36 mulgval 
 |-  ( ( N e. ZZ /\ X e. ( Base ` G ) ) -> ( N .x. X ) = if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
58 15 34 57 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) = if ( N = 0 , ( 0g ` G ) , if ( 0 < N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
59 2 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
60 59 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> S = ( Base ` H ) )
61 33 60 eleqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> X e. ( Base ` H ) )
62 eqid 
 |-  ( Base ` H ) = ( Base ` H )
63 eqid 
 |-  ( +g ` H ) = ( +g ` H )
64 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
65 eqid 
 |-  seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) )
66 62 63 64 44 3 65 mulgval 
 |-  ( ( N e. ZZ /\ X e. ( Base ` H ) ) -> ( N .xb X ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
67 15 61 66 syl2anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .xb X ) = if ( N = 0 , ( 0g ` H ) , if ( 0 < N , ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` -u N ) ) ) ) )
68 56 58 67 3eqtr4d 
 |-  ( ( S e. ( SubGrp ` G ) /\ N e. ZZ /\ X e. S ) -> ( N .x. X ) = ( N .xb X ) )