Metamath Proof Explorer

Theorem subgint

Description: The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Assertion subgint 
|- ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 intssuni 
 |-  ( S =/= (/) -> |^| S C_ U. S )
2 1 adantl 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> |^| S C_ U. S )
3 ssel2 
 |-  ( ( S C_ ( SubGrp ` G ) /\ g e. S ) -> g e. ( SubGrp ` G ) )
4 3 adantlr 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ g e. S ) -> g e. ( SubGrp ` G ) )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 5 subgss 
 |-  ( g e. ( SubGrp ` G ) -> g C_ ( Base ` G ) )
7 4 6 syl 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ g e. S ) -> g C_ ( Base ` G ) )
8 7 ralrimiva 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> A. g e. S g C_ ( Base ` G ) )
9 unissb 
 |-  ( U. S C_ ( Base ` G ) <-> A. g e. S g C_ ( Base ` G ) )
10 8 9 sylibr 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> U. S C_ ( Base ` G ) )
11 2 10 sstrd 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> |^| S C_ ( Base ` G ) )
12 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
13 12 subg0cl 
 |-  ( g e. ( SubGrp ` G ) -> ( 0g ` G ) e. g )
14 4 13 syl 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ g e. S ) -> ( 0g ` G ) e. g )
15 14 ralrimiva 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> A. g e. S ( 0g ` G ) e. g )
16 fvex 
 |-  ( 0g ` G ) e. _V
17 16 elint2 
 |-  ( ( 0g ` G ) e. |^| S <-> A. g e. S ( 0g ` G ) e. g )
18 15 17 sylibr 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> ( 0g ` G ) e. |^| S )
19 18 ne0d 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> |^| S =/= (/) )
20 4 adantlr 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ g e. S ) -> g e. ( SubGrp ` G ) )
21 simprl 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> x e. |^| S )
22 elinti 
 |-  ( x e. |^| S -> ( g e. S -> x e. g ) )
23 22 imp 
 |-  ( ( x e. |^| S /\ g e. S ) -> x e. g )
24 21 23 sylan 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ g e. S ) -> x e. g )
25 simprr 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> y e. |^| S )
26 elinti 
 |-  ( y e. |^| S -> ( g e. S -> y e. g ) )
27 26 imp 
 |-  ( ( y e. |^| S /\ g e. S ) -> y e. g )
28 25 27 sylan 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ g e. S ) -> y e. g )
29 eqid 
 |-  ( +g ` G ) = ( +g ` G )
30 29 subgcl 
 |-  ( ( g e. ( SubGrp ` G ) /\ x e. g /\ y e. g ) -> ( x ( +g ` G ) y ) e. g )
31 20 24 28 30 syl3anc 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ g e. S ) -> ( x ( +g ` G ) y ) e. g )
32 31 ralrimiva 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> A. g e. S ( x ( +g ` G ) y ) e. g )
33 ovex 
 |-  ( x ( +g ` G ) y ) e. _V
34 33 elint2 
 |-  ( ( x ( +g ` G ) y ) e. |^| S <-> A. g e. S ( x ( +g ` G ) y ) e. g )
35 32 34 sylibr 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> ( x ( +g ` G ) y ) e. |^| S )
36 35 anassrs 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) /\ y e. |^| S ) -> ( x ( +g ` G ) y ) e. |^| S )
37 36 ralrimiva 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) -> A. y e. |^| S ( x ( +g ` G ) y ) e. |^| S )
38 4 adantlr 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) /\ g e. S ) -> g e. ( SubGrp ` G ) )
39 23 adantll 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) /\ g e. S ) -> x e. g )
40 eqid 
 |-  ( invg ` G ) = ( invg ` G )
41 40 subginvcl 
 |-  ( ( g e. ( SubGrp ` G ) /\ x e. g ) -> ( ( invg ` G ) ` x ) e. g )
42 38 39 41 syl2anc 
 |-  ( ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) /\ g e. S ) -> ( ( invg ` G ) ` x ) e. g )
43 42 ralrimiva 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) -> A. g e. S ( ( invg ` G ) ` x ) e. g )
44 fvex 
 |-  ( ( invg ` G ) ` x ) e. _V
45 44 elint2 
 |-  ( ( ( invg ` G ) ` x ) e. |^| S <-> A. g e. S ( ( invg ` G ) ` x ) e. g )
46 43 45 sylibr 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) -> ( ( invg ` G ) ` x ) e. |^| S )
47 37 46 jca 
 |-  ( ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) /\ x e. |^| S ) -> ( A. y e. |^| S ( x ( +g ` G ) y ) e. |^| S /\ ( ( invg ` G ) ` x ) e. |^| S ) )
48 47 ralrimiva 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> A. x e. |^| S ( A. y e. |^| S ( x ( +g ` G ) y ) e. |^| S /\ ( ( invg ` G ) ` x ) e. |^| S ) )
49 ssn0 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> ( SubGrp ` G ) =/= (/) )
50 n0 
 |-  ( ( SubGrp ` G ) =/= (/) <-> E. g g e. ( SubGrp ` G ) )
51 subgrcl 
 |-  ( g e. ( SubGrp ` G ) -> G e. Grp )
52 51 exlimiv 
 |-  ( E. g g e. ( SubGrp ` G ) -> G e. Grp )
53 50 52 sylbi 
 |-  ( ( SubGrp ` G ) =/= (/) -> G e. Grp )
54 5 29 40 issubg2 
 |-  ( G e. Grp -> ( |^| S e. ( SubGrp ` G ) <-> ( |^| S C_ ( Base ` G ) /\ |^| S =/= (/) /\ A. x e. |^| S ( A. y e. |^| S ( x ( +g ` G ) y ) e. |^| S /\ ( ( invg ` G ) ` x ) e. |^| S ) ) ) )
55 49 53 54 3syl 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> ( |^| S e. ( SubGrp ` G ) <-> ( |^| S C_ ( Base ` G ) /\ |^| S =/= (/) /\ A. x e. |^| S ( A. y e. |^| S ( x ( +g ` G ) y ) e. |^| S /\ ( ( invg ` G ) ` x ) e. |^| S ) ) ) )
56 11 19 48 55 mpbir3and 
 |-  ( ( S C_ ( SubGrp ` G ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` G ) )