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 
|- ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( `' F " V ) e. ( SubGrp ` S ) )

Proof

Step Hyp Ref Expression
1 cnvimass 
 |-  ( `' F " V ) C_ dom F
2 eqid 
 |-  ( Base ` S ) = ( Base ` S )
3 eqid 
 |-  ( Base ` T ) = ( Base ` T )
4 2 3 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
5 4 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
6 1 5 fssdm 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( `' F " V ) C_ ( Base ` S ) )
7 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
8 7 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> S e. Grp )
9 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
10 2 9 grpidcl 
 |-  ( S e. Grp -> ( 0g ` S ) e. ( Base ` S ) )
11 8 10 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( 0g ` S ) e. ( Base ` S ) )
12 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
13 9 12 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
14 13 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
15 12 subg0cl 
 |-  ( V e. ( SubGrp ` T ) -> ( 0g ` T ) e. V )
16 15 adantl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( 0g ` T ) e. V )
17 14 16 eqeltrd 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( F ` ( 0g ` S ) ) e. V )
18 5 ffnd 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> F Fn ( Base ` S ) )
19 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( ( 0g ` S ) e. ( `' F " V ) <-> ( ( 0g ` S ) e. ( Base ` S ) /\ ( F ` ( 0g ` S ) ) e. V ) ) )
20 18 19 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( ( 0g ` S ) e. ( `' F " V ) <-> ( ( 0g ` S ) e. ( Base ` S ) /\ ( F ` ( 0g ` S ) ) e. V ) ) )
21 11 17 20 mpbir2and 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( 0g ` S ) e. ( `' F " V ) )
22 21 ne0d 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( `' F " V ) =/= (/) )
23 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( a e. ( `' F " V ) <-> ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) )
24 18 23 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( a e. ( `' F " V ) <-> ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) )
25 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( b e. ( `' F " V ) <-> ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) )
26 18 25 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( b e. ( `' F " V ) <-> ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) )
27 26 adantr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( b e. ( `' F " V ) <-> ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) )
28 7 ad2antrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> S e. Grp )
29 simprll 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> a e. ( Base ` S ) )
30 simprrl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> b e. ( Base ` S ) )
31 eqid 
 |-  ( +g ` S ) = ( +g ` S )
32 2 31 grpcl 
 |-  ( ( S e. Grp /\ a e. ( Base ` S ) /\ b e. ( Base ` S ) ) -> ( a ( +g ` S ) b ) e. ( Base ` S ) )
33 28 29 30 32 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( a ( +g ` S ) b ) e. ( Base ` S ) )
34 simpll 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> F e. ( S GrpHom T ) )
35 eqid 
 |-  ( +g ` T ) = ( +g ` T )
36 2 31 35 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ a e. ( Base ` S ) /\ b e. ( Base ` S ) ) -> ( F ` ( a ( +g ` S ) b ) ) = ( ( F ` a ) ( +g ` T ) ( F ` b ) ) )
37 34 29 30 36 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( F ` ( a ( +g ` S ) b ) ) = ( ( F ` a ) ( +g ` T ) ( F ` b ) ) )
38 simplr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> V e. ( SubGrp ` T ) )
39 simprlr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( F ` a ) e. V )
40 simprrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( F ` b ) e. V )
41 35 subgcl 
 |-  ( ( V e. ( SubGrp ` T ) /\ ( F ` a ) e. V /\ ( F ` b ) e. V ) -> ( ( F ` a ) ( +g ` T ) ( F ` b ) ) e. V )
42 38 39 40 41 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( ( F ` a ) ( +g ` T ) ( F ` b ) ) e. V )
43 37 42 eqeltrd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( F ` ( a ( +g ` S ) b ) ) e. V )
44 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( ( a ( +g ` S ) b ) e. ( `' F " V ) <-> ( ( a ( +g ` S ) b ) e. ( Base ` S ) /\ ( F ` ( a ( +g ` S ) b ) ) e. V ) ) )
45 18 44 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( ( a ( +g ` S ) b ) e. ( `' F " V ) <-> ( ( a ( +g ` S ) b ) e. ( Base ` S ) /\ ( F ` ( a ( +g ` S ) b ) ) e. V ) ) )
46 45 adantr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( ( a ( +g ` S ) b ) e. ( `' F " V ) <-> ( ( a ( +g ` S ) b ) e. ( Base ` S ) /\ ( F ` ( a ( +g ` S ) b ) ) e. V ) ) )
47 33 43 46 mpbir2and 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) /\ ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) ) ) -> ( a ( +g ` S ) b ) e. ( `' F " V ) )
48 47 expr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( ( b e. ( Base ` S ) /\ ( F ` b ) e. V ) -> ( a ( +g ` S ) b ) e. ( `' F " V ) ) )
49 27 48 sylbid 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( b e. ( `' F " V ) -> ( a ( +g ` S ) b ) e. ( `' F " V ) ) )
50 49 ralrimiv 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) )
51 simprl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> a e. ( Base ` S ) )
52 eqid 
 |-  ( invg ` S ) = ( invg ` S )
53 2 52 grpinvcl 
 |-  ( ( S e. Grp /\ a e. ( Base ` S ) ) -> ( ( invg ` S ) ` a ) e. ( Base ` S ) )
54 8 51 53 syl2an2r 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( ( invg ` S ) ` a ) e. ( Base ` S ) )
55 eqid 
 |-  ( invg ` T ) = ( invg ` T )
56 2 52 55 ghminv 
 |-  ( ( F e. ( S GrpHom T ) /\ a e. ( Base ` S ) ) -> ( F ` ( ( invg ` S ) ` a ) ) = ( ( invg ` T ) ` ( F ` a ) ) )
57 56 ad2ant2r 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( F ` ( ( invg ` S ) ` a ) ) = ( ( invg ` T ) ` ( F ` a ) ) )
58 55 subginvcl 
 |-  ( ( V e. ( SubGrp ` T ) /\ ( F ` a ) e. V ) -> ( ( invg ` T ) ` ( F ` a ) ) e. V )
59 58 ad2ant2l 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( ( invg ` T ) ` ( F ` a ) ) e. V )
60 57 59 eqeltrd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( F ` ( ( invg ` S ) ` a ) ) e. V )
61 elpreima 
 |-  ( F Fn ( Base ` S ) -> ( ( ( invg ` S ) ` a ) e. ( `' F " V ) <-> ( ( ( invg ` S ) ` a ) e. ( Base ` S ) /\ ( F ` ( ( invg ` S ) ` a ) ) e. V ) ) )
62 18 61 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( ( ( invg ` S ) ` a ) e. ( `' F " V ) <-> ( ( ( invg ` S ) ` a ) e. ( Base ` S ) /\ ( F ` ( ( invg ` S ) ` a ) ) e. V ) ) )
63 62 adantr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( ( ( invg ` S ) ` a ) e. ( `' F " V ) <-> ( ( ( invg ` S ) ` a ) e. ( Base ` S ) /\ ( F ` ( ( invg ` S ) ` a ) ) e. V ) ) )
64 54 60 63 mpbir2and 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( ( invg ` S ) ` a ) e. ( `' F " V ) )
65 50 64 jca 
 |-  ( ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) /\ ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) ) -> ( A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) /\ ( ( invg ` S ) ` a ) e. ( `' F " V ) ) )
66 65 ex 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( ( a e. ( Base ` S ) /\ ( F ` a ) e. V ) -> ( A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) /\ ( ( invg ` S ) ` a ) e. ( `' F " V ) ) ) )
67 24 66 sylbid 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( a e. ( `' F " V ) -> ( A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) /\ ( ( invg ` S ) ` a ) e. ( `' F " V ) ) ) )
68 67 ralrimiv 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> A. a e. ( `' F " V ) ( A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) /\ ( ( invg ` S ) ` a ) e. ( `' F " V ) ) )
69 2 31 52 issubg2 
 |-  ( S e. Grp -> ( ( `' F " V ) e. ( SubGrp ` S ) <-> ( ( `' F " V ) C_ ( Base ` S ) /\ ( `' F " V ) =/= (/) /\ A. a e. ( `' F " V ) ( A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) /\ ( ( invg ` S ) ` a ) e. ( `' F " V ) ) ) ) )
70 8 69 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( ( `' F " V ) e. ( SubGrp ` S ) <-> ( ( `' F " V ) C_ ( Base ` S ) /\ ( `' F " V ) =/= (/) /\ A. a e. ( `' F " V ) ( A. b e. ( `' F " V ) ( a ( +g ` S ) b ) e. ( `' F " V ) /\ ( ( invg ` S ) ` a ) e. ( `' F " V ) ) ) ) )
71 6 22 68 70 mpbir3and 
 |-  ( ( F e. ( S GrpHom T ) /\ V e. ( SubGrp ` T ) ) -> ( `' F " V ) e. ( SubGrp ` S ) )