Metamath Proof Explorer

Theorem ablo4

Description: Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 
|- X = ran G
Assertion ablo4 
|- ( ( G e. AbelOp /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )

Proof

Step Hyp Ref Expression
1 ablcom.1 
 |-  X = ran G
2 simprll 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> A e. X )
3 simprlr 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> B e. X )
4 simprrl 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> C e. X )
5 2 3 4 3jca 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( A e. X /\ B e. X /\ C e. X ) )
6 1 ablo32 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
7 5 6 syldan 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )
8 7 oveq1d 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A G B ) G C ) G D ) = ( ( ( A G C ) G B ) G D ) )
9 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
10 1 grpocl 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
11 10 3expb 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( A G B ) e. X )
12 11 adantrr 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( A G B ) e. X )
13 simprrl 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> C e. X )
14 simprrr 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> D e. X )
15 12 13 14 3jca 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A G B ) e. X /\ C e. X /\ D e. X ) )
16 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( ( A G B ) e. X /\ C e. X /\ D e. X ) ) -> ( ( ( A G B ) G C ) G D ) = ( ( A G B ) G ( C G D ) ) )
17 15 16 syldan 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A G B ) G C ) G D ) = ( ( A G B ) G ( C G D ) ) )
18 9 17 sylan 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A G B ) G C ) G D ) = ( ( A G B ) G ( C G D ) ) )
19 1 grpocl 
 |-  ( ( G e. GrpOp /\ A e. X /\ C e. X ) -> ( A G C ) e. X )
20 19 3expb 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X ) ) -> ( A G C ) e. X )
21 20 adantrlr 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ C e. X ) ) -> ( A G C ) e. X )
22 21 adantrrr 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( A G C ) e. X )
23 simprlr 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> B e. X )
24 22 23 14 3jca 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A G C ) e. X /\ B e. X /\ D e. X ) )
25 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( ( A G C ) e. X /\ B e. X /\ D e. X ) ) -> ( ( ( A G C ) G B ) G D ) = ( ( A G C ) G ( B G D ) ) )
26 24 25 syldan 
 |-  ( ( G e. GrpOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A G C ) G B ) G D ) = ( ( A G C ) G ( B G D ) ) )
27 9 26 sylan 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( ( A G C ) G B ) G D ) = ( ( A G C ) G ( B G D ) ) )
28 8 18 27 3eqtr3d 
 |-  ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )
29 28 3impb 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X ) /\ ( C e. X /\ D e. X ) ) -> ( ( A G B ) G ( C G D ) ) = ( ( A G C ) G ( B G D ) ) )