Theorem grpodivid

Description: Division of a group member by itself. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdivf.1	|- X = ran G
	grpdivf.3	|- D = ( /g ` G )
	grpdivid.3	|- U = ( GId ` G )
Assertion	grpodivid	|- ( ( G e. GrpOp /\ A e. X ) -> ( A D A ) = U )

Proof

Step	Hyp	Ref	Expression
1		grpdivf.1	|- X = ran G
2		grpdivf.3	|- D = ( /g ` G )
3		grpdivid.3	|- U = ( GId ` G )
4		eqid	|- ( inv ` G ) = ( inv ` G )
5	1 4 2	grpodivval	|- ( ( G e. GrpOp /\ A e. X /\ A e. X ) -> ( A D A ) = ( A G ( ( inv ` G ) ` A ) ) )
6	5	3anidm23	|- ( ( G e. GrpOp /\ A e. X ) -> ( A D A ) = ( A G ( ( inv ` G ) ` A ) ) )
7	1 3 4	grporinv	|- ( ( G e. GrpOp /\ A e. X ) -> ( A G ( ( inv ` G ) ` A ) ) = U )
8	6 7	eqtrd	|- ( ( G e. GrpOp /\ A e. X ) -> ( A D A ) = U )