Theorem ablomuldiv

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

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

Proof

Step	Hyp	Ref	Expression
1		abldiv.1	⊢ 𝑋 = ran 𝐺
2		abldiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3	1	ablocom	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) )
4	3	3adant3r3	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐵 𝐺 𝐴 ) )
5	4	oveq1d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐵 𝐺 𝐴 ) 𝐷 𝐶 ) )
6		3ancoma	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) )
7		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
8	1 2	grpomuldivass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 𝐺 𝐴 ) 𝐷 𝐶 ) = ( 𝐵 𝐺 ( 𝐴 𝐷 𝐶 ) ) )
9	7 8	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 𝐺 𝐴 ) 𝐷 𝐶 ) = ( 𝐵 𝐺 ( 𝐴 𝐷 𝐶 ) ) )
10	6 9	sylan2b	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 𝐺 𝐴 ) 𝐷 𝐶 ) = ( 𝐵 𝐺 ( 𝐴 𝐷 𝐶 ) ) )
11		simpr2	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
12	1 2	grpodivcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
13	7 12	syl3an1	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
14	13	3adant3r2	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
15	11 14	jca	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ) )
16	1	ablocom	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( 𝐴 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )
17	16	3expb	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ) ) → ( 𝐵 𝐺 ( 𝐴 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )
18	15 17	syldan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐺 ( 𝐴 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )
19	5 10 18	3eqtrd	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐷 𝐶 ) = ( ( 𝐴 𝐷 𝐶 ) 𝐺 𝐵 ) )