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