Theorem grponpcan

Description: Cancellation law for group division. ( npcan analog.) (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdivf.1	⊢ 𝑋 = ran 𝐺
	grpdivf.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion	grponpcan	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		grpdivf.1	⊢ 𝑋 = ran 𝐺
2		grpdivf.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3		eqid	⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
4	1 3 2	grpodivval	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
5	4	oveq1d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) )
6		simp1	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐺 ∈ GrpOp )
7		simp2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
8	1 3	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
9	8	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 )
10		simp3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
11	1	grpoass	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) )
12	6 7 9 10 11	syl13anc	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) = ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) )
13		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
14	1 13 3	grpolinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) = ( GId ‘ 𝐺 ) )
15	14	oveq2d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
16	15	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) = ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) )
17	1 13	grporid	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = 𝐴 )
18	17	3adant3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( GId ‘ 𝐺 ) ) = 𝐴 )
19	16 18	eqtrd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) 𝐺 𝐵 ) ) = 𝐴 )
20	12 19	eqtrd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) 𝐺 𝐵 ) = 𝐴 )
21	5 20	eqtrd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐷 𝐵 ) 𝐺 𝐵 ) = 𝐴 )