Metamath Proof Explorer

Theorem issubg4

Description: A subgroup is a nonempty subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 issubg4.b 
 |-  B = ( Base ` G )
2 issubg4.p 
 |-  .- = ( -g ` G )
3 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 4 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
6 5 ne0d 
 |-  ( S e. ( SubGrp ` G ) -> S =/= (/) )
7 2 subgsubcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ x e. S /\ y e. S ) -> ( x .- y ) e. S )
8 7 3expb 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( x e. S /\ y e. S ) ) -> ( x .- y ) e. S )
9 8 ralrimivva 
 |-  ( S e. ( SubGrp ` G ) -> A. x e. S A. y e. S ( x .- y ) e. S )
10 3 6 9 3jca 
 |-  ( S e. ( SubGrp ` G ) -> ( S C_ B /\ S =/= (/) /\ A. x e. S A. y e. S ( x .- y ) e. S ) )
11 simplrl 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> S C_ B )
12 simplrr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> S =/= (/) )
13 oveq1 
 |-  ( x = ( 0g ` G ) -> ( x .- y ) = ( ( 0g ` G ) .- y ) )
14 13 eleq1d 
 |-  ( x = ( 0g ` G ) -> ( ( x .- y ) e. S <-> ( ( 0g ` G ) .- y ) e. S ) )
15 14 ralbidv 
 |-  ( x = ( 0g ` G ) -> ( A. y e. S ( x .- y ) e. S <-> A. y e. S ( ( 0g ` G ) .- y ) e. S ) )
16 simpr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> A. x e. S A. y e. S ( x .- y ) e. S )
17 simprr 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) -> S =/= (/) )
18 r19.2z 
 |-  ( ( S =/= (/) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> E. x e. S A. y e. S ( x .- y ) e. S )
19 17 18 sylan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> E. x e. S A. y e. S ( x .- y ) e. S )
20 oveq2 
 |-  ( y = x -> ( x .- y ) = ( x .- x ) )
21 20 eleq1d 
 |-  ( y = x -> ( ( x .- y ) e. S <-> ( x .- x ) e. S ) )
22 21 rspcv 
 |-  ( x e. S -> ( A. y e. S ( x .- y ) e. S -> ( x .- x ) e. S ) )
23 22 adantl 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( A. y e. S ( x .- y ) e. S -> ( x .- x ) e. S ) )
24 simprl 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) -> S C_ B )
25 24 sselda 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> x e. B )
26 1 4 2 grpsubid 
 |-  ( ( G e. Grp /\ x e. B ) -> ( x .- x ) = ( 0g ` G ) )
27 26 adantlr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. B ) -> ( x .- x ) = ( 0g ` G ) )
28 25 27 syldan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( x .- x ) = ( 0g ` G ) )
29 28 eleq1d 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( ( x .- x ) e. S <-> ( 0g ` G ) e. S ) )
30 23 29 sylibd 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( A. y e. S ( x .- y ) e. S -> ( 0g ` G ) e. S ) )
31 30 rexlimdva 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) -> ( E. x e. S A. y e. S ( x .- y ) e. S -> ( 0g ` G ) e. S ) )
32 31 imp 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ E. x e. S A. y e. S ( x .- y ) e. S ) -> ( 0g ` G ) e. S )
33 19 32 syldan 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> ( 0g ` G ) e. S )
34 15 16 33 rspcdva 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> A. y e. S ( ( 0g ` G ) .- y ) e. S )
35 1 4 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
36 35 ad2antrr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> ( 0g ` G ) e. B )
37 24 sselda 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> y e. B )
38 eqid 
 |-  ( +g ` G ) = ( +g ` G )
39 eqid 
 |-  ( invg ` G ) = ( invg ` G )
40 1 38 39 2 grpsubval 
 |-  ( ( ( 0g ` G ) e. B /\ y e. B ) -> ( ( 0g ` G ) .- y ) = ( ( 0g ` G ) ( +g ` G ) ( ( invg ` G ) ` y ) ) )
41 36 37 40 syl2anc 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> ( ( 0g ` G ) .- y ) = ( ( 0g ` G ) ( +g ` G ) ( ( invg ` G ) ` y ) ) )
42 simpll 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> G e. Grp )
43 1 39 grpinvcl 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
44 42 37 43 syl2anc 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> ( ( invg ` G ) ` y ) e. B )
45 1 38 4 grplid 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` y ) e. B ) -> ( ( 0g ` G ) ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( ( invg ` G ) ` y ) )
46 42 44 45 syl2anc 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> ( ( 0g ` G ) ( +g ` G ) ( ( invg ` G ) ` y ) ) = ( ( invg ` G ) ` y ) )
47 41 46 eqtrd 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> ( ( 0g ` G ) .- y ) = ( ( invg ` G ) ` y ) )
48 47 eleq1d 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ y e. S ) -> ( ( ( 0g ` G ) .- y ) e. S <-> ( ( invg ` G ) ` y ) e. S ) )
49 48 ralbidva 
 |-  ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) -> ( A. y e. S ( ( 0g ` G ) .- y ) e. S <-> A. y e. S ( ( invg ` G ) ` y ) e. S ) )
50 49 adantr 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> ( A. y e. S ( ( 0g ` G ) .- y ) e. S <-> A. y e. S ( ( invg ` G ) ` y ) e. S ) )
51 34 50 mpbid 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> A. y e. S ( ( invg ` G ) ` y ) e. S )
52 fveq2 
 |-  ( y = z -> ( ( invg ` G ) ` y ) = ( ( invg ` G ) ` z ) )
53 52 eleq1d 
 |-  ( y = z -> ( ( ( invg ` G ) ` y ) e. S <-> ( ( invg ` G ) ` z ) e. S ) )
54 53 rspccva 
 |-  ( ( A. y e. S ( ( invg ` G ) ` y ) e. S /\ z e. S ) -> ( ( invg ` G ) ` z ) e. S )
55 54 ad2ant2l 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> ( ( invg ` G ) ` z ) e. S )
56 oveq2 
 |-  ( y = ( ( invg ` G ) ` z ) -> ( x .- y ) = ( x .- ( ( invg ` G ) ` z ) ) )
57 56 eleq1d 
 |-  ( y = ( ( invg ` G ) ` z ) -> ( ( x .- y ) e. S <-> ( x .- ( ( invg ` G ) ` z ) ) e. S ) )
58 57 rspcv 
 |-  ( ( ( invg ` G ) ` z ) e. S -> ( A. y e. S ( x .- y ) e. S -> ( x .- ( ( invg ` G ) ` z ) ) e. S ) )
59 55 58 syl 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> ( A. y e. S ( x .- y ) e. S -> ( x .- ( ( invg ` G ) ` z ) ) e. S ) )
60 simplll 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> G e. Grp )
61 simplrl 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) -> S C_ B )
62 61 adantr 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> S C_ B )
63 simprl 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> x e. S )
64 62 63 sseldd 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> x e. B )
65 simprr 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> z e. S )
66 62 65 sseldd 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> z e. B )
67 1 38 2 39 60 64 66 grpsubinv 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> ( x .- ( ( invg ` G ) ` z ) ) = ( x ( +g ` G ) z ) )
68 67 eleq1d 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> ( ( x .- ( ( invg ` G ) ` z ) ) e. S <-> ( x ( +g ` G ) z ) e. S ) )
69 59 68 sylibd 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ ( x e. S /\ z e. S ) ) -> ( A. y e. S ( x .- y ) e. S -> ( x ( +g ` G ) z ) e. S ) )
70 69 anassrs 
 |-  ( ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ x e. S ) /\ z e. S ) -> ( A. y e. S ( x .- y ) e. S -> ( x ( +g ` G ) z ) e. S ) )
71 70 ralrimdva 
 |-  ( ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) /\ x e. S ) -> ( A. y e. S ( x .- y ) e. S -> A. z e. S ( x ( +g ` G ) z ) e. S ) )
72 71 ralimdva 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) -> ( A. x e. S A. y e. S ( x .- y ) e. S -> A. x e. S A. z e. S ( x ( +g ` G ) z ) e. S ) )
73 72 impancom 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> ( A. y e. S ( ( invg ` G ) ` y ) e. S -> A. x e. S A. z e. S ( x ( +g ` G ) z ) e. S ) )
74 51 73 mpd 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> A. x e. S A. z e. S ( x ( +g ` G ) z ) e. S )
75 oveq1 
 |-  ( x = y -> ( x ( +g ` G ) z ) = ( y ( +g ` G ) z ) )
76 75 eleq1d 
 |-  ( x = y -> ( ( x ( +g ` G ) z ) e. S <-> ( y ( +g ` G ) z ) e. S ) )
77 76 ralbidv 
 |-  ( x = y -> ( A. z e. S ( x ( +g ` G ) z ) e. S <-> A. z e. S ( y ( +g ` G ) z ) e. S ) )
78 77 cbvralvw 
 |-  ( A. x e. S A. z e. S ( x ( +g ` G ) z ) e. S <-> A. y e. S A. z e. S ( y ( +g ` G ) z ) e. S )
79 74 78 sylib 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> A. y e. S A. z e. S ( y ( +g ` G ) z ) e. S )
80 r19.26 
 |-  ( A. y e. S ( A. z e. S ( y ( +g ` G ) z ) e. S /\ ( ( invg ` G ) ` y ) e. S ) <-> ( A. y e. S A. z e. S ( y ( +g ` G ) z ) e. S /\ A. y e. S ( ( invg ` G ) ` y ) e. S ) )
81 79 51 80 sylanbrc 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> A. y e. S ( A. z e. S ( y ( +g ` G ) z ) e. S /\ ( ( invg ` G ) ` y ) e. S ) )
82 11 12 81 3jca 
 |-  ( ( ( G e. Grp /\ ( S C_ B /\ S =/= (/) ) ) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> ( S C_ B /\ S =/= (/) /\ A. y e. S ( A. z e. S ( y ( +g ` G ) z ) e. S /\ ( ( invg ` G ) ` y ) e. S ) ) )
83 82 exp42 
 |-  ( G e. Grp -> ( S C_ B -> ( S =/= (/) -> ( A. x e. S A. y e. S ( x .- y ) e. S -> ( S C_ B /\ S =/= (/) /\ A. y e. S ( A. z e. S ( y ( +g ` G ) z ) e. S /\ ( ( invg ` G ) ` y ) e. S ) ) ) ) ) )
84 83 3impd 
 |-  ( G e. Grp -> ( ( S C_ B /\ S =/= (/) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> ( S C_ B /\ S =/= (/) /\ A. y e. S ( A. z e. S ( y ( +g ` G ) z ) e. S /\ ( ( invg ` G ) ` y ) e. S ) ) ) )
85 1 38 39 issubg2 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ S =/= (/) /\ A. y e. S ( A. z e. S ( y ( +g ` G ) z ) e. S /\ ( ( invg ` G ) ` y ) e. S ) ) ) )
86 84 85 sylibrd 
 |-  ( G e. Grp -> ( ( S C_ B /\ S =/= (/) /\ A. x e. S A. y e. S ( x .- y ) e. S ) -> S e. ( SubGrp ` G ) ) )
87 10 86 impbid2 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S C_ B /\ S =/= (/) /\ A. x e. S A. y e. S ( x .- y ) e. S ) ) )