# Metamath Proof Explorer

## Theorem ghomdiv

Description: Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses ghomdiv.1 ${⊢}{X}=\mathrm{ran}{G}$
ghomdiv.2 ${⊢}{D}={/}_{g}\left({G}\right)$
ghomdiv.3 ${⊢}{C}={/}_{g}\left({H}\right)$
Assertion ghomdiv ${⊢}\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}{D}{B}\right)={F}\left({A}\right){C}{F}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 ghomdiv.1 ${⊢}{X}=\mathrm{ran}{G}$
2 ghomdiv.2 ${⊢}{D}={/}_{g}\left({G}\right)$
3 ghomdiv.3 ${⊢}{C}={/}_{g}\left({H}\right)$
4 simpl2 ${⊢}\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 {H}\in \mathrm{GrpOp}$
5 eqid ${⊢}\mathrm{ran}{H}=\mathrm{ran}{H}$
6 1 5 ghomf ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}:{X}⟶\mathrm{ran}{H}$
7 6 ffvelrnda ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {A}\in {X}\right)\to {F}\left({A}\right)\in \mathrm{ran}{H}$
8 7 adantrr ${⊢}\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)\in \mathrm{ran}{H}$
9 6 ffvelrnda ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {B}\in {X}\right)\to {F}\left({B}\right)\in \mathrm{ran}{H}$
10 9 adantrl ${⊢}\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({B}\right)\in \mathrm{ran}{H}$
11 5 3 grponpcan ${⊢}\left({H}\in \mathrm{GrpOp}\wedge {F}\left({A}\right)\in \mathrm{ran}{H}\wedge {F}\left({B}\right)\in \mathrm{ran}{H}\right)\to \left({F}\left({A}\right){C}{F}\left({B}\right)\right){H}{F}\left({B}\right)={F}\left({A}\right)$
12 4 8 10 11 syl3anc ${⊢}\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 \left({F}\left({A}\right){C}{F}\left({B}\right)\right){H}{F}\left({B}\right)={F}\left({A}\right)$
13 1 2 grponpcan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}{D}{B}\right){G}{B}={A}$
14 13 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{D}{B}\right){G}{B}={A}$
15 14 3ad2antl1 ${⊢}\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 \left({A}{D}{B}\right){G}{B}={A}$
16 15 fveq2d ${⊢}\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(\left({A}{D}{B}\right){G}{B}\right)={F}\left({A}\right)$
17 1 2 grpodivcl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\in {X}$
18 17 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{D}{B}\in {X}$
19 simprr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {B}\in {X}$
20 18 19 jca ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{D}{B}\in {X}\wedge {B}\in {X}\right)$
21 20 3ad2antl1 ${⊢}\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 \left({A}{D}{B}\in {X}\wedge {B}\in {X}\right)$
22 1 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}{D}{B}\in {X}\wedge {B}\in {X}\right)\right)\to {F}\left({A}{D}{B}\right){H}{F}\left({B}\right)={F}\left(\left({A}{D}{B}\right){G}{B}\right)$
23 22 eqcomd ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge \left({A}{D}{B}\in {X}\wedge {B}\in {X}\right)\right)\to {F}\left(\left({A}{D}{B}\right){G}{B}\right)={F}\left({A}{D}{B}\right){H}{F}\left({B}\right)$
24 21 23 syldan ${⊢}\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(\left({A}{D}{B}\right){G}{B}\right)={F}\left({A}{D}{B}\right){H}{F}\left({B}\right)$
25 12 16 24 3eqtr2rd ${⊢}\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}{D}{B}\right){H}{F}\left({B}\right)=\left({F}\left({A}\right){C}{F}\left({B}\right)\right){H}{F}\left({B}\right)$
26 18 3ad2antl1 ${⊢}\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 {A}{D}{B}\in {X}$
27 6 ffvelrnda ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\wedge {A}{D}{B}\in {X}\right)\to {F}\left({A}{D}{B}\right)\in \mathrm{ran}{H}$
28 26 27 syldan ${⊢}\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}{D}{B}\right)\in \mathrm{ran}{H}$
29 5 3 grpodivcl ${⊢}\left({H}\in \mathrm{GrpOp}\wedge {F}\left({A}\right)\in \mathrm{ran}{H}\wedge {F}\left({B}\right)\in \mathrm{ran}{H}\right)\to {F}\left({A}\right){C}{F}\left({B}\right)\in \mathrm{ran}{H}$
30 4 8 10 29 syl3anc ${⊢}\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){C}{F}\left({B}\right)\in \mathrm{ran}{H}$
31 5 grporcan ${⊢}\left({H}\in \mathrm{GrpOp}\wedge \left({F}\left({A}{D}{B}\right)\in \mathrm{ran}{H}\wedge {F}\left({A}\right){C}{F}\left({B}\right)\in \mathrm{ran}{H}\wedge {F}\left({B}\right)\in \mathrm{ran}{H}\right)\right)\to \left({F}\left({A}{D}{B}\right){H}{F}\left({B}\right)=\left({F}\left({A}\right){C}{F}\left({B}\right)\right){H}{F}\left({B}\right)↔{F}\left({A}{D}{B}\right)={F}\left({A}\right){C}{F}\left({B}\right)\right)$
32 4 28 30 10 31 syl13anc ${⊢}\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 \left({F}\left({A}{D}{B}\right){H}{F}\left({B}\right)=\left({F}\left({A}\right){C}{F}\left({B}\right)\right){H}{F}\left({B}\right)↔{F}\left({A}{D}{B}\right)={F}\left({A}\right){C}{F}\left({B}\right)\right)$
33 25 32 mpbid ${⊢}\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}{D}{B}\right)={F}\left({A}\right){C}{F}\left({B}\right)$