This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( Base ‘ 𝑇 )
Assertion ghmnsgima ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ ( NrmSGrp ‘ 𝑆 ) ∧ ran 𝐹 = 𝑌 ) → ( 𝐹 “ 𝑈 ) ∈ ( NrmSGrp ‘ 𝑇 ) )

Proof

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