Metamath Proof Explorer

Theorem ghmrn

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

Ref Expression
Assertion ghmrn ⊢ F ∈ S GrpHom T → ran ⁡ F ∈ SubGrp ⁡ T

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base S = Base S
2 eqid ⊢ Base T = Base T
3 1 2 ghmf ⊢ F ∈ S GrpHom T → F : Base S ⟶ Base T
4 3 frnd ⊢ F ∈ S GrpHom T → ran ⁡ F ⊆ Base T
5 3 fdmd ⊢ F ∈ S GrpHom T → dom ⁡ F = Base S
6 ghmgrp1 ⊢ F ∈ S GrpHom T → S ∈ Grp
7 1 grpbn0 ⊢ S ∈ Grp → Base S ≠ ∅
8 6 7 syl ⊢ F ∈ S GrpHom T → Base S ≠ ∅
9 5 8 eqnetrd ⊢ F ∈ S GrpHom T → dom ⁡ F ≠ ∅
10 dm0rn0 ⊢ dom ⁡ F = ∅ ↔ ran ⁡ F = ∅
11 10 necon3bii ⊢ dom ⁡ F ≠ ∅ ↔ ran ⁡ F ≠ ∅
12 9 11 sylib ⊢ F ∈ S GrpHom T → ran ⁡ F ≠ ∅
13 eqid ⊢ + S = + S
14 eqid ⊢ + T = + T
15 1 13 14 ghmlin ⊢ F ∈ S GrpHom T ∧ c ∈ Base S ∧ a ∈ Base S → F ⁡ c + S a = F ⁡ c + T F ⁡ a
16 3 ffnd ⊢ F ∈ S GrpHom T → F Fn Base S
17 16 3ad2ant1 ⊢ F ∈ S GrpHom T ∧ c ∈ Base S ∧ a ∈ Base S → F Fn Base S
18 1 13 grpcl ⊢ S ∈ Grp ∧ c ∈ Base S ∧ a ∈ Base S → c + S a ∈ Base S
19 6 18 syl3an1 ⊢ F ∈ S GrpHom T ∧ c ∈ Base S ∧ a ∈ Base S → c + S a ∈ Base S
20 fnfvelrn ⊢ F Fn Base S ∧ c + S a ∈ Base S → F ⁡ c + S a ∈ ran ⁡ F
21 17 19 20 syl2anc ⊢ F ∈ S GrpHom T ∧ c ∈ Base S ∧ a ∈ Base S → F ⁡ c + S a ∈ ran ⁡ F
22 15 21 eqeltrrd ⊢ F ∈ S GrpHom T ∧ c ∈ Base S ∧ a ∈ Base S → F ⁡ c + T F ⁡ a ∈ ran ⁡ F
23 22 3expia ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → a ∈ Base S → F ⁡ c + T F ⁡ a ∈ ran ⁡ F
24 23 ralrimiv ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → ∀ a ∈ Base S F ⁡ c + T F ⁡ a ∈ ran ⁡ F
25 oveq2 ⊢ b = F ⁡ a → F ⁡ c + T b = F ⁡ c + T F ⁡ a
26 25 eleq1d ⊢ b = F ⁡ a → F ⁡ c + T b ∈ ran ⁡ F ↔ F ⁡ c + T F ⁡ a ∈ ran ⁡ F
27 26 ralrn ⊢ F Fn Base S → ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ↔ ∀ a ∈ Base S F ⁡ c + T F ⁡ a ∈ ran ⁡ F
28 16 27 syl ⊢ F ∈ S GrpHom T → ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ↔ ∀ a ∈ Base S F ⁡ c + T F ⁡ a ∈ ran ⁡ F
29 28 adantr ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ↔ ∀ a ∈ Base S F ⁡ c + T F ⁡ a ∈ ran ⁡ F
30 24 29 mpbird ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F
31 eqid ⊢ inv g ⁡ S = inv g ⁡ S
32 eqid ⊢ inv g ⁡ T = inv g ⁡ T
33 1 31 32 ghminv ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → F ⁡ inv g ⁡ S ⁡ c = inv g ⁡ T ⁡ F ⁡ c
34 16 adantr ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → F Fn Base S
35 1 31 grpinvcl ⊢ S ∈ Grp ∧ c ∈ Base S → inv g ⁡ S ⁡ c ∈ Base S
36 6 35 sylan ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → inv g ⁡ S ⁡ c ∈ Base S
37 fnfvelrn ⊢ F Fn Base S ∧ inv g ⁡ S ⁡ c ∈ Base S → F ⁡ inv g ⁡ S ⁡ c ∈ ran ⁡ F
38 34 36 37 syl2anc ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → F ⁡ inv g ⁡ S ⁡ c ∈ ran ⁡ F
39 33 38 eqeltrrd ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
40 30 39 jca ⊢ F ∈ S GrpHom T ∧ c ∈ Base S → ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
41 40 ralrimiva ⊢ F ∈ S GrpHom T → ∀ c ∈ Base S ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
42 oveq1 ⊢ a = F ⁡ c → a + T b = F ⁡ c + T b
43 42 eleq1d ⊢ a = F ⁡ c → a + T b ∈ ran ⁡ F ↔ F ⁡ c + T b ∈ ran ⁡ F
44 43 ralbidv ⊢ a = F ⁡ c → ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ↔ ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F
45 fveq2 ⊢ a = F ⁡ c → inv g ⁡ T ⁡ a = inv g ⁡ T ⁡ F ⁡ c
46 45 eleq1d ⊢ a = F ⁡ c → inv g ⁡ T ⁡ a ∈ ran ⁡ F ↔ inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
47 44 46 anbi12d ⊢ a = F ⁡ c → ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ a ∈ ran ⁡ F ↔ ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
48 47 ralrn ⊢ F Fn Base S → ∀ a ∈ ran ⁡ F ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ a ∈ ran ⁡ F ↔ ∀ c ∈ Base S ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
49 16 48 syl ⊢ F ∈ S GrpHom T → ∀ a ∈ ran ⁡ F ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ a ∈ ran ⁡ F ↔ ∀ c ∈ Base S ∀ b ∈ ran ⁡ F F ⁡ c + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ F ⁡ c ∈ ran ⁡ F
50 41 49 mpbird ⊢ F ∈ S GrpHom T → ∀ a ∈ ran ⁡ F ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ a ∈ ran ⁡ F
51 ghmgrp2 ⊢ F ∈ S GrpHom T → T ∈ Grp
52 2 14 32 issubg2 ⊢ T ∈ Grp → ran ⁡ F ∈ SubGrp ⁡ T ↔ ran ⁡ F ⊆ Base T ∧ ran ⁡ F ≠ ∅ ∧ ∀ a ∈ ran ⁡ F ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ a ∈ ran ⁡ F
53 51 52 syl ⊢ F ∈ S GrpHom T → ran ⁡ F ∈ SubGrp ⁡ T ↔ ran ⁡ F ⊆ Base T ∧ ran ⁡ F ≠ ∅ ∧ ∀ a ∈ ran ⁡ F ∀ b ∈ ran ⁡ F a + T b ∈ ran ⁡ F ∧ inv g ⁡ T ⁡ a ∈ ran ⁡ F
54 4 12 50 53 mpbir3and ⊢ F ∈ S GrpHom T → ran ⁡ F ∈ SubGrp ⁡ T