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 ∈ S GrpHom T ∧ U ∈ NrmSGrp ⁡ S ∧ ran ⁡ F = Y → F U ∈ NrmSGrp ⁡ T

Proof

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