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