Metamath Proof Explorer

Theorem ablonncan

Description: Cancellation law for group division. ( nncan analog.) (Contributed by NM, 7-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses abldiv.1 
|- X = ran G
abldiv.3 
|- D = ( /g ` G )
Assertion ablonncan 
|- ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A D ( A D B ) ) = B )

Proof

Step Hyp Ref Expression
1 abldiv.1 
 |-  X = ran G
2 abldiv.3 
 |-  D = ( /g ` G )
3 id 
 |-  ( ( A e. X /\ A e. X /\ B e. X ) -> ( A e. X /\ A e. X /\ B e. X ) )
4 3 3anidm12 
 |-  ( ( A e. X /\ B e. X ) -> ( A e. X /\ A e. X /\ B e. X ) )
5 1 2 ablodivdiv 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ A e. X /\ B e. X ) ) -> ( A D ( A D B ) ) = ( ( A D A ) G B ) )
6 4 5 sylan2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X ) ) -> ( A D ( A D B ) ) = ( ( A D A ) G B ) )
7 6 3impb 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A D ( A D B ) ) = ( ( A D A ) G B ) )
8 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
9 eqid 
 |-  ( GId ` G ) = ( GId ` G )
10 1 2 9 grpodivid 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A D A ) = ( GId ` G ) )
11 8 10 sylan 
 |-  ( ( G e. AbelOp /\ A e. X ) -> ( A D A ) = ( GId ` G ) )
12 11 3adant3 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A D A ) = ( GId ` G ) )
13 12 oveq1d 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( ( A D A ) G B ) = ( ( GId ` G ) G B ) )
14 1 9 grpolid 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( ( GId ` G ) G B ) = B )
15 8 14 sylan 
 |-  ( ( G e. AbelOp /\ B e. X ) -> ( ( GId ` G ) G B ) = B )
16 15 3adant2 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( ( GId ` G ) G B ) = B )
17 7 13 16 3eqtrd 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A D ( A D B ) ) = B )