ghmnsgima

Description: The image of a normal subgroup under a surjective homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Hypothesis	ghmnsgima.1	$⊢ Y = {Base}_{T}$
	Assertion	ghmnsgima	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to F [U] \in NrmSGrp (T)$

Proof

Step	Hyp	Ref	Expression
1		ghmnsgima.1	$⊢ Y = {Base}_{T}$
2		simp1	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to F \in (S GrpHom T)$
3		nsgsubg	$⊢ U \in NrmSGrp (S) \to U \in SubGrp (S)$
4	3	3ad2ant2	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to U \in SubGrp (S)$
5		ghmima	$⊢ (F \in (S GrpHom T) \land U \in SubGrp (S)) \to F [U] \in SubGrp (T)$
6	2 4 5	syl2anc	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to F [U] \in SubGrp (T)$
7	2	adantr	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F \in (S GrpHom T)$
8		ghmgrp1	$⊢ F \in (S GrpHom T) \to S \in Grp$
9	7 8	syl	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to S \in Grp$
10		simprl	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to z \in {Base}_{S}$
11		eqid	$⊢ {Base}_{S} = {Base}_{S}$
12	11	subgss	$⊢ U \in SubGrp (S) \to U \subseteq {Base}_{S}$
13	4 12	syl	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to U \subseteq {Base}_{S}$
14	13	adantr	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to U \subseteq {Base}_{S}$
15		simprr	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to x \in U$
16	14 15	sseldd	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to x \in {Base}_{S}$
17		eqid	$⊢ +_{S} = +_{S}$
18	11 17	grpcl	$⊢ (S \in Grp \land z \in {Base}_{S} \land x \in {Base}_{S}) \to z +_{S} x \in {Base}_{S}$
19	9 10 16 18	syl3anc	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to z +_{S} x \in {Base}_{S}$
20		eqid	$⊢ -_{S} = -_{S}$
21		eqid	$⊢ -_{T} = -_{T}$
22	11 20 21	ghmsub	$⊢ (F \in (S GrpHom T) \land z +_{S} x \in {Base}_{S} \land z \in {Base}_{S}) \to F ((z +_{S} x) -_{S} z) = F (z +_{S} x) -_{T} F (z)$
23	7 19 10 22	syl3anc	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F ((z +_{S} x) -_{S} z) = F (z +_{S} x) -_{T} F (z)$
24		eqid	$⊢ +_{T} = +_{T}$
25	11 17 24	ghmlin	$⊢ (F \in (S GrpHom T) \land z \in {Base}_{S} \land x \in {Base}_{S}) \to F (z +_{S} x) = F (z) +_{T} F (x)$
26	7 10 16 25	syl3anc	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F (z +_{S} x) = F (z) +_{T} F (x)$
27	26	oveq1d	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F (z +_{S} x) -_{T} F (z) = (F (z) +_{T} F (x)) -_{T} F (z)$
28	23 27	eqtrd	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F ((z +_{S} x) -_{S} z) = (F (z) +_{T} F (x)) -_{T} F (z)$
29	11 1	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ Y$
30	2 29	syl	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to F : {Base}_{S} ⟶ Y$
31	30	adantr	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F : {Base}_{S} ⟶ Y$
32	31	ffnd	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F Fn {Base}_{S}$
33		simpl2	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to U \in NrmSGrp (S)$
34	11 17 20	nsgconj	$⊢ (U \in NrmSGrp (S) \land z \in {Base}_{S} \land x \in U) \to (z +_{S} x) -_{S} z \in U$
35	33 10 15 34	syl3anc	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to (z +_{S} x) -_{S} z \in U$
36		fnfvima	$⊢ (F Fn {Base}_{S} \land U \subseteq {Base}_{S} \land (z +_{S} x) -_{S} z \in U) \to F ((z +_{S} x) -_{S} z) \in F [U]$
37	32 14 35 36	syl3anc	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to F ((z +_{S} x) -_{S} z) \in F [U]$
38	28 37	eqeltrrd	$⊢ ((F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \land (z \in {Base}_{S} \land x \in U)) \to (F (z) +_{T} F (x)) -_{T} F (z) \in F [U]$
39	38	ralrimivva	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to \forall z \in {Base}_{S} \forall x \in U (F (z) +_{T} F (x)) -_{T} F (z) \in F [U]$
40	30	ffnd	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to F Fn {Base}_{S}$
41		oveq1	$⊢ x = F (z) \to x +_{T} y = F (z) +_{T} y$
42		id	$⊢ x = F (z) \to x = F (z)$
43	41 42	oveq12d	$⊢ x = F (z) \to (x +_{T} y) -_{T} x = (F (z) +_{T} y) -_{T} F (z)$
44	43	eleq1d	$⊢ x = F (z) \to ((x +_{T} y) -_{T} x \in F [U] \leftrightarrow (F (z) +_{T} y) -_{T} F (z) \in F [U])$
45	44	ralbidv	$⊢ x = F (z) \to (\forall y \in F [U] (x +_{T} y) -_{T} x \in F [U] \leftrightarrow \forall y \in F [U] (F (z) +_{T} y) -_{T} F (z) \in F [U])$
46	45	ralrn	$⊢ F Fn {Base}_{S} \to (\forall x \in ran F \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U] \leftrightarrow \forall z \in {Base}_{S} \forall y \in F [U] (F (z) +_{T} y) -_{T} F (z) \in F [U])$
47	40 46	syl	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to (\forall x \in ran F \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U] \leftrightarrow \forall z \in {Base}_{S} \forall y \in F [U] (F (z) +_{T} y) -_{T} F (z) \in F [U])$
48		simp3	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to ran F = Y$
49	48	raleqdv	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to (\forall x \in ran F \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U] \leftrightarrow \forall x \in Y \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U])$
50		oveq2	$⊢ y = F (x) \to F (z) +_{T} y = F (z) +_{T} F (x)$
51	50	oveq1d	$⊢ y = F (x) \to (F (z) +_{T} y) -_{T} F (z) = (F (z) +_{T} F (x)) -_{T} F (z)$
52	51	eleq1d	$⊢ y = F (x) \to ((F (z) +_{T} y) -_{T} F (z) \in F [U] \leftrightarrow (F (z) +_{T} F (x)) -_{T} F (z) \in F [U])$
53	52	ralima	$⊢ (F Fn {Base}_{S} \land U \subseteq {Base}_{S}) \to (\forall y \in F [U] (F (z) +_{T} y) -_{T} F (z) \in F [U] \leftrightarrow \forall x \in U (F (z) +_{T} F (x)) -_{T} F (z) \in F [U])$
54	40 13 53	syl2anc	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to (\forall y \in F [U] (F (z) +_{T} y) -_{T} F (z) \in F [U] \leftrightarrow \forall x \in U (F (z) +_{T} F (x)) -_{T} F (z) \in F [U])$
55	54	ralbidv	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to (\forall z \in {Base}_{S} \forall y \in F [U] (F (z) +_{T} y) -_{T} F (z) \in F [U] \leftrightarrow \forall z \in {Base}_{S} \forall x \in U (F (z) +_{T} F (x)) -_{T} F (z) \in F [U])$
56	47 49 55	3bitr3d	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to (\forall x \in Y \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U] \leftrightarrow \forall z \in {Base}_{S} \forall x \in U (F (z) +_{T} F (x)) -_{T} F (z) \in F [U])$
57	39 56	mpbird	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to \forall x \in Y \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U]$
58	1 24 21	isnsg3	$⊢ F [U] \in NrmSGrp (T) \leftrightarrow (F [U] \in SubGrp (T) \land \forall x \in Y \forall y \in F [U] (x +_{T} y) -_{T} x \in F [U])$
59	6 57 58	sylanbrc	$⊢ (F \in (S GrpHom T) \land U \in NrmSGrp (S) \land ran F = Y) \to F [U] \in NrmSGrp (T)$

Metamath Proof Explorer

Theorem ghmnsgima

Proof