Theorem grpodivinv

Description: Group division by an inverse. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdiv.1	⊢ 𝑋 = ran 𝐺
	grpdiv.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
	grpdiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion	grpodivinv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 𝐺 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		grpdiv.1	⊢ 𝑋 = ran 𝐺
2		grpdiv.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
3		grpdiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
4	1 2	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
5	4	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
6	1 2 3	grpodivval	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) ) )
7	5 6	syld3an3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) ) )
8	1 2	grpo2inv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) = 𝐵 )
9	8	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) = 𝐵 )
10	9	oveq2d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) ) = ( 𝐴 𝐺 𝐵 ) )
11	7 10	eqtrd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 𝐺 𝐵 ) )