Metamath Proof Explorer


Theorem ghmpreima

Description: The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion ghmpreima ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝐹𝑉 ) ∈ ( SubGrp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 cnvimass ( 𝐹𝑉 ) ⊆ dom 𝐹
2 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
3 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
4 2 3 ghmf ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
5 4 adantr ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
6 1 5 fssdm ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝐹𝑉 ) ⊆ ( Base ‘ 𝑆 ) )
7 ghmgrp1 ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
8 7 adantr ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝑆 ∈ Grp )
9 eqid ( 0g𝑆 ) = ( 0g𝑆 )
10 2 9 grpidcl ( 𝑆 ∈ Grp → ( 0g𝑆 ) ∈ ( Base ‘ 𝑆 ) )
11 8 10 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 0g𝑆 ) ∈ ( Base ‘ 𝑆 ) )
12 eqid ( 0g𝑇 ) = ( 0g𝑇 )
13 9 12 ghmid ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) )
14 13 adantr ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) )
15 12 subg0cl ( 𝑉 ∈ ( SubGrp ‘ 𝑇 ) → ( 0g𝑇 ) ∈ 𝑉 )
16 15 adantl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 0g𝑇 ) ∈ 𝑉 )
17 14 16 eqeltrd ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝐹 ‘ ( 0g𝑆 ) ) ∈ 𝑉 )
18 5 ffnd ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
19 elpreima ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( ( 0g𝑆 ) ∈ ( 𝐹𝑉 ) ↔ ( ( 0g𝑆 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 0g𝑆 ) ) ∈ 𝑉 ) ) )
20 18 19 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( ( 0g𝑆 ) ∈ ( 𝐹𝑉 ) ↔ ( ( 0g𝑆 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 0g𝑆 ) ) ∈ 𝑉 ) ) )
21 11 17 20 mpbir2and ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 0g𝑆 ) ∈ ( 𝐹𝑉 ) )
22 21 ne0d ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝐹𝑉 ) ≠ ∅ )
23 elpreima ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( 𝑎 ∈ ( 𝐹𝑉 ) ↔ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) )
24 18 23 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝑎 ∈ ( 𝐹𝑉 ) ↔ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) )
25 elpreima ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( 𝑏 ∈ ( 𝐹𝑉 ) ↔ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) )
26 18 25 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝑏 ∈ ( 𝐹𝑉 ) ↔ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) )
27 26 adantr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( 𝑏 ∈ ( 𝐹𝑉 ) ↔ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) )
28 7 ad2antrr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → 𝑆 ∈ Grp )
29 simprll ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
30 simprrl ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
31 eqid ( +g𝑆 ) = ( +g𝑆 )
32 2 31 grpcl ( ( 𝑆 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
33 28 29 30 32 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
34 simpll ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
35 eqid ( +g𝑇 ) = ( +g𝑇 )
36 2 31 35 ghmlin ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑆 ) 𝑏 ) ) = ( ( 𝐹𝑎 ) ( +g𝑇 ) ( 𝐹𝑏 ) ) )
37 34 29 30 36 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑆 ) 𝑏 ) ) = ( ( 𝐹𝑎 ) ( +g𝑇 ) ( 𝐹𝑏 ) ) )
38 simplr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → 𝑉 ∈ ( SubGrp ‘ 𝑇 ) )
39 simprlr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( 𝐹𝑎 ) ∈ 𝑉 )
40 simprrr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( 𝐹𝑏 ) ∈ 𝑉 )
41 35 subgcl ( ( 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) → ( ( 𝐹𝑎 ) ( +g𝑇 ) ( 𝐹𝑏 ) ) ∈ 𝑉 )
42 38 39 40 41 syl3anc ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( ( 𝐹𝑎 ) ( +g𝑇 ) ( 𝐹𝑏 ) ) ∈ 𝑉 )
43 37 42 eqeltrd ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑆 ) 𝑏 ) ) ∈ 𝑉 )
44 elpreima ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ↔ ( ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑎 ( +g𝑆 ) 𝑏 ) ) ∈ 𝑉 ) ) )
45 18 44 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ↔ ( ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑎 ( +g𝑆 ) 𝑏 ) ) ∈ 𝑉 ) ) )
46 45 adantr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ↔ ( ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑎 ( +g𝑆 ) 𝑏 ) ) ∈ 𝑉 ) ) )
47 33 43 46 mpbir2and ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ∧ ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) ) ) → ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) )
48 47 expr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( ( 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑏 ) ∈ 𝑉 ) → ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ) )
49 27 48 sylbid ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( 𝑏 ∈ ( 𝐹𝑉 ) → ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ) )
50 49 ralrimiv ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) )
51 simprl ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
52 eqid ( invg𝑆 ) = ( invg𝑆 )
53 2 52 grpinvcl ( ( 𝑆 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ) → ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) )
54 8 51 53 syl2an2r ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) )
55 eqid ( invg𝑇 ) = ( invg𝑇 )
56 2 52 55 ghminv ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( invg𝑆 ) ‘ 𝑎 ) ) = ( ( invg𝑇 ) ‘ ( 𝐹𝑎 ) ) )
57 56 ad2ant2r ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( invg𝑆 ) ‘ 𝑎 ) ) = ( ( invg𝑇 ) ‘ ( 𝐹𝑎 ) ) )
58 55 subginvcl ( ( 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) → ( ( invg𝑇 ) ‘ ( 𝐹𝑎 ) ) ∈ 𝑉 )
59 58 ad2ant2l ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( ( invg𝑇 ) ‘ ( 𝐹𝑎 ) ) ∈ 𝑉 )
60 57 59 eqeltrd ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( invg𝑆 ) ‘ 𝑎 ) ) ∈ 𝑉 )
61 elpreima ( 𝐹 Fn ( Base ‘ 𝑆 ) → ( ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ↔ ( ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( ( invg𝑆 ) ‘ 𝑎 ) ) ∈ 𝑉 ) ) )
62 18 61 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ↔ ( ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( ( invg𝑆 ) ‘ 𝑎 ) ) ∈ 𝑉 ) ) )
63 62 adantr ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ↔ ( ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( ( invg𝑆 ) ‘ 𝑎 ) ) ∈ 𝑉 ) ) )
64 54 60 63 mpbir2and ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) )
65 50 64 jca ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) ) → ( ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ∧ ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ) )
66 65 ex ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑎 ) ∈ 𝑉 ) → ( ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ∧ ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ) ) )
67 24 66 sylbid ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝑎 ∈ ( 𝐹𝑉 ) → ( ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ∧ ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ) ) )
68 67 ralrimiv ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ∀ 𝑎 ∈ ( 𝐹𝑉 ) ( ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ∧ ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ) )
69 2 31 52 issubg2 ( 𝑆 ∈ Grp → ( ( 𝐹𝑉 ) ∈ ( SubGrp ‘ 𝑆 ) ↔ ( ( 𝐹𝑉 ) ⊆ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑉 ) ≠ ∅ ∧ ∀ 𝑎 ∈ ( 𝐹𝑉 ) ( ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ∧ ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ) ) ) )
70 8 69 syl ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( ( 𝐹𝑉 ) ∈ ( SubGrp ‘ 𝑆 ) ↔ ( ( 𝐹𝑉 ) ⊆ ( Base ‘ 𝑆 ) ∧ ( 𝐹𝑉 ) ≠ ∅ ∧ ∀ 𝑎 ∈ ( 𝐹𝑉 ) ( ∀ 𝑏 ∈ ( 𝐹𝑉 ) ( 𝑎 ( +g𝑆 ) 𝑏 ) ∈ ( 𝐹𝑉 ) ∧ ( ( invg𝑆 ) ‘ 𝑎 ) ∈ ( 𝐹𝑉 ) ) ) ) )
71 6 22 68 70 mpbir3and ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑉 ∈ ( SubGrp ‘ 𝑇 ) ) → ( 𝐹𝑉 ) ∈ ( SubGrp ‘ 𝑆 ) )