This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpoinv

Description: The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpinv.1 
|- X = ran G
grpinv.2 
|- U = ( GId ` G )
grpinv.3 
|- N = ( inv ` G )
Assertion grpoinv 
|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) )

Proof

Step Hyp Ref Expression
1 grpinv.1 
 |-  X = ran G
2 grpinv.2 
 |-  U = ( GId ` G )
3 grpinv.3 
 |-  N = ( inv ` G )
4 1 2 3 grpoinvval 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) = ( iota_ y e. X ( y G A ) = U ) )
5 1 2 grpoinveu 
 |-  ( ( G e. GrpOp /\ A e. X ) -> E! y e. X ( y G A ) = U )
6 riotacl2 
 |-  ( E! y e. X ( y G A ) = U -> ( iota_ y e. X ( y G A ) = U ) e. { y e. X | ( y G A ) = U } )
7 5 6 syl 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( iota_ y e. X ( y G A ) = U ) e. { y e. X | ( y G A ) = U } )
8 4 7 eqeltrd 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. { y e. X | ( y G A ) = U } )
9 simpl 
 |-  ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U )
10 9 rgenw 
 |-  A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U )
11 10 a1i 
 |-  ( ( G e. GrpOp /\ A e. X ) -> A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U ) )
12 1 2 grpoidinv2 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )
13 12 simprd 
 |-  ( ( G e. GrpOp /\ A e. X ) -> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) )
14 11 13 5 3jca 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) /\ E! y e. X ( y G A ) = U ) )
15 reupick2 
 |-  ( ( ( A. y e. X ( ( ( y G A ) = U /\ ( A G y ) = U ) -> ( y G A ) = U ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) /\ E! y e. X ( y G A ) = U ) /\ y e. X ) -> ( ( y G A ) = U <-> ( ( y G A ) = U /\ ( A G y ) = U ) ) )
16 14 15 sylan 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( ( y G A ) = U <-> ( ( y G A ) = U /\ ( A G y ) = U ) ) )
17 16 rabbidva 
 |-  ( ( G e. GrpOp /\ A e. X ) -> { y e. X | ( y G A ) = U } = { y e. X | ( ( y G A ) = U /\ ( A G y ) = U ) } )
18 8 17 eleqtrd 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. { y e. X | ( ( y G A ) = U /\ ( A G y ) = U ) } )
19 oveq1 
 |-  ( y = ( N ` A ) -> ( y G A ) = ( ( N ` A ) G A ) )
20 19 eqeq1d 
 |-  ( y = ( N ` A ) -> ( ( y G A ) = U <-> ( ( N ` A ) G A ) = U ) )
21 oveq2 
 |-  ( y = ( N ` A ) -> ( A G y ) = ( A G ( N ` A ) ) )
22 21 eqeq1d 
 |-  ( y = ( N ` A ) -> ( ( A G y ) = U <-> ( A G ( N ` A ) ) = U ) )
23 20 22 anbi12d 
 |-  ( y = ( N ` A ) -> ( ( ( y G A ) = U /\ ( A G y ) = U ) <-> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) ) )
24 23 elrab 
 |-  ( ( N ` A ) e. { y e. X | ( ( y G A ) = U /\ ( A G y ) = U ) } <-> ( ( N ` A ) e. X /\ ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) ) )
25 18 24 sylib 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) e. X /\ ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) ) )
26 25 simprd 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G A ) = U /\ ( A G ( N ` A ) ) = U ) )