Metamath Proof Explorer

Theorem grpoinvop

Description: The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of Herstein p. 55. (Contributed by NM, 27-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grpasscan1.1 
|- X = ran G
grpasscan1.2 
|- N = ( inv ` G )
Assertion grpoinvop 
|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( A G B ) ) = ( ( N ` B ) G ( N ` A ) ) )

Proof

Step Hyp Ref Expression
1 grpasscan1.1 
 |-  X = ran G
2 grpasscan1.2 
 |-  N = ( inv ` G )
3 simp1 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> G e. GrpOp )
4 simp2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> A e. X )
5 simp3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> B e. X )
6 1 2 grpoinvcl 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( N ` B ) e. X )
7 6 3adant2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` B ) e. X )
8 1 2 grpoinvcl 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( N ` A ) e. X )
9 8 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` A ) e. X )
10 1 grpocl 
 |-  ( ( G e. GrpOp /\ ( N ` B ) e. X /\ ( N ` A ) e. X ) -> ( ( N ` B ) G ( N ` A ) ) e. X )
11 3 7 9 10 syl3anc 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` B ) G ( N ` A ) ) e. X )
12 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ ( ( N ` B ) G ( N ` A ) ) e. X ) ) -> ( ( A G B ) G ( ( N ` B ) G ( N ` A ) ) ) = ( A G ( B G ( ( N ` B ) G ( N ` A ) ) ) ) )
13 3 4 5 11 12 syl13anc 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A G B ) G ( ( N ` B ) G ( N ` A ) ) ) = ( A G ( B G ( ( N ` B ) G ( N ` A ) ) ) ) )
14 eqid 
 |-  ( GId ` G ) = ( GId ` G )
15 1 14 2 grporinv 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( B G ( N ` B ) ) = ( GId ` G ) )
16 15 3adant2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( B G ( N ` B ) ) = ( GId ` G ) )
17 16 oveq1d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( B G ( N ` B ) ) G ( N ` A ) ) = ( ( GId ` G ) G ( N ` A ) ) )
18 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ ( N ` B ) e. X /\ ( N ` A ) e. X ) ) -> ( ( B G ( N ` B ) ) G ( N ` A ) ) = ( B G ( ( N ` B ) G ( N ` A ) ) ) )
19 3 5 7 9 18 syl13anc 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( B G ( N ` B ) ) G ( N ` A ) ) = ( B G ( ( N ` B ) G ( N ` A ) ) ) )
20 1 14 grpolid 
 |-  ( ( G e. GrpOp /\ ( N ` A ) e. X ) -> ( ( GId ` G ) G ( N ` A ) ) = ( N ` A ) )
21 8 20 syldan 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( GId ` G ) G ( N ` A ) ) = ( N ` A ) )
22 21 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( GId ` G ) G ( N ` A ) ) = ( N ` A ) )
23 17 19 22 3eqtr3d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( B G ( ( N ` B ) G ( N ` A ) ) ) = ( N ` A ) )
24 23 oveq2d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( B G ( ( N ` B ) G ( N ` A ) ) ) ) = ( A G ( N ` A ) ) )
25 1 14 2 grporinv 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A G ( N ` A ) ) = ( GId ` G ) )
26 25 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( N ` A ) ) = ( GId ` G ) )
27 13 24 26 3eqtrd 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A G B ) G ( ( N ` B ) G ( N ` A ) ) ) = ( GId ` G ) )
28 1 grpocl 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
29 1 14 2 grpoinvid1 
 |-  ( ( G e. GrpOp /\ ( A G B ) e. X /\ ( ( N ` B ) G ( N ` A ) ) e. X ) -> ( ( N ` ( A G B ) ) = ( ( N ` B ) G ( N ` A ) ) <-> ( ( A G B ) G ( ( N ` B ) G ( N ` A ) ) ) = ( GId ` G ) ) )
30 3 28 11 29 syl3anc 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) = ( ( N ` B ) G ( N ` A ) ) <-> ( ( A G B ) G ( ( N ` B ) G ( N ` A ) ) ) = ( GId ` G ) ) )
31 27 30 mpbird 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( A G B ) ) = ( ( N ` B ) G ( N ` A ) ) )