ghmnsgpreima

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

		Ref	Expression
	Assertion	ghmnsgpreima	$⊢ (F \in (S GrpHom T) \land V \in NrmSGrp (T)) \to F^{-1} [V] \in NrmSGrp (S)$

Proof

Step	Hyp	Ref	Expression
1		nsgsubg	$⊢ V \in NrmSGrp (T) \to V \in SubGrp (T)$
2		ghmpreima	$⊢ (F \in (S GrpHom T) \land V \in SubGrp (T)) \to F^{-1} [V] \in SubGrp (S)$
3	1 2	sylan2	$⊢ (F \in (S GrpHom T) \land V \in NrmSGrp (T)) \to F^{-1} [V] \in SubGrp (S)$
4		ghmgrp1	$⊢ F \in (S GrpHom T) \to S \in Grp$
5	4	ad2antrr	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to S \in Grp$
6		simprl	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to x \in {Base}_{S}$
7		simprr	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to y \in F^{-1} [V]$
8		simpll	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F \in (S GrpHom T)$
9		eqid	$⊢ {Base}_{S} = {Base}_{S}$
10		eqid	$⊢ {Base}_{T} = {Base}_{T}$
11	9 10	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
12	8 11	syl	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F : {Base}_{S} ⟶ {Base}_{T}$
13	12	ffnd	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F Fn {Base}_{S}$
14		elpreima	$⊢ F Fn {Base}_{S} \to (y \in F^{-1} [V] \leftrightarrow (y \in {Base}_{S} \land F (y) \in V))$
15	13 14	syl	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to (y \in F^{-1} [V] \leftrightarrow (y \in {Base}_{S} \land F (y) \in V))$
16	7 15	mpbid	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to (y \in {Base}_{S} \land F (y) \in V)$
17	16	simpld	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to y \in {Base}_{S}$
18		eqid	$⊢ +_{S} = +_{S}$
19	9 18	grpcl	$⊢ (S \in Grp \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
20	5 6 17 19	syl3anc	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to x +_{S} y \in {Base}_{S}$
21		eqid	$⊢ -_{S} = -_{S}$
22	9 21	grpsubcl	$⊢ (S \in Grp \land x +_{S} y \in {Base}_{S} \land x \in {Base}_{S}) \to (x +_{S} y) -_{S} x \in {Base}_{S}$
23	5 20 6 22	syl3anc	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to (x +_{S} y) -_{S} x \in {Base}_{S}$
24		eqid	$⊢ -_{T} = -_{T}$
25	9 21 24	ghmsub	$⊢ (F \in (S GrpHom T) \land x +_{S} y \in {Base}_{S} \land x \in {Base}_{S}) \to F ((x +_{S} y) -_{S} x) = F (x +_{S} y) -_{T} F (x)$
26	8 20 6 25	syl3anc	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F ((x +_{S} y) -_{S} x) = F (x +_{S} y) -_{T} F (x)$
27		eqid	$⊢ +_{T} = +_{T}$
28	9 18 27	ghmlin	$⊢ (F \in (S GrpHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{T} F (y)$
29	8 6 17 28	syl3anc	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F (x +_{S} y) = F (x) +_{T} F (y)$
30	29	oveq1d	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F (x +_{S} y) -_{T} F (x) = (F (x) +_{T} F (y)) -_{T} F (x)$
31	26 30	eqtrd	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F ((x +_{S} y) -_{S} x) = (F (x) +_{T} F (y)) -_{T} F (x)$
32		simplr	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to V \in NrmSGrp (T)$
33	12 6	ffvelcdmd	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F (x) \in {Base}_{T}$
34	16	simprd	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F (y) \in V$
35	10 27 24	nsgconj	$⊢ (V \in NrmSGrp (T) \land F (x) \in {Base}_{T} \land F (y) \in V) \to (F (x) +_{T} F (y)) -_{T} F (x) \in V$
36	32 33 34 35	syl3anc	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to (F (x) +_{T} F (y)) -_{T} F (x) \in V$
37	31 36	eqeltrd	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to F ((x +_{S} y) -_{S} x) \in V$
38		elpreima	$⊢ F Fn {Base}_{S} \to ((x +_{S} y) -_{S} x \in F^{-1} [V] \leftrightarrow ((x +_{S} y) -_{S} x \in {Base}_{S} \land F ((x +_{S} y) -_{S} x) \in V))$
39	13 38	syl	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to ((x +_{S} y) -_{S} x \in F^{-1} [V] \leftrightarrow ((x +_{S} y) -_{S} x \in {Base}_{S} \land F ((x +_{S} y) -_{S} x) \in V))$
40	23 37 39	mpbir2and	$⊢ ((F \in (S GrpHom T) \land V \in NrmSGrp (T)) \land (x \in {Base}_{S} \land y \in F^{-1} [V])) \to (x +_{S} y) -_{S} x \in F^{-1} [V]$
41	40	ralrimivva	$⊢ (F \in (S GrpHom T) \land V \in NrmSGrp (T)) \to \forall x \in {Base}_{S} \forall y \in F^{-1} [V] (x +_{S} y) -_{S} x \in F^{-1} [V]$
42	9 18 21	isnsg3	$⊢ F^{-1} [V] \in NrmSGrp (S) \leftrightarrow (F^{-1} [V] \in SubGrp (S) \land \forall x \in {Base}_{S} \forall y \in F^{-1} [V] (x +_{S} y) -_{S} x \in F^{-1} [V])$
43	3 41 42	sylanbrc	$⊢ (F \in (S GrpHom T) \land V \in NrmSGrp (T)) \to F^{-1} [V] \in NrmSGrp (S)$

Metamath Proof Explorer

Theorem ghmnsgpreima

Proof