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 e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) -> ( `' F " V ) e. ( NrmSGrp ` S ) )

Proof

Step Hyp Ref Expression
1 nsgsubg 
 |-  ( V e. ( NrmSGrp ` T ) -> V e. ( SubGrp ` T ) )
2 ghmpreima 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( `' F " V ) e. ( SubGrp ` S ) )
3 1 2 sylan2 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) -> ( `' F " V ) e. ( SubGrp ` S ) )
4 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
5 4 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> S e. Grp )
6 simprl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> x e. ( Base ` S ) )
7 simprr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> y e. ( `' F " V ) )
8 simpll 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> F e. ( S GrpHom T ) )
9 eqid 
 |-  ( Base ` S ) = ( Base ` S )
10 eqid 
 |-  ( Base ` T ) = ( Base ` T )
11 9 10 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
12 8 11 syl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
13 12 ffnd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> F Fn ( Base ` S ) )
14 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( y e. ( `' F " V ) <-> ( y e. ( Base ` S ) /\ ( F ` y ) e. V ) ) )
15 13 14 syl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( y e. ( `' F " V ) <-> ( y e. ( Base ` S ) /\ ( F ` y ) e. V ) ) )
16 7 15 mpbid 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( y e. ( Base ` S ) /\ ( F ` y ) e. V ) )
17 16 simpld 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> y e. ( Base ` S ) )
18 eqid 
 |-  ( +g ` S ) = ( +g ` S )
19 9 18 grpcl 
 |-  ( ( S e. Grp /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
20 5 6 17 19 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
21 eqid 
 |-  ( -g ` S ) = ( -g ` S )
22 9 21 grpsubcl 
 |-  ( ( S e. Grp /\ ( x ( +g ` S ) y ) e. ( Base ` S ) /\ x e. ( Base ` S ) ) -> ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( Base ` S ) )
23 5 20 6 22 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( Base ` S ) )
24 eqid 
 |-  ( -g ` T ) = ( -g ` T )
25 9 21 24 ghmsub 
 |-  ( ( F e. ( S GrpHom T ) /\ ( x ( +g ` S ) y ) e. ( Base ` S ) /\ x e. ( Base ` S ) ) -> ( F ` ( ( x ( +g ` S ) y ) ( -g ` S ) x ) ) = ( ( F ` ( x ( +g ` S ) y ) ) ( -g ` T ) ( F ` x ) ) )
26 8 20 6 25 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( F ` ( ( x ( +g ` S ) y ) ( -g ` S ) x ) ) = ( ( F ` ( x ( +g ` S ) y ) ) ( -g ` T ) ( F ` x ) ) )
27 eqid 
 |-  ( +g ` T ) = ( +g ` T )
28 9 18 27 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
29 8 6 17 28 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
30 29 oveq1d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( ( F ` ( x ( +g ` S ) y ) ) ( -g ` T ) ( F ` x ) ) = ( ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ( -g ` T ) ( F ` x ) ) )
31 26 30 eqtrd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( F ` ( ( x ( +g ` S ) y ) ( -g ` S ) x ) ) = ( ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ( -g ` T ) ( F ` x ) ) )
32 simplr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> V e. ( NrmSGrp ` T ) )
33 12 6 ffvelrnd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( F ` x ) e. ( Base ` T ) )
34 16 simprd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( F ` y ) e. V )
35 10 27 24 nsgconj 
 |-  ( ( V e. ( NrmSGrp ` T ) /\ ( F ` x ) e. ( Base ` T ) /\ ( F ` y ) e. V ) -> ( ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ( -g ` T ) ( F ` x ) ) e. V )
36 32 33 34 35 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ( -g ` T ) ( F ` x ) ) e. V )
37 31 36 eqeltrd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( F ` ( ( x ( +g ` S ) y ) ( -g ` S ) x ) ) e. V )
38 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( `' F " V ) <-> ( ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( Base ` S ) /\ ( F ` ( ( x ( +g ` S ) y ) ( -g ` S ) x ) ) e. V ) ) )
39 13 38 syl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( `' F " V ) <-> ( ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( Base ` S ) /\ ( F ` ( ( x ( +g ` S ) y ) ( -g ` S ) x ) ) e. V ) ) )
40 23 37 39 mpbir2and 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( `' F " V ) ) ) -> ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( `' F " V ) )
41 40 ralrimivva 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) -> A. x e. ( Base ` S ) A. y e. ( `' F " V ) ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( `' F " V ) )
42 9 18 21 isnsg3 
 |-  ( ( `' F " V ) e. ( NrmSGrp ` S ) <-> ( ( `' F " V ) e. ( SubGrp ` S ) /\ A. x e. ( Base ` S ) A. y e. ( `' F " V ) ( ( x ( +g ` S ) y ) ( -g ` S ) x ) e. ( `' F " V ) ) )
43 3 41 42 sylanbrc 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( NrmSGrp ` T ) ) -> ( `' F " V ) e. ( NrmSGrp ` S ) )