Metamath Proof Explorer

Theorem grpoinvid1

Description: The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpinv.1 
|- X = ran G
grpinv.2 
|- U = ( GId ` G )
grpinv.3 
|- N = ( inv ` G )
Assertion grpoinvid1 
|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` A ) = B <-> ( A G B ) = 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 oveq2 
 |-  ( ( N ` A ) = B -> ( A G ( N ` A ) ) = ( A G B ) )
5 4 adantl 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( N ` A ) = B ) -> ( A G ( N ` A ) ) = ( A G B ) )
6 1 2 3 grporinv 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A G ( N ` A ) ) = U )
7 6 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( N ` A ) ) = U )
8 7 adantr 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( N ` A ) = B ) -> ( A G ( N ` A ) ) = U )
9 5 8 eqtr3d 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( N ` A ) = B ) -> ( A G B ) = U )
10 oveq2 
 |-  ( ( A G B ) = U -> ( ( N ` A ) G ( A G B ) ) = ( ( N ` A ) G U ) )
11 10 adantl 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( A G B ) = U ) -> ( ( N ` A ) G ( A G B ) ) = ( ( N ` A ) G U ) )
12 1 2 3 grpolinv 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) G A ) = U )
13 12 oveq1d 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( ( N ` A ) G A ) G B ) = ( U G B ) )
14 13 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( ( N ` A ) G A ) G B ) = ( U G B ) )
15 1 3 grpoinvcl 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. X )
16 15 adantrr 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( N ` A ) e. X )
17 simprl 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> A e. X )
18 simprr 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> B e. X )
19 16 17 18 3jca 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( ( N ` A ) e. X /\ A e. X /\ B e. X ) )
20 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( ( N ` A ) e. X /\ A e. X /\ B e. X ) ) -> ( ( ( N ` A ) G A ) G B ) = ( ( N ` A ) G ( A G B ) ) )
21 19 20 syldan 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( ( ( N ` A ) G A ) G B ) = ( ( N ` A ) G ( A G B ) ) )
22 21 3impb 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( ( N ` A ) G A ) G B ) = ( ( N ` A ) G ( A G B ) ) )
23 14 22 eqtr3d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( U G B ) = ( ( N ` A ) G ( A G B ) ) )
24 1 2 grpolid 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( U G B ) = B )
25 24 3adant2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( U G B ) = B )
26 23 25 eqtr3d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` A ) G ( A G B ) ) = B )
27 26 adantr 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( A G B ) = U ) -> ( ( N ` A ) G ( A G B ) ) = B )
28 1 2 grporid 
 |-  ( ( G e. GrpOp /\ ( N ` A ) e. X ) -> ( ( N ` A ) G U ) = ( N ` A ) )
29 15 28 syldan 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( N ` A ) G U ) = ( N ` A ) )
30 29 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` A ) G U ) = ( N ` A ) )
31 30 adantr 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( A G B ) = U ) -> ( ( N ` A ) G U ) = ( N ` A ) )
32 11 27 31 3eqtr3rd 
 |-  ( ( ( G e. GrpOp /\ A e. X /\ B e. X ) /\ ( A G B ) = U ) -> ( N ` A ) = B )
33 9 32 impbida 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` A ) = B <-> ( A G B ) = U ) )