Metamath Proof Explorer

Theorem issubg3

Description: A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis issubg3.i 
|- I = ( invg ` G )
Assertion issubg3 
|- ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) ) )

Proof

Step Hyp Ref Expression
1 issubg3.i 
 |-  I = ( invg ` G )
2 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
3 2 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S )
4 3 a1i 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) -> ( 0g ` G ) e. S ) )
5 2 subm0cl 
 |-  ( S e. ( SubMnd ` G ) -> ( 0g ` G ) e. S )
6 5 adantr 
 |-  ( ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) -> ( 0g ` G ) e. S )
7 6 a1i 
 |-  ( G e. Grp -> ( ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) -> ( 0g ` G ) e. S ) )
8 ne0i 
 |-  ( ( 0g ` G ) e. S -> S =/= (/) )
9 id 
 |-  ( ( 0g ` G ) e. S -> ( 0g ` G ) e. S )
10 8 9 2thd 
 |-  ( ( 0g ` G ) e. S -> ( S =/= (/) <-> ( 0g ` G ) e. S ) )
11 10 adantl 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( S =/= (/) <-> ( 0g ` G ) e. S ) )
12 r19.26 
 |-  ( A. x e. S ( A. y e. S ( x ( +g ` G ) y ) e. S /\ ( I ` x ) e. S ) <-> ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) )
13 12 a1i 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( A. x e. S ( A. y e. S ( x ( +g ` G ) y ) e. S /\ ( I ` x ) e. S ) <-> ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) ) )
14 11 13 3anbi23d 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( ( S C_ ( Base ` G ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` G ) y ) e. S /\ ( I ` x ) e. S ) ) <-> ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) ) ) )
15 anass 
 |-  ( ( ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S ) /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S ) /\ ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) ) )
16 df-3an 
 |-  ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S ) /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) )
17 16 anbi1i 
 |-  ( ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) <-> ( ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S ) /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) )
18 df-3an 
 |-  ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S ) /\ ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) ) )
19 15 17 18 3bitr4ri 
 |-  ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ ( A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S /\ A. x e. S ( I ` x ) e. S ) ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) )
20 14 19 bitrdi 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( ( S C_ ( Base ` G ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` G ) y ) e. S /\ ( I ` x ) e. S ) ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) ) )
21 eqid 
 |-  ( Base ` G ) = ( Base ` G )
22 eqid 
 |-  ( +g ` G ) = ( +g ` G )
23 21 22 1 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 /\ ( I ` x ) e. S ) ) ) )
24 23 adantr 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( S e. ( SubGrp ` G ) <-> ( S C_ ( Base ` G ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` G ) y ) e. S /\ ( I ` x ) e. S ) ) ) )
25 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
26 21 2 22 issubm 
 |-  ( G e. Mnd -> ( S e. ( SubMnd ` G ) <-> ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) ) )
27 25 26 syl 
 |-  ( G e. Grp -> ( S e. ( SubMnd ` G ) <-> ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) ) )
28 27 anbi1d 
 |-  ( G e. Grp -> ( ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) ) )
29 28 adantr 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) <-> ( ( S C_ ( Base ` G ) /\ ( 0g ` G ) e. S /\ A. x e. S A. y e. S ( x ( +g ` G ) y ) e. S ) /\ A. x e. S ( I ` x ) e. S ) ) )
30 20 24 29 3bitr4d 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. S ) -> ( S e. ( SubGrp ` G ) <-> ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) ) )
31 30 ex 
 |-  ( G e. Grp -> ( ( 0g ` G ) e. S -> ( S e. ( SubGrp ` G ) <-> ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) ) ) )
32 4 7 31 pm5.21ndd 
 |-  ( G e. Grp -> ( S e. ( SubGrp ` G ) <-> ( S e. ( SubMnd ` G ) /\ A. x e. S ( I ` x ) e. S ) ) )