Theorem grporndm

Description: A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	grporndm	$$⊢G\in \mathrm{GrpOp}\to \mathrm{ran}G=\mathrm{dom}\mathrm{dom}G$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{ran}G=\mathrm{ran}G$$
2	1	grpofo	$$⊢G\in \mathrm{GrpOp}\to G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G$$
3		fof	$$⊢G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G\to G:\mathrm{ran}G\times \mathrm{ran}G⟶\mathrm{ran}G$$
4	3	fdmd	$$⊢G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G\to \mathrm{dom}G=\mathrm{ran}G\times \mathrm{ran}G$$
5	4	dmeqd	$$⊢G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G\to \mathrm{dom}\mathrm{dom}G=\mathrm{dom}\left(\mathrm{ran}G\times \mathrm{ran}G\right)$$
6		dmxpid	$$⊢\mathrm{dom}\left(\mathrm{ran}G\times \mathrm{ran}G\right)=\mathrm{ran}G$$
7	5 6	syl6req	$$⊢G:\mathrm{ran}G\times \mathrm{ran}G\underset{onto}{⟶}\mathrm{ran}G\to \mathrm{ran}G=\mathrm{dom}\mathrm{dom}G$$
8	2 7	syl	$$⊢G\in \mathrm{GrpOp}\to \mathrm{ran}G=\mathrm{dom}\mathrm{dom}G$$