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=\mathrm{ran}G$$
	grpdivf.3	$$⊢D={/}_g\left(G\right)$$
	grpdivid.3	$$⊢U=\mathrm{GId}\left(G\right)$$
Assertion	grpodivid	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to ADA=U$$

Proof

Step	Hyp	Ref	Expression
1		grpdivf.1	$$⊢X=\mathrm{ran}G$$
2		grpdivf.3	$$⊢D={/}_g\left(G\right)$$
3		grpdivid.3	$$⊢U=\mathrm{GId}\left(G\right)$$
4		eqid	$$⊢\mathrm{inv}\left(G\right)=\mathrm{inv}\left(G\right)$$
5	1 4 2	grpodivval	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\wedge A\in X\right)\to ADA=AG\mathrm{inv}\left(G\right)\left(A\right)$$
6	5	3anidm23	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to ADA=AG\mathrm{inv}\left(G\right)\left(A\right)$$
7	1 3 4	grporinv	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to AG\mathrm{inv}\left(G\right)\left(A\right)=U$$
8	6 7	eqtrd	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to ADA=U$$