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 \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to 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 \in GrpOp \land H \in GrpOp) \to (F \in (G GrpOpHom H) \leftrightarrow (F : X ⟶ ran H \land \forall x \in X \forall y \in X F (x) H F (y) = F (x G y)))$
4	3	biimp3a	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F : X ⟶ ran H \land \forall x \in X \forall y \in X F (x) H F (y) = F (x G y))$
5	4	simprd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to \forall x \in X \forall y \in X F (x) H F (y) = F (x G y)$
6		fveq2	$⊢ x = A \to F (x) = F (A)$
7	6	oveq1d	$⊢ x = A \to F (x) H F (y) = F (A) H F (y)$
8		oveq1	$⊢ x = A \to x G y = A G y$
9	8	fveq2d	$⊢ x = A \to F (x G y) = F (A G y)$
10	7 9	eqeq12d	$⊢ x = A \to (F (x) H F (y) = F (x G y) \leftrightarrow F (A) H F (y) = F (A G y))$
11		fveq2	$⊢ y = B \to F (y) = F (B)$
12	11	oveq2d	$⊢ y = B \to F (A) H F (y) = F (A) H F (B)$
13		oveq2	$⊢ y = B \to A G y = A G B$
14	13	fveq2d	$⊢ y = B \to F (A G y) = F (A G B)$
15	12 14	eqeq12d	$⊢ y = B \to (F (A) H F (y) = F (A G y) \leftrightarrow F (A) H F (B) = F (A G B))$
16	10 15	rspc2v	$⊢ (A \in X \land B \in X) \to (\forall x \in X \forall y \in X F (x) H F (y) = F (x G y) \to F (A) H F (B) = F (A G B))$
17	5 16	mpan9	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (A \in X \land B \in X)) \to F (A) H F (B) = F (A G B)$