Metamath Proof Explorer

Theorem 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 e. ( S GrpHom T ) /\ U e. ( NrmSGrp ` S ) /\ ran F = Y ) -> ( F " U ) e. ( NrmSGrp ` T ) )

Proof

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