Description: Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof shortened by AV, 18-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mgpress.1 | |
|
mgpress.2 | |
||
Assertion | mgpress | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mgpress.1 | |
|
2 | mgpress.2 | |
|
3 | simpr | |
|
4 | 2 | fvexi | |
5 | 4 | a1i | |
6 | simplr | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | 2 8 | mgpbas | |
10 | 7 9 | ressid2 | |
11 | 3 5 6 10 | syl3anc | |
12 | simpll | |
|
13 | 1 8 | ressid2 | |
14 | 3 12 6 13 | syl3anc | |
15 | 14 | fveq2d | |
16 | 2 11 15 | 3eqtr4a | |
17 | eqid | |
|
18 | 2 17 | mgpval | |
19 | 18 | oveq1i | |
20 | simpr | |
|
21 | 4 | a1i | |
22 | simplr | |
|
23 | 7 9 | ressval2 | |
24 | 20 21 22 23 | syl3anc | |
25 | eqid | |
|
26 | eqid | |
|
27 | 25 26 | mgpval | |
28 | simpll | |
|
29 | 1 8 | ressval2 | |
30 | 20 28 22 29 | syl3anc | |
31 | 1 17 | ressmulr | |
32 | 31 | eqcomd | |
33 | 32 | ad2antlr | |
34 | 33 | opeq2d | |
35 | 30 34 | oveq12d | |
36 | 27 35 | eqtrid | |
37 | basendxnplusgndx | |
|
38 | 37 | necomi | |
39 | fvex | |
|
40 | fvex | |
|
41 | 40 | inex2 | |
42 | fvex | |
|
43 | fvex | |
|
44 | 42 43 | setscom | |
45 | 39 41 44 | mpanr12 | |
46 | 28 38 45 | sylancl | |
47 | 36 46 | eqtr4d | |
48 | 19 24 47 | 3eqtr4a | |
49 | 16 48 | pm2.61dan | |