Description: A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | submmulgcl.t | |
|
submmulg.h | |
||
submmulg.t | |
||
Assertion | submmulg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | submmulgcl.t | |
|
2 | submmulg.h | |
|
3 | submmulg.t | |
|
4 | simpl1 | |
|
5 | eqid | |
|
6 | 2 5 | ressplusg | |
7 | 4 6 | syl | |
8 | 7 | seqeq2d | |
9 | 8 | fveq1d | |
10 | simpr | |
|
11 | eqid | |
|
12 | 11 | submss | |
13 | 12 | 3ad2ant1 | |
14 | simp3 | |
|
15 | 13 14 | sseldd | |
16 | 15 | adantr | |
17 | eqid | |
|
18 | 11 5 1 17 | mulgnn | |
19 | 10 16 18 | syl2anc | |
20 | 2 | submbas | |
21 | 20 | 3ad2ant1 | |
22 | 14 21 | eleqtrd | |
23 | 22 | adantr | |
24 | eqid | |
|
25 | eqid | |
|
26 | eqid | |
|
27 | 24 25 3 26 | mulgnn | |
28 | 10 23 27 | syl2anc | |
29 | 9 19 28 | 3eqtr4d | |
30 | simpl1 | |
|
31 | eqid | |
|
32 | 2 31 | subm0 | |
33 | 30 32 | syl | |
34 | 15 | adantr | |
35 | 11 31 1 | mulg0 | |
36 | 34 35 | syl | |
37 | 22 | adantr | |
38 | eqid | |
|
39 | 24 38 3 | mulg0 | |
40 | 37 39 | syl | |
41 | 33 36 40 | 3eqtr4d | |
42 | simpr | |
|
43 | 42 | oveq1d | |
44 | 42 | oveq1d | |
45 | 41 43 44 | 3eqtr4d | |
46 | simp2 | |
|
47 | elnn0 | |
|
48 | 46 47 | sylib | |
49 | 29 45 48 | mpjaodan | |