ghmeql

Description: The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	ghmeql	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to dom (F \cap G) \in SubGrp (S)$

Proof

Step	Hyp	Ref	Expression
1		ghmmhm	$⊢ F \in (S GrpHom T) \to F \in (S MndHom T)$
2		ghmmhm	$⊢ G \in (S GrpHom T) \to G \in (S MndHom T)$
3		mhmeql	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to dom (F \cap G) \in SubMnd (S)$
4	1 2 3	syl2an	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to dom (F \cap G) \in SubMnd (S)$
5		fveq2	$⊢ y = {inv}_{g} (S) (x) \to F (y) = F ({inv}_{g} (S) (x))$
6		fveq2	$⊢ y = {inv}_{g} (S) (x) \to G (y) = G ({inv}_{g} (S) (x))$
7	5 6	eqeq12d	$⊢ y = {inv}_{g} (S) (x) \to (F (y) = G (y) \leftrightarrow F ({inv}_{g} (S) (x)) = G ({inv}_{g} (S) (x)))$
8		ghmgrp1	$⊢ F \in (S GrpHom T) \to S \in Grp$
9	8	adantr	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to S \in Grp$
10	9	adantr	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to S \in Grp$
11		simprl	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to x \in {Base}_{S}$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
14	12 13	grpinvcl	$⊢ (S \in Grp \land x \in {Base}_{S}) \to {inv}_{g} (S) (x) \in {Base}_{S}$
15	10 11 14	syl2anc	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to {inv}_{g} (S) (x) \in {Base}_{S}$
16		simprr	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to F (x) = G (x)$
17	16	fveq2d	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to {inv}_{g} (T) (F (x)) = {inv}_{g} (T) (G (x))$
18		eqid	$⊢ {inv}_{g} (T) = {inv}_{g} (T)$
19	12 13 18	ghminv	$⊢ (F \in (S GrpHom T) \land x \in {Base}_{S}) \to F ({inv}_{g} (S) (x)) = {inv}_{g} (T) (F (x))$
20	19	ad2ant2r	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to F ({inv}_{g} (S) (x)) = {inv}_{g} (T) (F (x))$
21	12 13 18	ghminv	$⊢ (G \in (S GrpHom T) \land x \in {Base}_{S}) \to G ({inv}_{g} (S) (x)) = {inv}_{g} (T) (G (x))$
22	21	ad2ant2lr	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to G ({inv}_{g} (S) (x)) = {inv}_{g} (T) (G (x))$
23	17 20 22	3eqtr4d	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to F ({inv}_{g} (S) (x)) = G ({inv}_{g} (S) (x))$
24	7 15 23	elrabd	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\}$
25	24	expr	$⊢ ((F \in (S GrpHom T) \land G \in (S GrpHom T)) \land x \in {Base}_{S}) \to (F (x) = G (x) \to {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\})$
26	25	ralrimiva	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to \forall x \in {Base}_{S} (F (x) = G (x) \to {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\})$
27		fveq2	$⊢ y = x \to F (y) = F (x)$
28		fveq2	$⊢ y = x \to G (y) = G (x)$
29	27 28	eqeq12d	$⊢ y = x \to (F (y) = G (y) \leftrightarrow F (x) = G (x))$
30	29	ralrab	$⊢ \forall x \in \{y \in {Base}_{S} \| F (y) = G (y)\} {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\} \leftrightarrow \forall x \in {Base}_{S} (F (x) = G (x) \to {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\})$
31	26 30	sylibr	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to \forall x \in \{y \in {Base}_{S} \| F (y) = G (y)\} {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\}$
32		eqid	$⊢ {Base}_{T} = {Base}_{T}$
33	12 32	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
34	33	adantr	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
35	34	ffnd	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to F Fn {Base}_{S}$
36	12 32	ghmf	$⊢ G \in (S GrpHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
37	36	adantl	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to G : {Base}_{S} ⟶ {Base}_{T}$
38	37	ffnd	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to G Fn {Base}_{S}$
39		fndmin	$⊢ (F Fn {Base}_{S} \land G Fn {Base}_{S}) \to dom (F \cap G) = \{y \in {Base}_{S} \| F (y) = G (y)\}$
40	35 38 39	syl2anc	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to dom (F \cap G) = \{y \in {Base}_{S} \| F (y) = G (y)\}$
41		eleq2	$⊢ dom (F \cap G) = \{y \in {Base}_{S} \| F (y) = G (y)\} \to ({inv}_{g} (S) (x) \in dom (F \cap G) \leftrightarrow {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\})$
42	41	raleqbi1dv	$⊢ dom (F \cap G) = \{y \in {Base}_{S} \| F (y) = G (y)\} \to (\forall x \in dom (F \cap G) {inv}_{g} (S) (x) \in dom (F \cap G) \leftrightarrow \forall x \in \{y \in {Base}_{S} \| F (y) = G (y)\} {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\})$
43	40 42	syl	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to (\forall x \in dom (F \cap G) {inv}_{g} (S) (x) \in dom (F \cap G) \leftrightarrow \forall x \in \{y \in {Base}_{S} \| F (y) = G (y)\} {inv}_{g} (S) (x) \in \{y \in {Base}_{S} \| F (y) = G (y)\})$
44	31 43	mpbird	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to \forall x \in dom (F \cap G) {inv}_{g} (S) (x) \in dom (F \cap G)$
45	13	issubg3	$⊢ S \in Grp \to (dom (F \cap G) \in SubGrp (S) \leftrightarrow (dom (F \cap G) \in SubMnd (S) \land \forall x \in dom (F \cap G) {inv}_{g} (S) (x) \in dom (F \cap G)))$
46	9 45	syl	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to (dom (F \cap G) \in SubGrp (S) \leftrightarrow (dom (F \cap G) \in SubMnd (S) \land \forall x \in dom (F \cap G) {inv}_{g} (S) (x) \in dom (F \cap G)))$
47	4 44 46	mpbir2and	$⊢ (F \in (S GrpHom T) \land G \in (S GrpHom T)) \to dom (F \cap G) \in SubGrp (S)$

Metamath Proof Explorer

Theorem ghmeql

Proof