Description: The direct sum of an element X of a subgroup A is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | grplsmid.p | |
|
Assertion | grplsmid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grplsmid.p | |
|
2 | subgrcl | |
|
3 | 2 | adantr | |
4 | eqid | |
|
5 | 4 | subgss | |
6 | 5 | sselda | |
7 | 6 | snssd | |
8 | 5 | adantr | |
9 | eqid | |
|
10 | 4 9 1 | lsmelvalx | |
11 | 3 7 8 10 | syl3anc | |
12 | oveq1 | |
|
13 | 12 | eqeq2d | |
14 | 13 | rexbidv | |
15 | 14 | rexsng | |
16 | 15 | adantl | |
17 | simpr | |
|
18 | 9 | subgcl | |
19 | 18 | ad4ant123 | |
20 | 17 19 | eqeltrd | |
21 | 20 | r19.29an | |
22 | simpll | |
|
23 | eqid | |
|
24 | 23 | subginvcl | |
25 | 24 | adantr | |
26 | simpr | |
|
27 | 9 | subgcl | |
28 | 22 25 26 27 | syl3anc | |
29 | oveq2 | |
|
30 | 29 | eqeq2d | |
31 | 30 | adantl | |
32 | 3 | adantr | |
33 | 6 | adantr | |
34 | 8 | sselda | |
35 | 4 9 23 | grpasscan1 | |
36 | 32 33 34 35 | syl3anc | |
37 | 36 | eqcomd | |
38 | 28 31 37 | rspcedvd | |
39 | 21 38 | impbida | |
40 | 11 16 39 | 3bitrd | |
41 | 40 | eqrdv | |