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

Metamath Proof Explorer

Theorem ablomuldiv

Description: Law for group multiplication and division. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 abldiv.1 
 |-  X = ran G
2 abldiv.3 
 |-  D = ( /g ` G )
3 1 ablocom 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )
4 3 3adant3r3 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A G B ) = ( B G A ) )
5 4 oveq1d 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) D C ) = ( ( B G A ) D C ) )
6 3ancoma 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) <-> ( B e. X /\ A e. X /\ C e. X ) )
7 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
8 1 2 grpomuldivass 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ A e. X /\ C e. X ) ) -> ( ( B G A ) D C ) = ( B G ( A D C ) ) )
9 7 8 sylan 
 |-  ( ( G e. AbelOp /\ ( B e. X /\ A e. X /\ C e. X ) ) -> ( ( B G A ) D C ) = ( B G ( A D C ) ) )
10 6 9 sylan2b 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( B G A ) D C ) = ( B G ( A D C ) ) )
11 simpr2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X )
12 1 2 grpodivcl 
 |-  ( ( G e. GrpOp /\ A e. X /\ C e. X ) -> ( A D C ) e. X )
13 7 12 syl3an1 
 |-  ( ( G e. AbelOp /\ A e. X /\ C e. X ) -> ( A D C ) e. X )
14 13 3adant3r2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D C ) e. X )
15 11 14 jca 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B e. X /\ ( A D C ) e. X ) )
16 1 ablocom 
 |-  ( ( G e. AbelOp /\ B e. X /\ ( A D C ) e. X ) -> ( B G ( A D C ) ) = ( ( A D C ) G B ) )
17 16 3expb 
 |-  ( ( G e. AbelOp /\ ( B e. X /\ ( A D C ) e. X ) ) -> ( B G ( A D C ) ) = ( ( A D C ) G B ) )
18 15 17 syldan 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B G ( A D C ) ) = ( ( A D C ) G B ) )
19 5 10 18 3eqtrd 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) D C ) = ( ( A D C ) G B ) )