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 ‘ 𝑆 ) )