Metamath Proof Explorer

Theorem subginv

Description: The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses subg0.h 
|- H = ( G |`s S )
subginv.i 
|- I = ( invg ` G )
subginv.j 
|- J = ( invg ` H )
Assertion subginv 
|- ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( I ` X ) = ( J ` X ) )

Proof

Step Hyp Ref Expression
1 subg0.h 
 |-  H = ( G |`s S )
2 subginv.i 
 |-  I = ( invg ` G )
3 subginv.j 
 |-  J = ( invg ` H )
4 1 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> H e. Grp )
5 1 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` H ) )
6 5 eleq2d 
 |-  ( S e. ( SubGrp ` G ) -> ( X e. S <-> X e. ( Base ` H ) ) )
7 6 biimpa 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> X e. ( Base ` H ) )
8 eqid 
 |-  ( Base ` H ) = ( Base ` H )
9 eqid 
 |-  ( +g ` H ) = ( +g ` H )
10 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
11 8 9 10 3 grprinv 
 |-  ( ( H e. Grp /\ X e. ( Base ` H ) ) -> ( X ( +g ` H ) ( J ` X ) ) = ( 0g ` H ) )
12 4 7 11 syl2an2r 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( X ( +g ` H ) ( J ` X ) ) = ( 0g ` H ) )
13 eqid 
 |-  ( +g ` G ) = ( +g ` G )
14 1 13 ressplusg 
 |-  ( S e. ( SubGrp ` G ) -> ( +g ` G ) = ( +g ` H ) )
15 14 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( +g ` G ) = ( +g ` H ) )
16 15 oveqd 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( X ( +g ` G ) ( J ` X ) ) = ( X ( +g ` H ) ( J ` X ) ) )
17 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
18 1 17 subg0 
 |-  ( S e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
19 18 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( 0g ` G ) = ( 0g ` H ) )
20 12 16 19 3eqtr4d 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( X ( +g ` G ) ( J ` X ) ) = ( 0g ` G ) )
21 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
22 21 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> G e. Grp )
23 eqid 
 |-  ( Base ` G ) = ( Base ` G )
24 23 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) )
25 24 sselda 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> X e. ( Base ` G ) )
26 8 3 grpinvcl 
 |-  ( ( H e. Grp /\ X e. ( Base ` H ) ) -> ( J ` X ) e. ( Base ` H ) )
27 26 ex 
 |-  ( H e. Grp -> ( X e. ( Base ` H ) -> ( J ` X ) e. ( Base ` H ) ) )
28 4 27 syl 
 |-  ( S e. ( SubGrp ` G ) -> ( X e. ( Base ` H ) -> ( J ` X ) e. ( Base ` H ) ) )
29 5 eleq2d 
 |-  ( S e. ( SubGrp ` G ) -> ( ( J ` X ) e. S <-> ( J ` X ) e. ( Base ` H ) ) )
30 28 6 29 3imtr4d 
 |-  ( S e. ( SubGrp ` G ) -> ( X e. S -> ( J ` X ) e. S ) )
31 30 imp 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( J ` X ) e. S )
32 24 sselda 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( J ` X ) e. S ) -> ( J ` X ) e. ( Base ` G ) )
33 31 32 syldan 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( J ` X ) e. ( Base ` G ) )
34 23 13 17 2 grpinvid1 
 |-  ( ( G e. Grp /\ X e. ( Base ` G ) /\ ( J ` X ) e. ( Base ` G ) ) -> ( ( I ` X ) = ( J ` X ) <-> ( X ( +g ` G ) ( J ` X ) ) = ( 0g ` G ) ) )
35 22 25 33 34 syl3anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( ( I ` X ) = ( J ` X ) <-> ( X ( +g ` G ) ( J ` X ) ) = ( 0g ` G ) ) )
36 20 35 mpbird 
 |-  ( ( S e. ( SubGrp ` G ) /\ X e. S ) -> ( I ` X ) = ( J ` X ) )