mhmeql

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

		Ref	Expression
	Assertion	mhmeql	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to dom (F \cap G) \in SubMnd (S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{S} = {Base}_{S}$
2		eqid	$⊢ {Base}_{T} = {Base}_{T}$
3	1 2	mhmf	$⊢ F \in (S MndHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
4	3	adantr	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
5	4	ffnd	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to F Fn {Base}_{S}$
6	1 2	mhmf	$⊢ G \in (S MndHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
7	6	adantl	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to G : {Base}_{S} ⟶ {Base}_{T}$
8	7	ffnd	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to G Fn {Base}_{S}$
9		fndmin	$⊢ (F Fn {Base}_{S} \land G Fn {Base}_{S}) \to dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\}$
10	5 8 9	syl2anc	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to dom (F \cap G) = \{z \in {Base}_{S} \| F (z) = G (z)\}$
11		ssrab2	$⊢ \{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S}$
12	11	a1i	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to \{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S}$
13		fveq2	$⊢ z = 0_{S} \to F (z) = F (0_{S})$
14		fveq2	$⊢ z = 0_{S} \to G (z) = G (0_{S})$
15	13 14	eqeq12d	$⊢ z = 0_{S} \to (F (z) = G (z) \leftrightarrow F (0_{S}) = G (0_{S}))$
16		mhmrcl1	$⊢ F \in (S MndHom T) \to S \in Mnd$
17	16	adantr	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to S \in Mnd$
18		eqid	$⊢ 0_{S} = 0_{S}$
19	1 18	mndidcl	$⊢ S \in Mnd \to 0_{S} \in {Base}_{S}$
20	17 19	syl	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to 0_{S} \in {Base}_{S}$
21		eqid	$⊢ 0_{T} = 0_{T}$
22	18 21	mhm0	$⊢ F \in (S MndHom T) \to F (0_{S}) = 0_{T}$
23	22	adantr	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to F (0_{S}) = 0_{T}$
24	18 21	mhm0	$⊢ G \in (S MndHom T) \to G (0_{S}) = 0_{T}$
25	24	adantl	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to G (0_{S}) = 0_{T}$
26	23 25	eqtr4d	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to F (0_{S}) = G (0_{S})$
27	15 20 26	elrabd	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to 0_{S} \in \{z \in {Base}_{S} \| F (z) = G (z)\}$
28		fveq2	$⊢ z = x +_{S} y \to F (z) = F (x +_{S} y)$
29		fveq2	$⊢ z = x +_{S} y \to G (z) = G (x +_{S} y)$
30	28 29	eqeq12d	$⊢ z = x +_{S} y \to (F (z) = G (z) \leftrightarrow F (x +_{S} y) = G (x +_{S} y))$
31	17	ad2antrr	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to S \in Mnd$
32		simplrl	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x \in {Base}_{S}$
33		simprl	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to y \in {Base}_{S}$
34		eqid	$⊢ +_{S} = +_{S}$
35	1 34	mndcl	$⊢ (S \in Mnd \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
36	31 32 33 35	syl3anc	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x +_{S} y \in {Base}_{S}$
37		simplll	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F \in (S MndHom T)$
38		eqid	$⊢ +_{T} = +_{T}$
39	1 34 38	mhmlin	$⊢ (F \in (S MndHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{T} F (y)$
40	37 32 33 39	syl3anc	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (x +_{S} y) = F (x) +_{T} F (y)$
41		simpllr	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to G \in (S MndHom T)$
42	1 34 38	mhmlin	$⊢ (G \in (S MndHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to G (x +_{S} y) = G (x) +_{T} G (y)$
43	41 32 33 42	syl3anc	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to G (x +_{S} y) = G (x) +_{T} G (y)$
44		simplrr	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (x) = G (x)$
45		simprr	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (y) = G (y)$
46	44 45	oveq12d	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (x) +_{T} F (y) = G (x) +_{T} G (y)$
47	43 46	eqtr4d	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to G (x +_{S} y) = F (x) +_{T} F (y)$
48	40 47	eqtr4d	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to F (x +_{S} y) = G (x +_{S} y)$
49	30 36 48	elrabd	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}$
50	49	expr	$⊢ (((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land y \in {Base}_{S}) \to (F (y) = G (y) \to x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
51	50	ralrimiva	$⊢ ((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to \forall y \in {Base}_{S} (F (y) = G (y) \to x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
52		fveq2	$⊢ z = y \to F (z) = F (y)$
53		fveq2	$⊢ z = y \to G (z) = G (y)$
54	52 53	eqeq12d	$⊢ z = y \to (F (z) = G (z) \leftrightarrow F (y) = G (y))$
55	54	ralrab	$⊢ \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\} \leftrightarrow \forall y \in {Base}_{S} (F (y) = G (y) \to x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
56	51 55	sylibr	$⊢ ((F \in (S MndHom T) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \to \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}$
57	56	expr	$⊢ ((F \in (S MndHom T) \land G \in (S MndHom T)) \land x \in {Base}_{S}) \to (F (x) = G (x) \to \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
58	57	ralrimiva	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to \forall x \in {Base}_{S} (F (x) = G (x) \to \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
59		fveq2	$⊢ z = x \to F (z) = F (x)$
60		fveq2	$⊢ z = x \to G (z) = G (x)$
61	59 60	eqeq12d	$⊢ z = x \to (F (z) = G (z) \leftrightarrow F (x) = G (x))$
62	61	ralrab	$⊢ \forall x \in \{z \in {Base}_{S} \| F (z) = G (z)\} \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\} \leftrightarrow \forall x \in {Base}_{S} (F (x) = G (x) \to \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\})$
63	58 62	sylibr	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to \forall x \in \{z \in {Base}_{S} \| F (z) = G (z)\} \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}$
64	1 18 34	issubm	$⊢ S \in Mnd \to (\{z \in {Base}_{S} \| F (z) = G (z)\} \in SubMnd (S) \leftrightarrow (\{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S} \land 0_{S} \in \{z \in {Base}_{S} \| F (z) = G (z)\} \land \forall x \in \{z \in {Base}_{S} \| F (z) = G (z)\} \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}))$
65	17 64	syl	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to (\{z \in {Base}_{S} \| F (z) = G (z)\} \in SubMnd (S) \leftrightarrow (\{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S} \land 0_{S} \in \{z \in {Base}_{S} \| F (z) = G (z)\} \land \forall x \in \{z \in {Base}_{S} \| F (z) = G (z)\} \forall y \in \{z \in {Base}_{S} \| F (z) = G (z)\} x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\}))$
66	12 27 63 65	mpbir3and	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to \{z \in {Base}_{S} \| F (z) = G (z)\} \in SubMnd (S)$
67	10 66	eqeltrd	$⊢ (F \in (S MndHom T) \land G \in (S MndHom T)) \to dom (F \cap G) \in SubMnd (S)$

Metamath Proof Explorer

Theorem mhmeql

Proof