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 = ran ⁡ G
Assertion ghomlinOLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A H F ⁡ B = F ⁡ A G B

Proof

Step Hyp Ref Expression
1 ghomlinOLD.1 ⊢ X = ran ⁡ G
2 eqid ⊢ ran ⁡ H = ran ⁡ H
3 1 2 elghomOLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ G GrpOpHom H ↔ F : X ⟶ ran ⁡ H ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y
4 3 biimp3a ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H → F : X ⟶ ran ⁡ H ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y
5 4 simprd ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H → ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y
6 fveq2 ⊢ x = A → F ⁡ x = F ⁡ A
7 6 oveq1d ⊢ x = A → F ⁡ x H F ⁡ y = F ⁡ A H F ⁡ y
8 oveq1 ⊢ x = A → x G y = A G y
9 8 fveq2d ⊢ x = A → F ⁡ x G y = F ⁡ A G y
10 7 9 eqeq12d ⊢ x = A → F ⁡ x H F ⁡ y = F ⁡ x G y ↔ F ⁡ A H F ⁡ y = F ⁡ A G y
11 fveq2 ⊢ y = B → F ⁡ y = F ⁡ B
12 11 oveq2d ⊢ y = B → F ⁡ A H F ⁡ y = F ⁡ A H F ⁡ B
13 oveq2 ⊢ y = B → A G y = A G B
14 13 fveq2d ⊢ y = B → F ⁡ A G y = F ⁡ A G B
15 12 14 eqeq12d ⊢ y = B → F ⁡ A H F ⁡ y = F ⁡ A G y ↔ F ⁡ A H F ⁡ B = F ⁡ A G B
16 10 15 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y → F ⁡ A H F ⁡ B = F ⁡ A G B
17 5 16 mpan9 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H ∧ A ∈ X ∧ B ∈ X → F ⁡ A H F ⁡ B = F ⁡ A G B