Metamath Proof Explorer


Theorem submmulg

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

Ref Expression
Hypotheses submmulgcl.t
|- .xb = ( .g ` G )
submmulg.h
|- H = ( G |`s S )
submmulg.t
|- .x. = ( .g ` H )
Assertion submmulg
|- ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N .xb X ) = ( N .x. X ) )

Proof

Step Hyp Ref Expression
1 submmulgcl.t
 |-  .xb = ( .g ` G )
2 submmulg.h
 |-  H = ( G |`s S )
3 submmulg.t
 |-  .x. = ( .g ` H )
4 simpl1
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> S e. ( SubMnd ` G ) )
5 eqid
 |-  ( +g ` G ) = ( +g ` G )
6 2 5 ressplusg
 |-  ( S e. ( SubMnd ` G ) -> ( +g ` G ) = ( +g ` H ) )
7 4 6 syl
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( +g ` G ) = ( +g ` H ) )
8 7 seqeq2d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) )
9 8 fveq1d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) )
10 simpr
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> N e. NN )
11 eqid
 |-  ( Base ` G ) = ( Base ` G )
12 11 submss
 |-  ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
13 12 3ad2ant1
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> S C_ ( Base ` G ) )
14 simp3
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> X e. S )
15 13 14 sseldd
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> X e. ( Base ` G ) )
16 15 adantr
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> X e. ( Base ` G ) )
17 eqid
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
18 11 5 1 17 mulgnn
 |-  ( ( N e. NN /\ X e. ( Base ` G ) ) -> ( N .xb X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
19 10 16 18 syl2anc
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( N .xb X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
20 2 submbas
 |-  ( S e. ( SubMnd ` G ) -> S = ( Base ` H ) )
21 20 3ad2ant1
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> S = ( Base ` H ) )
22 14 21 eleqtrd
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> X e. ( Base ` H ) )
23 22 adantr
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> X e. ( Base ` H ) )
24 eqid
 |-  ( Base ` H ) = ( Base ` H )
25 eqid
 |-  ( +g ` H ) = ( +g ` H )
26 eqid
 |-  seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { X } ) )
27 24 25 3 26 mulgnn
 |-  ( ( N e. NN /\ X e. ( Base ` H ) ) -> ( N .x. X ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) )
28 10 23 27 syl2anc
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( N .x. X ) = ( seq 1 ( ( +g ` H ) , ( NN X. { X } ) ) ` N ) )
29 9 19 28 3eqtr4d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( N .xb X ) = ( N .x. X ) )
30 simpl1
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> S e. ( SubMnd ` G ) )
31 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
32 2 31 subm0
 |-  ( S e. ( SubMnd ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
33 30 32 syl
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( 0g ` G ) = ( 0g ` H ) )
34 15 adantr
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> X e. ( Base ` G ) )
35 11 31 1 mulg0
 |-  ( X e. ( Base ` G ) -> ( 0 .xb X ) = ( 0g ` G ) )
36 34 35 syl
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( 0 .xb X ) = ( 0g ` G ) )
37 22 adantr
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> X e. ( Base ` H ) )
38 eqid
 |-  ( 0g ` H ) = ( 0g ` H )
39 24 38 3 mulg0
 |-  ( X e. ( Base ` H ) -> ( 0 .x. X ) = ( 0g ` H ) )
40 37 39 syl
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( 0 .x. X ) = ( 0g ` H ) )
41 33 36 40 3eqtr4d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( 0 .xb X ) = ( 0 .x. X ) )
42 simpr
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> N = 0 )
43 42 oveq1d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .xb X ) = ( 0 .xb X ) )
44 42 oveq1d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .x. X ) = ( 0 .x. X ) )
45 41 43 44 3eqtr4d
 |-  ( ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .xb X ) = ( N .x. X ) )
46 simp2
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> N e. NN0 )
47 elnn0
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
48 46 47 sylib
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N e. NN \/ N = 0 ) )
49 29 45 48 mpjaodan
 |-  ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) -> ( N .xb X ) = ( N .x. X ) )