Theorem ablonnncan1

Description: Cancellation law for group division. ( nnncan1 analog.) (Contributed by NM, 7-Mar-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		abldiv.1	⊢ 𝑋 = ran 𝐺
2		abldiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3		simpr1	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
4		simpr2	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
5		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
6	1 2	grpodivcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
7	5 6	syl3an1	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
8	7	3adant3r2	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 )
9	3 4 8	3jca	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ) )
10	1 2	ablodiv32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 ( 𝐴 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 ( 𝐴 𝐷 𝐶 ) ) 𝐷 𝐵 ) )
11	9 10	syldan	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 ( 𝐴 𝐷 𝐶 ) ) = ( ( 𝐴 𝐷 ( 𝐴 𝐷 𝐶 ) ) 𝐷 𝐵 ) )
12	1 2	ablonncan	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐴 𝐷 𝐶 ) ) = 𝐶 )
13	12	3adant3r2	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐴 𝐷 𝐶 ) ) = 𝐶 )
14	13	oveq1d	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 ( 𝐴 𝐷 𝐶 ) ) 𝐷 𝐵 ) = ( 𝐶 𝐷 𝐵 ) )
15	11 14	eqtrd	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) 𝐷 ( 𝐴 𝐷 𝐶 ) ) = ( 𝐶 𝐷 𝐵 ) )