Metamath Proof Explorer

Theorem prmgrpsimpgd

Description: A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses prmgrpsimpgd.1 
|- B = ( Base ` G )
prmgrpsimpgd.2 
|- ( ph -> G e. Grp )
prmgrpsimpgd.3 
|- ( ph -> ( # ` B ) e. Prime )
Assertion prmgrpsimpgd 
|- ( ph -> G e. SimpGrp )

Proof

Step Hyp Ref Expression
1 prmgrpsimpgd.1 
 |-  B = ( Base ` G )
2 prmgrpsimpgd.2 
 |-  ( ph -> G e. Grp )
3 prmgrpsimpgd.3 
 |-  ( ph -> ( # ` B ) e. Prime )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 fveq2 
 |-  ( { ( 0g ` G ) } = B -> ( # ` { ( 0g ` G ) } ) = ( # ` B ) )
6 5 adantl 
 |-  ( ( ph /\ { ( 0g ` G ) } = B ) -> ( # ` { ( 0g ` G ) } ) = ( # ` B ) )
7 4 fvexi 
 |-  ( 0g ` G ) e. _V
8 hashsng 
 |-  ( ( 0g ` G ) e. _V -> ( # ` { ( 0g ` G ) } ) = 1 )
9 7 8 mp1i 
 |-  ( ( ph /\ { ( 0g ` G ) } = B ) -> ( # ` { ( 0g ` G ) } ) = 1 )
10 6 9 eqtr3d 
 |-  ( ( ph /\ { ( 0g ` G ) } = B ) -> ( # ` B ) = 1 )
11 3 adantr 
 |-  ( ( ph /\ { ( 0g ` G ) } = B ) -> ( # ` B ) e. Prime )
12 10 11 eqeltrrd 
 |-  ( ( ph /\ { ( 0g ` G ) } = B ) -> 1 e. Prime )
13 1nprm 
 |-  -. 1 e. Prime
14 13 a1i 
 |-  ( ( ph /\ { ( 0g ` G ) } = B ) -> -. 1 e. Prime )
15 12 14 pm2.65da 
 |-  ( ph -> -. { ( 0g ` G ) } = B )
16 nsgsubg 
 |-  ( x e. ( NrmSGrp ` G ) -> x e. ( SubGrp ` G ) )
17 eqid 
 |-  ( # ` B ) = ( # ` B )
18 1 fvexi 
 |-  B e. _V
19 18 a1i 
 |-  ( ph -> B e. _V )
20 prmnn 
 |-  ( ( # ` B ) e. Prime -> ( # ` B ) e. NN )
21 3 20 syl 
 |-  ( ph -> ( # ` B ) e. NN )
22 21 nnnn0d 
 |-  ( ph -> ( # ` B ) e. NN0 )
23 hashvnfin 
 |-  ( ( B e. _V /\ ( # ` B ) e. NN0 ) -> ( ( # ` B ) = ( # ` B ) -> B e. Fin ) )
24 19 22 23 syl2anc 
 |-  ( ph -> ( ( # ` B ) = ( # ` B ) -> B e. Fin ) )
25 17 24 mpi 
 |-  ( ph -> B e. Fin )
26 25 ad2antrr 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = ( # ` B ) ) -> B e. Fin )
27 1 subgss 
 |-  ( x e. ( SubGrp ` G ) -> x C_ B )
28 27 ad2antlr 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = ( # ` B ) ) -> x C_ B )
29 simpr 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = ( # ` B ) ) -> ( # ` x ) = ( # ` B ) )
30 26 28 29 phphashrd 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = ( # ` B ) ) -> x = B )
31 30 olcd 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = ( # ` B ) ) -> ( x = { ( 0g ` G ) } \/ x = B ) )
32 simpr 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = 1 ) -> ( # ` x ) = 1 )
33 4 subg0cl 
 |-  ( x e. ( SubGrp ` G ) -> ( 0g ` G ) e. x )
34 33 ad2antlr 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = 1 ) -> ( 0g ` G ) e. x )
35 vex 
 |-  x e. _V
36 35 a1i 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = 1 ) -> x e. _V )
37 32 34 36 hash1elsn 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = 1 ) -> x = { ( 0g ` G ) } )
38 37 orcd 
 |-  ( ( ( ph /\ x e. ( SubGrp ` G ) ) /\ ( # ` x ) = 1 ) -> ( x = { ( 0g ` G ) } \/ x = B ) )
39 1 lagsubg 
 |-  ( ( x e. ( SubGrp ` G ) /\ B e. Fin ) -> ( # ` x ) || ( # ` B ) )
40 25 39 sylan2 
 |-  ( ( x e. ( SubGrp ` G ) /\ ph ) -> ( # ` x ) || ( # ` B ) )
41 40 ancoms 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( # ` x ) || ( # ` B ) )
42 3 adantr 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( # ` B ) e. Prime )
43 25 adantr 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> B e. Fin )
44 27 adantl 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> x C_ B )
45 43 44 ssfid 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> x e. Fin )
46 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
47 45 46 syl 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( # ` x ) e. NN0 )
48 33 adantl 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( 0g ` G ) e. x )
49 35 a1i 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> x e. _V )
50 48 49 hashelne0d 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> -. ( # ` x ) = 0 )
51 50 neqned 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( # ` x ) =/= 0 )
52 elnnne0 
 |-  ( ( # ` x ) e. NN <-> ( ( # ` x ) e. NN0 /\ ( # ` x ) =/= 0 ) )
53 47 51 52 sylanbrc 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( # ` x ) e. NN )
54 dvdsprime 
 |-  ( ( ( # ` B ) e. Prime /\ ( # ` x ) e. NN ) -> ( ( # ` x ) || ( # ` B ) <-> ( ( # ` x ) = ( # ` B ) \/ ( # ` x ) = 1 ) ) )
55 42 53 54 syl2anc 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( ( # ` x ) || ( # ` B ) <-> ( ( # ` x ) = ( # ` B ) \/ ( # ` x ) = 1 ) ) )
56 41 55 mpbid 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( ( # ` x ) = ( # ` B ) \/ ( # ` x ) = 1 ) )
57 31 38 56 mpjaodan 
 |-  ( ( ph /\ x e. ( SubGrp ` G ) ) -> ( x = { ( 0g ` G ) } \/ x = B ) )
58 16 57 sylan2 
 |-  ( ( ph /\ x e. ( NrmSGrp ` G ) ) -> ( x = { ( 0g ` G ) } \/ x = B ) )
59 1 4 2 15 58 2nsgsimpgd 
 |-  ( ph -> G e. SimpGrp )