Metamath Proof Explorer

Theorem 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 ∈ S GrpHom T ∧ V ∈ NrmSGrp ⁡ T → F -1 V ∈ NrmSGrp ⁡ S

Proof

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