ghmpreima

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

		Ref	Expression
	Assertion	ghmpreima	$⊢ (F \in (S GrpHom T) \land V \in SubGrp (T)) \to F^{-1} [V] \in SubGrp (S)$

Proof

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

Metamath Proof Explorer

Theorem ghmpreima

Proof