This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ablonnncan1

Description: Cancellation law for group division. ( nnncan1 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 ablonnncan1 
|- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D ( A D C ) ) = ( C D B ) )

Proof

Step Hyp Ref Expression
1 abldiv.1 
 |-  X = ran G
2 abldiv.3 
 |-  D = ( /g ` G )
3 simpr1 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X )
4 simpr2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X )
5 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
6 1 2 grpodivcl 
 |-  ( ( G e. GrpOp /\ A e. X /\ C e. X ) -> ( A D C ) e. X )
7 5 6 syl3an1 
 |-  ( ( G e. AbelOp /\ A e. X /\ C e. X ) -> ( A D C ) e. X )
8 7 3adant3r2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D C ) e. X )
9 3 4 8 3jca 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A e. X /\ B e. X /\ ( A D C ) e. X ) )
10 1 2 ablodiv32 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ ( A D C ) e. X ) ) -> ( ( A D B ) D ( A D C ) ) = ( ( A D ( A D C ) ) D B ) )
11 9 10 syldan 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D ( A D C ) ) = ( ( A D ( A D C ) ) D B ) )
12 1 2 ablonncan 
 |-  ( ( G e. AbelOp /\ A e. X /\ C e. X ) -> ( A D ( A D C ) ) = C )
13 12 3adant3r2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D ( A D C ) ) = C )
14 13 oveq1d 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D ( A D C ) ) D B ) = ( C D B ) )
15 11 14 eqtrd 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D ( A D C ) ) = ( C D B ) )