# Metamath Proof Explorer

## Theorem ghomidOLD

Description: Obsolete version of ghmid as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ghomidOLD.1 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
ghomidOLD.2 ${⊢}{T}=\mathrm{GId}\left({H}\right)$
Assertion ghomidOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({U}\right)={T}$

### Proof

Step Hyp Ref Expression
1 ghomidOLD.1 ${⊢}{U}=\mathrm{GId}\left({G}\right)$
2 ghomidOLD.2 ${⊢}{T}=\mathrm{GId}\left({H}\right)$
3 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
4 3 1 grpoidcl ${⊢}{G}\in \mathrm{GrpOp}\to {U}\in \mathrm{ran}{G}$
5 4 3ad2ant1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {U}\in \mathrm{ran}{G}$
6 5 5 jca ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({U}\in \mathrm{ran}{G}\wedge {U}\in \mathrm{ran}{G}\right)$
7 3 ghomlinOLD ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({U}\in \mathrm{ran}{G}\wedge {U}\in \mathrm{ran}{G}\right)\right)\to {F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}{G}{U}\right)$
8 6 7 mpdan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}{G}{U}\right)$
9 3 1 grpolid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {U}\in \mathrm{ran}{G}\right)\to {U}{G}{U}={U}$
10 4 9 mpdan ${⊢}{G}\in \mathrm{GrpOp}\to {U}{G}{U}={U}$
11 10 fveq2d ${⊢}{G}\in \mathrm{GrpOp}\to {F}\left({U}{G}{U}\right)={F}\left({U}\right)$
12 11 3ad2ant1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({U}{G}{U}\right)={F}\left({U}\right)$
13 8 12 eqtrd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}\right)$
14 eqid ${⊢}\mathrm{ran}{H}=\mathrm{ran}{H}$
15 3 14 elghomOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({F}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔\left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)\right)$
16 15 biimp3a ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)$
17 16 simpld ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}$
18 17 5 ffvelrnd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({U}\right)\in \mathrm{ran}{H}$
19 14 2 grpoid ${⊢}\left({H}\in \mathrm{GrpOp}\wedge {F}\left({U}\right)\in \mathrm{ran}{H}\right)\to \left({F}\left({U}\right)={T}↔{F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}\right)\right)$
20 19 ex ${⊢}{H}\in \mathrm{GrpOp}\to \left({F}\left({U}\right)\in \mathrm{ran}{H}\to \left({F}\left({U}\right)={T}↔{F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}\right)\right)\right)$
21 20 3ad2ant2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}\left({U}\right)\in \mathrm{ran}{H}\to \left({F}\left({U}\right)={T}↔{F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}\right)\right)\right)$
22 18 21 mpd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}\left({U}\right)={T}↔{F}\left({U}\right){H}{F}\left({U}\right)={F}\left({U}\right)\right)$
23 13 22 mpbird ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}\left({U}\right)={T}$