Description: If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 2nsgsimpgd.1 | |
|
2nsgsimpgd.2 | |
||
2nsgsimpgd.3 | |
||
2nsgsimpgd.4 | |
||
2nsgsimpgd.5 | |
||
Assertion | 2nsgsimpgd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nsgsimpgd.1 | |
|
2 | 2nsgsimpgd.2 | |
|
3 | 2nsgsimpgd.3 | |
|
4 | 2nsgsimpgd.4 | |
|
5 | 2nsgsimpgd.5 | |
|
6 | elprg | |
|
7 | 6 | adantl | |
8 | 5 7 | mpbird | |
9 | simpr | |
|
10 | 2 | 0nsg | |
11 | 3 10 | syl | |
12 | 11 | adantr | |
13 | 9 12 | eqeltrd | |
14 | 13 | adantlr | |
15 | simpr | |
|
16 | 1 | nsgid | |
17 | 3 16 | syl | |
18 | 17 | adantr | |
19 | 15 18 | eqeltrd | |
20 | 19 | adantlr | |
21 | elpri | |
|
22 | 21 | adantl | |
23 | 14 20 22 | mpjaodan | |
24 | 8 23 | impbida | |
25 | 24 | eqrdv | |
26 | snex | |
|
27 | 26 | a1i | |
28 | 1 | fvexi | |
29 | 28 | a1i | |
30 | 27 29 4 | enpr2d | |
31 | 25 30 | eqbrtrd | |
32 | 3 31 | issimpgd | |