# Metamath Proof Explorer

## 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}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}$
3 fof ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}\to {G}:\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}$
4 3 fdmd ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}\to \mathrm{dom}{G}=\mathrm{ran}{G}×\mathrm{ran}{G}$
5 4 dmeqd ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}\to \mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\left(\mathrm{ran}{G}×\mathrm{ran}{G}\right)$
6 dmxpid ${⊢}\mathrm{dom}\left(\mathrm{ran}{G}×\mathrm{ran}{G}\right)=\mathrm{ran}{G}$
7 5 6 syl6req ${⊢}{G}:\mathrm{ran}{G}×\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}$