# Metamath Proof Explorer

## Theorem ghomlinOLD

Description: Obsolete version of ghmlin as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis ghomlinOLD.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion ghomlinOLD ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {F}\left({A}\right){H}{F}\left({B}\right)={F}\left({A}{G}{B}\right)$

### Proof

Step Hyp Ref Expression
1 ghomlinOLD.1 ${⊢}{X}=\mathrm{ran}{G}$
2 eqid ${⊢}\mathrm{ran}{H}=\mathrm{ran}{H}$
3 1 2 elghomOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({F}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔\left({F}:{X}⟶\mathrm{ran}{H}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)\right)$
4 3 biimp3a ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \left({F}:{X}⟶\mathrm{ran}{H}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)$
5 4 simprd ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)$
6 fveq2 ${⊢}{x}={A}\to {F}\left({x}\right)={F}\left({A}\right)$
7 6 oveq1d ${⊢}{x}={A}\to {F}\left({x}\right){H}{F}\left({y}\right)={F}\left({A}\right){H}{F}\left({y}\right)$
8 oveq1 ${⊢}{x}={A}\to {x}{G}{y}={A}{G}{y}$
9 8 fveq2d ${⊢}{x}={A}\to {F}\left({x}{G}{y}\right)={F}\left({A}{G}{y}\right)$
10 7 9 eqeq12d ${⊢}{x}={A}\to \left({F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)↔{F}\left({A}\right){H}{F}\left({y}\right)={F}\left({A}{G}{y}\right)\right)$
11 fveq2 ${⊢}{y}={B}\to {F}\left({y}\right)={F}\left({B}\right)$
12 11 oveq2d ${⊢}{y}={B}\to {F}\left({A}\right){H}{F}\left({y}\right)={F}\left({A}\right){H}{F}\left({B}\right)$
13 oveq2 ${⊢}{y}={B}\to {A}{G}{y}={A}{G}{B}$
14 13 fveq2d ${⊢}{y}={B}\to {F}\left({A}{G}{y}\right)={F}\left({A}{G}{B}\right)$
15 12 14 eqeq12d ${⊢}{y}={B}\to \left({F}\left({A}\right){H}{F}\left({y}\right)={F}\left({A}{G}{y}\right)↔{F}\left({A}\right){H}{F}\left({B}\right)={F}\left({A}{G}{B}\right)\right)$
16 10 15 rspc2v ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\to {F}\left({A}\right){H}{F}\left({B}\right)={F}\left({A}{G}{B}\right)\right)$
17 5 16 mpan9 ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {F}\left({A}\right){H}{F}\left({B}\right)={F}\left({A}{G}{B}\right)$