Metamath Proof Explorer

Theorem ghomdiv

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

Ref Expression
Hypotheses ghomdiv.1 ⊢ X = ran ⁡ G
ghomdiv.2 ⊢ D = / g ⁡ G
ghomdiv.3 ⊢ C = / g ⁡ H
Assertion ghomdiv ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B = F ⁡ A C F ⁡ B

Proof

Step Hyp Ref Expression
1 ghomdiv.1 ⊢ X = ran ⁡ G
2 ghomdiv.2 ⊢ D = / g ⁡ G
3 ghomdiv.3 ⊢ C = / g ⁡ H
4 simpl2 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → H ∈ GrpOp
5 eqid ⊢ ran ⁡ H = ran ⁡ H
6 1 5 ghomf ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H → F : X ⟶ ran ⁡ H
7 6 ffvelrnda ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X → F ⁡ A ∈ ran ⁡ H
8 7 adantrr ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A ∈ ran ⁡ H
9 6 ffvelrnda ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ B ∈ X → F ⁡ B ∈ ran ⁡ H
10 9 adantrl ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ B ∈ ran ⁡ H
11 5 3 grponpcan ⊢ H ∈ GrpOp ∧ F ⁡ A ∈ ran ⁡ H ∧ F ⁡ B ∈ ran ⁡ H → F ⁡ A C F ⁡ B H F ⁡ B = F ⁡ A
12 4 8 10 11 syl3anc ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A C F ⁡ B H F ⁡ B = F ⁡ A
13 1 2 grponpcan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B G B = A
14 13 3expb ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B G B = A
15 14 3ad2antl1 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → A D B G B = A
16 15 fveq2d ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B G B = F ⁡ A
17 1 2 grpodivcl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B ∈ X
18 17 3expb ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B ∈ X
19 simprr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → B ∈ X
20 18 19 jca ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A D B ∈ X ∧ B ∈ X
21 20 3ad2antl1 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → A D B ∈ X ∧ B ∈ X
22 1 ghomlinOLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A D B ∈ X ∧ B ∈ X → F ⁡ A D B H F ⁡ B = F ⁡ A D B G B
23 22 eqcomd ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A D B ∈ X ∧ B ∈ X → F ⁡ A D B G B = F ⁡ A D B H F ⁡ B
24 21 23 syldan ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B G B = F ⁡ A D B H F ⁡ B
25 12 16 24 3eqtr2rd ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B H F ⁡ B = F ⁡ A C F ⁡ B H F ⁡ B
26 18 3ad2antl1 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → A D B ∈ X
27 6 ffvelrnda ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A D B ∈ X → F ⁡ A D B ∈ ran ⁡ H
28 26 27 syldan ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B ∈ ran ⁡ H
29 5 3 grpodivcl ⊢ H ∈ GrpOp ∧ F ⁡ A ∈ ran ⁡ H ∧ F ⁡ B ∈ ran ⁡ H → F ⁡ A C F ⁡ B ∈ ran ⁡ H
30 4 8 10 29 syl3anc ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A C F ⁡ B ∈ ran ⁡ H
31 5 grporcan ⊢ H ∈ GrpOp ∧ F ⁡ A D B ∈ ran ⁡ H ∧ F ⁡ A C F ⁡ B ∈ ran ⁡ H ∧ F ⁡ B ∈ ran ⁡ H → F ⁡ A D B H F ⁡ B = F ⁡ A C F ⁡ B H F ⁡ B ↔ F ⁡ A D B = F ⁡ A C F ⁡ B
32 4 28 30 10 31 syl13anc ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B H F ⁡ B = F ⁡ A C F ⁡ B H F ⁡ B ↔ F ⁡ A D B = F ⁡ A C F ⁡ B
33 25 32 mpbid ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A D B = F ⁡ A C F ⁡ B