ghmrn

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

		Ref	Expression
	Assertion	ghmrn	$⊢ F \in (S GrpHom T) \to ran F \in SubGrp (T)$

Proof

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

Metamath Proof Explorer

Theorem ghmrn

Proof