ghomidOLD

Description: Obsolete version of ghmid as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	ghomidOLD.1	$⊢ U = GId (G)$
	ghomidOLD.2	$⊢ T = GId (H)$
Assertion	ghomidOLD	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (U) = T$

Proof

Step	Hyp	Ref	Expression
1		ghomidOLD.1	$⊢ U = GId (G)$
2		ghomidOLD.2	$⊢ T = GId (H)$
3		eqid	$⊢ ran G = ran G$
4	3 1	grpoidcl	$⊢ G \in GrpOp \to U \in ran G$
5	4	3ad2ant1	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to U \in ran G$
6	5 5	jca	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (U \in ran G \land U \in ran G)$
7	3	ghomlinOLD	$⊢ ((G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \land (U \in ran G \land U \in ran G)) \to F (U) H F (U) = F (U G U)$
8	6 7	mpdan	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (U) H F (U) = F (U G U)$
9	3 1	grpolid	$⊢ (G \in GrpOp \land U \in ran G) \to U G U = U$
10	4 9	mpdan	$⊢ G \in GrpOp \to U G U = U$
11	10	fveq2d	$⊢ G \in GrpOp \to F (U G U) = F (U)$
12	11	3ad2ant1	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (U G U) = F (U)$
13	8 12	eqtrd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (U) H F (U) = F (U)$
14		eqid	$⊢ ran H = ran H$
15	3 14	elghomOLD	$⊢ (G \in GrpOp \land H \in GrpOp) \to (F \in (G GrpOpHom H) \leftrightarrow (F : ran G ⟶ ran H \land \forall x \in ran G \forall y \in ran G F (x) H F (y) = F (x G y)))$
16	15	biimp3a	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F : ran G ⟶ ran H \land \forall x \in ran G \forall y \in ran G F (x) H F (y) = F (x G y))$
17	16	simpld	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F : ran G ⟶ ran H$
18	17 5	ffvelcdmd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (U) \in ran H$
19	14 2	grpoid	$⊢ (H \in GrpOp \land F (U) \in ran H) \to (F (U) = T \leftrightarrow F (U) H F (U) = F (U))$
20	19	ex	$⊢ H \in GrpOp \to (F (U) \in ran H \to (F (U) = T \leftrightarrow F (U) H F (U) = F (U)))$
21	20	3ad2ant2	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F (U) \in ran H \to (F (U) = T \leftrightarrow F (U) H F (U) = F (U)))$
22	18 21	mpd	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to (F (U) = T \leftrightarrow F (U) H F (U) = F (U))$
23	13 22	mpbird	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F (U) = T$

Metamath Proof Explorer

Theorem ghomidOLD

Proof