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=BaseS
ghminv.y ⊢M=invg⁡S
ghminv.z ⊢N=invg⁡T
Assertion ghminv ⊢F∈SGrpHomT∧X∈B→F⁡M⁡X=N⁡F⁡X

Proof

Step Hyp Ref Expression
1 ghminv.b ⊢B=BaseS
2 ghminv.y ⊢M=invg⁡S
3 ghminv.z ⊢N=invg⁡T
4 ghmgrp1 ⊢F∈SGrpHomT→S∈Grp
5 eqid ⊢+S=+S
6 eqid ⊢0S=0S
7 1 5 6 2 grprinv ⊢S∈Grp∧X∈B→X+SM⁡X=0S
8 4 7 sylan ⊢F∈SGrpHomT∧X∈B→X+SM⁡X=0S
9 8 fveq2d ⊢F∈SGrpHomT∧X∈B→F⁡X+SM⁡X=F⁡0S
10 1 2 grpinvcl ⊢S∈Grp∧X∈B→M⁡X∈B
11 4 10 sylan ⊢F∈SGrpHomT∧X∈B→M⁡X∈B
12 eqid ⊢+T=+T
13 1 5 12 ghmlin ⊢F∈SGrpHomT∧X∈B∧M⁡X∈B→F⁡X+SM⁡X=F⁡X+TF⁡M⁡X
14 11 13 mpd3an3 ⊢F∈SGrpHomT∧X∈B→F⁡X+SM⁡X=F⁡X+TF⁡M⁡X
15 eqid ⊢0T=0T
16 6 15 ghmid ⊢F∈SGrpHomT→F⁡0S=0T
17 16 adantr ⊢F∈SGrpHomT∧X∈B→F⁡0S=0T
18 9 14 17 3eqtr3d ⊢F∈SGrpHomT∧X∈B→F⁡X+TF⁡M⁡X=0T
19 ghmgrp2 ⊢F∈SGrpHomT→T∈Grp
20 19 adantr ⊢F∈SGrpHomT∧X∈B→T∈Grp
21 eqid ⊢BaseT=BaseT
22 1 21 ghmf ⊢F∈SGrpHomT→F:B⟶BaseT
23 22 ffvelcdmda ⊢F∈SGrpHomT∧X∈B→F⁡X∈BaseT
24 22 adantr ⊢F∈SGrpHomT∧X∈B→F:B⟶BaseT
25 24 11 ffvelcdmd ⊢F∈SGrpHomT∧X∈B→F⁡M⁡X∈BaseT
26 21 12 15 3 grpinvid1 ⊢T∈Grp∧F⁡X∈BaseT∧F⁡M⁡X∈BaseT→N⁡F⁡X=F⁡M⁡X↔F⁡X+TF⁡M⁡X=0T
27 20 23 25 26 syl3anc ⊢F∈SGrpHomT∧X∈B→N⁡F⁡X=F⁡M⁡X↔F⁡X+TF⁡M⁡X=0T
28 18 27 mpbird ⊢F∈SGrpHomT∧X∈B→N⁡F⁡X=F⁡M⁡X
29 28 eqcomd ⊢F∈SGrpHomT∧X∈B→F⁡M⁡X=N⁡F⁡X