ghmgrp

Description: The image of a group G under a group homomorphism F is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 25-Jan-2020)

	Ref	Expression
Hypotheses	ghmgrp.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
	ghmgrp.x	$⊢ X = {Base}_{G}$
	ghmgrp.y	$⊢ Y = {Base}_{H}$
	ghmgrp.p	$⊢ \underset{˙}{+} = +_{G}$
	ghmgrp.q	$⊢ \underset{˙}{⨣} = +_{H}$
	ghmgrp.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
	ghmgrp.3	$⊢ φ \to G \in Grp$
Assertion	ghmgrp	$⊢ φ \to H \in Grp$

Proof

Step	Hyp	Ref	Expression
1		ghmgrp.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
2		ghmgrp.x	$⊢ X = {Base}_{G}$
3		ghmgrp.y	$⊢ Y = {Base}_{H}$
4		ghmgrp.p	$⊢ \underset{˙}{+} = +_{G}$
5		ghmgrp.q	$⊢ \underset{˙}{⨣} = +_{H}$
6		ghmgrp.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
7		ghmgrp.3	$⊢ φ \to G \in Grp$
8	7	grpmndd	$⊢ φ \to G \in Mnd$
9	1 2 3 4 5 6 8	mhmmnd	$⊢ φ \to H \in Mnd$
10		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
11	6 10	syl	$⊢ φ \to F : X ⟶ Y$
12	11	ad3antrrr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F : X ⟶ Y$
13	7	ad3antrrr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to G \in Grp$
14		simplr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to i \in X$
15		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
16	2 15	grpinvcl	$⊢ (G \in Grp \land i \in X) \to {inv}_{g} (G) (i) \in X$
17	13 14 16	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to {inv}_{g} (G) (i) \in X$
18	12 17	ffvelrnd	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F ({inv}_{g} (G) (i)) \in Y$
19	1	3adant1r	$⊢ ((φ \land i \in X) \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
20	7 16	sylan	$⊢ (φ \land i \in X) \to {inv}_{g} (G) (i) \in X$
21		simpr	$⊢ (φ \land i \in X) \to i \in X$
22	19 20 21	mhmlem	$⊢ (φ \land i \in X) \to F ({inv}_{g} (G) (i) \underset{˙}{+} i) = F ({inv}_{g} (G) (i)) \underset{˙}{⨣} F (i)$
23	22	ad4ant13	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F ({inv}_{g} (G) (i) \underset{˙}{+} i) = F ({inv}_{g} (G) (i)) \underset{˙}{⨣} F (i)$
24		eqid	$⊢ 0_{G} = 0_{G}$
25	2 4 24 15	grplinv	$⊢ (G \in Grp \land i \in X) \to {inv}_{g} (G) (i) \underset{˙}{+} i = 0_{G}$
26	25	fveq2d	$⊢ (G \in Grp \land i \in X) \to F ({inv}_{g} (G) (i) \underset{˙}{+} i) = F (0_{G})$
27	13 14 26	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F ({inv}_{g} (G) (i) \underset{˙}{+} i) = F (0_{G})$
28	1 2 3 4 5 6 8 24	mhmid	$⊢ φ \to F (0_{G}) = 0_{H}$
29	28	ad3antrrr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (0_{G}) = 0_{H}$
30	27 29	eqtrd	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F ({inv}_{g} (G) (i) \underset{˙}{+} i) = 0_{H}$
31		simpr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) = a$
32	31	oveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F ({inv}_{g} (G) (i)) \underset{˙}{⨣} F (i) = F ({inv}_{g} (G) (i)) \underset{˙}{⨣} a$
33	23 30 32	3eqtr3rd	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F ({inv}_{g} (G) (i)) \underset{˙}{⨣} a = 0_{H}$
34		oveq1	$⊢ f = F ({inv}_{g} (G) (i)) \to f \underset{˙}{⨣} a = F ({inv}_{g} (G) (i)) \underset{˙}{⨣} a$
35	34	eqeq1d	$⊢ f = F ({inv}_{g} (G) (i)) \to (f \underset{˙}{⨣} a = 0_{H} \leftrightarrow F ({inv}_{g} (G) (i)) \underset{˙}{⨣} a = 0_{H})$
36	35	rspcev	$⊢ (F ({inv}_{g} (G) (i)) \in Y \land F ({inv}_{g} (G) (i)) \underset{˙}{⨣} a = 0_{H}) \to \exists f \in Y f \underset{˙}{⨣} a = 0_{H}$
37	18 33 36	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to \exists f \in Y f \underset{˙}{⨣} a = 0_{H}$
38		foelrni	$⊢ (F : X \underset{onto}{⟶} Y \land a \in Y) \to \exists i \in X F (i) = a$
39	6 38	sylan	$⊢ (φ \land a \in Y) \to \exists i \in X F (i) = a$
40	37 39	r19.29a	$⊢ (φ \land a \in Y) \to \exists f \in Y f \underset{˙}{⨣} a = 0_{H}$
41	40	ralrimiva	$⊢ φ \to \forall a \in Y \exists f \in Y f \underset{˙}{⨣} a = 0_{H}$
42		eqid	$⊢ 0_{H} = 0_{H}$
43	3 5 42	isgrp	$⊢ H \in Grp \leftrightarrow (H \in Mnd \land \forall a \in Y \exists f \in Y f \underset{˙}{⨣} a = 0_{H})$
44	9 41 43	sylanbrc	$⊢ φ \to H \in Grp$

Metamath Proof Explorer

Theorem ghmgrp

Proof