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 ) )