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