# Metamath Proof Explorer

## Theorem ghminv

Description: A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypotheses ghminv.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
ghminv.y ${⊢}{M}={inv}_{g}\left({S}\right)$
ghminv.z ${⊢}{N}={inv}_{g}\left({T}\right)$
Assertion ghminv ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({M}\left({X}\right)\right)={N}\left({F}\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ghminv.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
2 ghminv.y ${⊢}{M}={inv}_{g}\left({S}\right)$
3 ghminv.z ${⊢}{N}={inv}_{g}\left({T}\right)$
4 ghmgrp1 ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {S}\in \mathrm{Grp}$
5 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
6 eqid ${⊢}{0}_{{S}}={0}_{{S}}$
7 1 5 6 2 grprinv ${⊢}\left({S}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {X}{+}_{{S}}{M}\left({X}\right)={0}_{{S}}$
8 4 7 sylan ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {X}{+}_{{S}}{M}\left({X}\right)={0}_{{S}}$
9 8 fveq2d ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({X}{+}_{{S}}{M}\left({X}\right)\right)={F}\left({0}_{{S}}\right)$
10 1 2 grpinvcl ${⊢}\left({S}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {M}\left({X}\right)\in {B}$
11 4 10 sylan ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {M}\left({X}\right)\in {B}$
12 eqid ${⊢}{+}_{{T}}={+}_{{T}}$
13 1 5 12 ghmlin ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\wedge {M}\left({X}\right)\in {B}\right)\to {F}\left({X}{+}_{{S}}{M}\left({X}\right)\right)={F}\left({X}\right){+}_{{T}}{F}\left({M}\left({X}\right)\right)$
14 11 13 mpd3an3 ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({X}{+}_{{S}}{M}\left({X}\right)\right)={F}\left({X}\right){+}_{{T}}{F}\left({M}\left({X}\right)\right)$
15 eqid ${⊢}{0}_{{T}}={0}_{{T}}$
16 6 15 ghmid ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {F}\left({0}_{{S}}\right)={0}_{{T}}$
17 16 adantr ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({0}_{{S}}\right)={0}_{{T}}$
18 9 14 17 3eqtr3d ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({X}\right){+}_{{T}}{F}\left({M}\left({X}\right)\right)={0}_{{T}}$
19 ghmgrp2 ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {T}\in \mathrm{Grp}$
20 19 adantr ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {T}\in \mathrm{Grp}$
21 eqid ${⊢}{\mathrm{Base}}_{{T}}={\mathrm{Base}}_{{T}}$
22 1 21 ghmf ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {F}:{B}⟶{\mathrm{Base}}_{{T}}$
23 22 ffvelrnda ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in {\mathrm{Base}}_{{T}}$
24 22 adantr ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}:{B}⟶{\mathrm{Base}}_{{T}}$
25 24 11 ffvelrnd ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({M}\left({X}\right)\right)\in {\mathrm{Base}}_{{T}}$
26 21 12 15 3 grpinvid1 ${⊢}\left({T}\in \mathrm{Grp}\wedge {F}\left({X}\right)\in {\mathrm{Base}}_{{T}}\wedge {F}\left({M}\left({X}\right)\right)\in {\mathrm{Base}}_{{T}}\right)\to \left({N}\left({F}\left({X}\right)\right)={F}\left({M}\left({X}\right)\right)↔{F}\left({X}\right){+}_{{T}}{F}\left({M}\left({X}\right)\right)={0}_{{T}}\right)$
27 20 23 25 26 syl3anc ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to \left({N}\left({F}\left({X}\right)\right)={F}\left({M}\left({X}\right)\right)↔{F}\left({X}\right){+}_{{T}}{F}\left({M}\left({X}\right)\right)={0}_{{T}}\right)$
28 18 27 mpbird ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {N}\left({F}\left({X}\right)\right)={F}\left({M}\left({X}\right)\right)$
29 28 eqcomd ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in {B}\right)\to {F}\left({M}\left({X}\right)\right)={N}\left({F}\left({X}\right)\right)$