Metamath Proof Explorer

Theorem issubg2

Description: Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses issubg2.b 
|- B = ( Base ` G )
issubg2.p 
|- .+ = ( +g ` G )
issubg2.i 
|- I = ( invg ` G )
Assertion issubg2 
|- ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) )

Proof

Step Hyp Ref Expression
1 issubg2.b 
 |-  B = ( Base ` G )
2 issubg2.p 
 |-  .+ = ( +g ` G )
3 issubg2.i 
 |-  I = ( invg ` G )
4 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
5 eqid 
 |-  ( G |`s S ) = ( G |`s S )
6 5 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` ( G |`s S ) ) )
7 5 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> ( G |`s S ) e. Grp )
8 eqid 
 |-  ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) )
9 8 grpbn0 
 |-  ( ( G |`s S ) e. Grp -> ( Base ` ( G |`s S ) ) =/= (/) )
10 7 9 syl 
 |-  ( S e. ( SubGrp ` G ) -> ( Base ` ( G |`s S ) ) =/= (/) )
11 6 10 eqnetrd 
 |-  ( S e. ( SubGrp ` G ) -> S =/= (/) )
12 2 subgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )
13 12 3expa 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ x e. S ) /\ y e. S ) -> ( x .+ y ) e. S )
14 13 ralrimiva 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S ) -> A. y e. S ( x .+ y ) e. S )
15 3 subginvcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S ) -> ( I ` x ) e. S )
16 14 15 jca 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S ) -> ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) )
17 16 ralrimiva 
 |-  ( S e. ( SubGrp ` G ) -> A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) )
18 4 11 17 3jca 
 |-  ( S e. ( SubGrp ` G ) -> ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) )
19 simpl 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> G e. Grp )
20 simpr1 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> S C_ B )
21 5 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` ( G |`s S ) ) )
22 20 21 syl 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> S = ( Base ` ( G |`s S ) ) )
23 fvex 
 |-  ( Base ` ( G |`s S ) ) e. _V
24 22 23 eqeltrdi 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> S e. _V )
25 5 2 ressplusg 
 |-  ( S e. _V -> .+ = ( +g ` ( G |`s S ) ) )
26 24 25 syl 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> .+ = ( +g ` ( G |`s S ) ) )
27 simpr3 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) )
28 simpl 
 |-  ( ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) -> A. y e. S ( x .+ y ) e. S )
29 28 ralimi 
 |-  ( A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) -> A. x e. S A. y e. S ( x .+ y ) e. S )
30 27 29 syl 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> A. x e. S A. y e. S ( x .+ y ) e. S )
31 oveq1 
 |-  ( x = u -> ( x .+ y ) = ( u .+ y ) )
32 31 eleq1d 
 |-  ( x = u -> ( ( x .+ y ) e. S <-> ( u .+ y ) e. S ) )
33 oveq2 
 |-  ( y = v -> ( u .+ y ) = ( u .+ v ) )
34 33 eleq1d 
 |-  ( y = v -> ( ( u .+ y ) e. S <-> ( u .+ v ) e. S ) )
35 32 34 rspc2v 
 |-  ( ( u e. S /\ v e. S ) -> ( A. x e. S A. y e. S ( x .+ y ) e. S -> ( u .+ v ) e. S ) )
36 30 35 syl5com 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( ( u e. S /\ v e. S ) -> ( u .+ v ) e. S ) )
37 36 3impib 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S /\ v e. S ) -> ( u .+ v ) e. S )
38 20 sseld 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( u e. S -> u e. B ) )
39 20 sseld 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( v e. S -> v e. B ) )
40 20 sseld 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( w e. S -> w e. B ) )
41 38 39 40 3anim123d 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( ( u e. S /\ v e. S /\ w e. S ) -> ( u e. B /\ v e. B /\ w e. B ) ) )
42 41 imp 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ ( u e. S /\ v e. S /\ w e. S ) ) -> ( u e. B /\ v e. B /\ w e. B ) )
43 1 2 grpass 
 |-  ( ( G e. Grp /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
44 43 adantlr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
45 42 44 syldan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ ( u e. S /\ v e. S /\ w e. S ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
46 simpr2 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> S =/= (/) )
47 n0 
 |-  ( S =/= (/) <-> E. u u e. S )
48 46 47 sylib 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> E. u u e. S )
49 20 sselda 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> u e. B )
50 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
51 1 2 50 3 grplinv 
 |-  ( ( G e. Grp /\ u e. B ) -> ( ( I ` u ) .+ u ) = ( 0g ` G ) )
52 51 adantlr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. B ) -> ( ( I ` u ) .+ u ) = ( 0g ` G ) )
53 49 52 syldan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> ( ( I ` u ) .+ u ) = ( 0g ` G ) )
54 simpr 
 |-  ( ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) -> ( I ` x ) e. S )
55 54 ralimi 
 |-  ( A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) -> A. x e. S ( I ` x ) e. S )
56 27 55 syl 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> A. x e. S ( I ` x ) e. S )
57 fveq2 
 |-  ( x = u -> ( I ` x ) = ( I ` u ) )
58 57 eleq1d 
 |-  ( x = u -> ( ( I ` x ) e. S <-> ( I ` u ) e. S ) )
59 58 rspccva 
 |-  ( ( A. x e. S ( I ` x ) e. S /\ u e. S ) -> ( I ` u ) e. S )
60 56 59 sylan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> ( I ` u ) e. S )
61 simpr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> u e. S )
62 30 adantr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> A. x e. S A. y e. S ( x .+ y ) e. S )
63 ovrspc2v 
 |-  ( ( ( ( I ` u ) e. S /\ u e. S ) /\ A. x e. S A. y e. S ( x .+ y ) e. S ) -> ( ( I ` u ) .+ u ) e. S )
64 60 61 62 63 syl21anc 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> ( ( I ` u ) .+ u ) e. S )
65 53 64 eqeltrrd 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> ( 0g ` G ) e. S )
66 48 65 exlimddv 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( 0g ` G ) e. S )
67 1 2 50 grplid 
 |-  ( ( G e. Grp /\ u e. B ) -> ( ( 0g ` G ) .+ u ) = u )
68 67 adantlr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. B ) -> ( ( 0g ` G ) .+ u ) = u )
69 49 68 syldan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) /\ u e. S ) -> ( ( 0g ` G ) .+ u ) = u )
70 22 26 37 45 66 69 60 53 isgrpd 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> ( G |`s S ) e. Grp )
71 1 issubg 
 |-  ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) )
72 19 20 70 71 syl3anbrc 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) -> S e. ( SubGrp ` G ) )
73 72 ex 
 |-  ( G e. Grp -> ( ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) -> S e. ( SubGrp ` G ) ) )
74 18 73 impbid2 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x .+ y ) e. S /\ ( I ` x ) e. S ) ) ) )