Metamath Proof Explorer


Theorem ghmf1

Description: Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses ghmf1.x X = Base S
ghmf1.y Y = Base T
ghmf1.z 0 ˙ = 0 S
ghmf1.u U = 0 T
Assertion ghmf1 F S GrpHom T F : X 1-1 Y x X F x = U x = 0 ˙

Proof

Step Hyp Ref Expression
1 ghmf1.x X = Base S
2 ghmf1.y Y = Base T
3 ghmf1.z 0 ˙ = 0 S
4 ghmf1.u U = 0 T
5 3 4 ghmid F S GrpHom T F 0 ˙ = U
6 5 ad2antrr F S GrpHom T F : X 1-1 Y x X F 0 ˙ = U
7 6 eqeq2d F S GrpHom T F : X 1-1 Y x X F x = F 0 ˙ F x = U
8 simplr F S GrpHom T F : X 1-1 Y x X F : X 1-1 Y
9 simpr F S GrpHom T F : X 1-1 Y x X x X
10 ghmgrp1 F S GrpHom T S Grp
11 10 ad2antrr F S GrpHom T F : X 1-1 Y x X S Grp
12 1 3 grpidcl S Grp 0 ˙ X
13 11 12 syl F S GrpHom T F : X 1-1 Y x X 0 ˙ X
14 f1fveq F : X 1-1 Y x X 0 ˙ X F x = F 0 ˙ x = 0 ˙
15 8 9 13 14 syl12anc F S GrpHom T F : X 1-1 Y x X F x = F 0 ˙ x = 0 ˙
16 7 15 bitr3d F S GrpHom T F : X 1-1 Y x X F x = U x = 0 ˙
17 16 biimpd F S GrpHom T F : X 1-1 Y x X F x = U x = 0 ˙
18 17 ralrimiva F S GrpHom T F : X 1-1 Y x X F x = U x = 0 ˙
19 1 2 ghmf F S GrpHom T F : X Y
20 19 adantr F S GrpHom T x X F x = U x = 0 ˙ F : X Y
21 eqid - S = - S
22 eqid - T = - T
23 1 21 22 ghmsub F S GrpHom T y X z X F y - S z = F y - T F z
24 23 3expb F S GrpHom T y X z X F y - S z = F y - T F z
25 24 adantlr F S GrpHom T x X F x = U x = 0 ˙ y X z X F y - S z = F y - T F z
26 25 eqeq1d F S GrpHom T x X F x = U x = 0 ˙ y X z X F y - S z = U F y - T F z = U
27 fveqeq2 x = y - S z F x = U F y - S z = U
28 eqeq1 x = y - S z x = 0 ˙ y - S z = 0 ˙
29 27 28 imbi12d x = y - S z F x = U x = 0 ˙ F y - S z = U y - S z = 0 ˙
30 simplr F S GrpHom T x X F x = U x = 0 ˙ y X z X x X F x = U x = 0 ˙
31 10 adantr F S GrpHom T x X F x = U x = 0 ˙ S Grp
32 1 21 grpsubcl S Grp y X z X y - S z X
33 32 3expb S Grp y X z X y - S z X
34 31 33 sylan F S GrpHom T x X F x = U x = 0 ˙ y X z X y - S z X
35 29 30 34 rspcdva F S GrpHom T x X F x = U x = 0 ˙ y X z X F y - S z = U y - S z = 0 ˙
36 26 35 sylbird F S GrpHom T x X F x = U x = 0 ˙ y X z X F y - T F z = U y - S z = 0 ˙
37 ghmgrp2 F S GrpHom T T Grp
38 37 ad2antrr F S GrpHom T x X F x = U x = 0 ˙ y X z X T Grp
39 19 ad2antrr F S GrpHom T x X F x = U x = 0 ˙ y X z X F : X Y
40 simprl F S GrpHom T x X F x = U x = 0 ˙ y X z X y X
41 39 40 ffvelrnd F S GrpHom T x X F x = U x = 0 ˙ y X z X F y Y
42 simprr F S GrpHom T x X F x = U x = 0 ˙ y X z X z X
43 39 42 ffvelrnd F S GrpHom T x X F x = U x = 0 ˙ y X z X F z Y
44 2 4 22 grpsubeq0 T Grp F y Y F z Y F y - T F z = U F y = F z
45 38 41 43 44 syl3anc F S GrpHom T x X F x = U x = 0 ˙ y X z X F y - T F z = U F y = F z
46 10 ad2antrr F S GrpHom T x X F x = U x = 0 ˙ y X z X S Grp
47 1 3 21 grpsubeq0 S Grp y X z X y - S z = 0 ˙ y = z
48 46 40 42 47 syl3anc F S GrpHom T x X F x = U x = 0 ˙ y X z X y - S z = 0 ˙ y = z
49 36 45 48 3imtr3d F S GrpHom T x X F x = U x = 0 ˙ y X z X F y = F z y = z
50 49 ralrimivva F S GrpHom T x X F x = U x = 0 ˙ y X z X F y = F z y = z
51 dff13 F : X 1-1 Y F : X Y y X z X F y = F z y = z
52 20 50 51 sylanbrc F S GrpHom T x X F x = U x = 0 ˙ F : X 1-1 Y
53 18 52 impbida F S GrpHom T F : X 1-1 Y x X F x = U x = 0 ˙