Theorem ablonncan

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

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

Proof

Step	Hyp	Ref	Expression
1		abldiv.1	⊢ 𝑋 = ran 𝐺
2		abldiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3		id	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
4	3	3anidm12	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
5	1 2	ablodivdiv	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐴 ) 𝐺 𝐵 ) )
6	4 5	sylan2	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐴 ) 𝐺 𝐵 ) )
7	6	3impb	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐴 ) 𝐺 𝐵 ) )
8		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
9		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
10	1 2 9	grpodivid	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = ( GId ‘ 𝐺 ) )
11	8 10	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = ( GId ‘ 𝐺 ) )
12	11	3adant3	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = ( GId ‘ 𝐺 ) )
13	12	oveq1d	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐴 ) 𝐺 𝐵 ) = ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) )
14	1 9	grpolid	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) = 𝐵 )
15	8 14	sylan	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐵 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) = 𝐵 )
16	15	3adant2	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( GId ‘ 𝐺 ) 𝐺 𝐵 ) = 𝐵 )
17	7 13 16	3eqtrd	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐴 𝐷 𝐵 ) ) = 𝐵 )