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 ffvelrnd 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