Theorem grpoinvdiv

Description: Inverse of a group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		grpdiv.1	⊢ 𝑋 = ran 𝐺
2		grpdiv.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
3		grpdiv.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
4	1 2 3	grpodivval	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )
5	4	fveq2d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ) )
6	1 2	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
7	6	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 )
8	1 2	grpoinvop	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
9	7 8	syld3an3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ) = ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
10	1 2	grpo2inv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) = 𝐵 )
11	10	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) = 𝐵 )
12	11	oveq1d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐵 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
13	1 2 3	grpodivval	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐵 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
14	13	3com23	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐵 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
15	12 14	eqtr4d	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝐵 ) ) 𝐺 ( 𝑁 ‘ 𝐴 ) ) = ( 𝐵 𝐷 𝐴 ) )
16	5 9 15	3eqtrd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐷 𝐵 ) ) = ( 𝐵 𝐷 𝐴 ) )