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

Metamath Proof Explorer

Theorem ghmgrp

Proof