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 ) )