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