Metamath Proof Explorer

Theorem grpoinvid2

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