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 ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ran 𝐹 ∈ ( SubGrp ‘ 𝑇 ) )

Proof

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