Theorem ablodivdiv

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

	Ref	Expression
Hypotheses	abldiv.1	⊢ 𝑋 = ran 𝐺
	abldiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion	ablodivdiv	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		abldiv.1	⊢ 𝑋 = ran 𝐺
2		abldiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
4	1 2	grpodivdiv	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) )
5	3 4	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) )
6		3ancomb	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
7	1 2	grpomuldivass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) )
8	3 7	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) )
9	1 2	ablomuldiv	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐶 ) 𝐷 𝐵 ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐶 ) )
10	8 9	eqtr3d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐶 ) )
11	6 10	sylan2b	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 ( 𝐶 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐶 ) )
12	5 11	eqtrd	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐵 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐶 ) )