Metamath Proof Explorer

Theorem grponpcan

Description: Cancellation law for group division. ( npcan analog.) (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 grpdivf.1 
 |-  X = ran G
2 grpdivf.3 
 |-  D = ( /g ` G )
3 eqid 
 |-  ( inv ` G ) = ( inv ` G )
4 1 3 2 grpodivval 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) = ( A G ( ( inv ` G ) ` B ) ) )
5 4 oveq1d 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A D B ) G B ) = ( ( A G ( ( inv ` G ) ` B ) ) G B ) )
6 simp1 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> G e. GrpOp )
7 simp2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> A e. X )
8 1 3 grpoinvcl 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( ( inv ` G ) ` B ) e. X )
9 8 3adant2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( inv ` G ) ` B ) e. X )
10 simp3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> B e. X )
11 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ ( ( inv ` G ) ` B ) e. X /\ B e. X ) ) -> ( ( A G ( ( inv ` G ) ` B ) ) G B ) = ( A G ( ( ( inv ` G ) ` B ) G B ) ) )
12 6 7 9 10 11 syl13anc 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A G ( ( inv ` G ) ` B ) ) G B ) = ( A G ( ( ( inv ` G ) ` B ) G B ) ) )
13 eqid 
 |-  ( GId ` G ) = ( GId ` G )
14 1 13 3 grpolinv 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( ( ( inv ` G ) ` B ) G B ) = ( GId ` G ) )
15 14 oveq2d 
 |-  ( ( G e. GrpOp /\ B e. X ) -> ( A G ( ( ( inv ` G ) ` B ) G B ) ) = ( A G ( GId ` G ) ) )
16 15 3adant2 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( ( ( inv ` G ) ` B ) G B ) ) = ( A G ( GId ` G ) ) )
17 1 13 grporid 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A G ( GId ` G ) ) = A )
18 17 3adant3 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( GId ` G ) ) = A )
19 16 18 eqtrd 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G ( ( ( inv ` G ) ` B ) G B ) ) = A )
20 12 19 eqtrd 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A G ( ( inv ` G ) ` B ) ) G B ) = A )
21 5 20 eqtrd 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A D B ) G B ) = A )