Metamath Proof Explorer

Theorem ablodivdiv4

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

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

Proof

Step Hyp Ref Expression
1 abldiv.1 
 |-  X = ran G
2 abldiv.3 
 |-  D = ( /g ` G )
3 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
4 simpl 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. GrpOp )
5 1 2 grpodivcl 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) e. X )
6 5 3adant3r3 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) e. X )
7 simpr3 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> C e. X )
8 eqid 
 |-  ( inv ` G ) = ( inv ` G )
9 1 8 2 grpodivval 
 |-  ( ( G e. GrpOp /\ ( A D B ) e. X /\ C e. X ) -> ( ( A D B ) D C ) = ( ( A D B ) G ( ( inv ` G ) ` C ) ) )
10 4 6 7 9 syl3anc 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D C ) = ( ( A D B ) G ( ( inv ` G ) ` C ) ) )
11 3 10 sylan 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D C ) = ( ( A D B ) G ( ( inv ` G ) ` C ) ) )
12 simpr1 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X )
13 simpr2 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X )
14 simp3 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> C e. X )
15 1 8 grpoinvcl 
 |-  ( ( G e. GrpOp /\ C e. X ) -> ( ( inv ` G ) ` C ) e. X )
16 3 14 15 syl2an 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( inv ` G ) ` C ) e. X )
17 12 13 16 3jca 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A e. X /\ B e. X /\ ( ( inv ` G ) ` C ) e. X ) )
18 1 2 ablodivdiv 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ ( ( inv ` G ) ` C ) e. X ) ) -> ( A D ( B D ( ( inv ` G ) ` C ) ) ) = ( ( A D B ) G ( ( inv ` G ) ` C ) ) )
19 17 18 syldan 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D ( B D ( ( inv ` G ) ` C ) ) ) = ( ( A D B ) G ( ( inv ` G ) ` C ) ) )
20 1 8 2 grpodivinv 
 |-  ( ( G e. GrpOp /\ B e. X /\ C e. X ) -> ( B D ( ( inv ` G ) ` C ) ) = ( B G C ) )
21 3 20 syl3an1 
 |-  ( ( G e. AbelOp /\ B e. X /\ C e. X ) -> ( B D ( ( inv ` G ) ` C ) ) = ( B G C ) )
22 21 3adant3r1 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B D ( ( inv ` G ) ` C ) ) = ( B G C ) )
23 22 oveq2d 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D ( B D ( ( inv ` G ) ` C ) ) ) = ( A D ( B G C ) ) )
24 11 19 23 3eqtr2d 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D B ) D C ) = ( A D ( B G C ) ) )