Metamath Proof Explorer

Theorem grpoinvdiv

Description: Inverse of a group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdiv.1 
|- X = ran G
grpdiv.2 
|- N = ( inv ` G )
grpdiv.3 
|- D = ( /g ` G )
Assertion grpoinvdiv 
|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( A D B ) ) = ( B D A ) )

Proof

Step Hyp Ref Expression
1 grpdiv.1 
 |-  X = ran G
2 grpdiv.2 
 |-  N = ( inv ` G )
3 grpdiv.3 
 |-  D = ( /g ` G )
4 1 2 3 grpodivval 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( N ` B ) ) )
5 4 fveq2d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( A D B ) ) = ( N ` ( A G ( N ` B ) ) ) )
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 grpoinvop 
 |-  ( ( G e. GrpOp /\ A e. X /\ ( N ` B ) e. X ) -> ( N ` ( A G ( N ` B ) ) ) = ( ( N ` ( N ` B ) ) G ( N ` A ) ) )
9 7 8 syld3an3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( A G ( N ` B ) ) ) = ( ( N ` ( N ` B ) ) G ( N ` A ) ) )
10 1 2 grpo2inv 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( N ` ( N ` B ) ) = B )
11 10 3adant2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( N ` B ) ) = B )
12 11 oveq1d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` ( N ` B ) ) G ( N ` A ) ) = ( B G ( N ` A ) ) )
13 1 2 3 grpodivval 
 |-  ( ( G e. GrpOp /\ B e. X /\ A e. X ) -> ( B D A ) = ( B G ( N ` A ) ) )
14 13 3com23 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( B D A ) = ( B G ( N ` A ) ) )
15 12 14 eqtr4d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( N ` ( N ` B ) ) G ( N ` A ) ) = ( B D A ) )
16 5 9 15 3eqtrd 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( N ` ( A D B ) ) = ( B D A ) )