mgmhmeql

Description: The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020)

		Ref	Expression
	Assertion	mgmhmeql	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to dom (F \cap G) \in SubMgm (S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{S} = {Base}_{S}$
2		eqid	$⊢ {Base}_{T} = {Base}_{T}$
3	1 2	mgmhmf	$⊢ F \in (S MgmHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
4	3	adantr	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
5	4	ffnd	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to F Fn {Base}_{S}$
6	1 2	mgmhmf	$⊢ G \in (S MgmHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
7	6	adantl	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to G : {Base}_{S} ⟶ {Base}_{T}$
8	7	ffnd	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom 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 MgmHom T) \land G \in (S MgmHom 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 MgmHom T) \land G \in (S MgmHom T)) \to \{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S}$
13		mgmhmrcl	$⊢ F \in (S MgmHom T) \to (S \in Mgm \land T \in Mgm)$
14	13	simpld	$⊢ F \in (S MgmHom T) \to S \in Mgm$
15	14	adantr	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to S \in Mgm$
16	15	ad2antrr	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land F (x) = G (x))) \land (y \in {Base}_{S} \land F (y) = G (y))) \to S \in Mgm$
17		simplrl	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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}$
18		simprl	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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}$
19		eqid	$⊢ +_{S} = +_{S}$
20	1 19	mgmcl	$⊢ (S \in Mgm \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
21	16 17 18 20	syl3anc	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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}$
22		simplrr	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)$
23		simprr	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)$
24	22 23	oveq12d	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)$
25		simplll	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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 MgmHom T)$
26		eqid	$⊢ +_{T} = +_{T}$
27	1 19 26	mgmhmlin	$⊢ (F \in (S MgmHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{T} F (y)$
28	25 17 18 27	syl3anc	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)$
29		simpllr	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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 MgmHom T)$
30	1 19 26	mgmhmlin	$⊢ (G \in (S MgmHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to G (x +_{S} y) = G (x) +_{T} G (y)$
31	29 17 18 30	syl3anc	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)$
32	24 28 31	3eqtr4d	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)$
33		fveq2	$⊢ z = x +_{S} y \to F (z) = F (x +_{S} y)$
34		fveq2	$⊢ z = x +_{S} y \to G (z) = G (x +_{S} y)$
35	33 34	eqeq12d	$⊢ z = x +_{S} y \to (F (z) = G (z) \leftrightarrow F (x +_{S} y) = G (x +_{S} y))$
36	35	elrab	$⊢ x +_{S} y \in \{z \in {Base}_{S} \| F (z) = G (z)\} \leftrightarrow (x +_{S} y \in {Base}_{S} \land F (x +_{S} y) = G (x +_{S} y))$
37	21 32 36	sylanbrc	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)\}$
38	37	expr	$⊢ (((F \in (S MgmHom T) \land G \in (S MgmHom 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)\})$
39	38	ralrimiva	$⊢ ((F \in (S MgmHom T) \land G \in (S MgmHom 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)\})$
40		fveq2	$⊢ z = y \to F (z) = F (y)$
41		fveq2	$⊢ z = y \to G (z) = G (y)$
42	40 41	eqeq12d	$⊢ z = y \to (F (z) = G (z) \leftrightarrow F (y) = G (y))$
43	42	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)\})$
44	39 43	sylibr	$⊢ ((F \in (S MgmHom T) \land G \in (S MgmHom 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)\}$
45	44	expr	$⊢ ((F \in (S MgmHom T) \land G \in (S MgmHom 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)\})$
46	45	ralrimiva	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom 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)\})$
47		fveq2	$⊢ z = x \to F (z) = F (x)$
48		fveq2	$⊢ z = x \to G (z) = G (x)$
49	47 48	eqeq12d	$⊢ z = x \to (F (z) = G (z) \leftrightarrow F (x) = G (x))$
50	49	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)\})$
51	46 50	sylibr	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom 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)\}$
52	1 19	issubmgm	$⊢ S \in Mgm \to (\{z \in {Base}_{S} \| F (z) = G (z)\} \in SubMgm (S) \leftrightarrow (\{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S} \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)\}))$
53	15 52	syl	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to (\{z \in {Base}_{S} \| F (z) = G (z)\} \in SubMgm (S) \leftrightarrow (\{z \in {Base}_{S} \| F (z) = G (z)\} \subseteq {Base}_{S} \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)\}))$
54	12 51 53	mpbir2and	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to \{z \in {Base}_{S} \| F (z) = G (z)\} \in SubMgm (S)$
55	10 54	eqeltrd	$⊢ (F \in (S MgmHom T) \land G \in (S MgmHom T)) \to dom (F \cap G) \in SubMgm (S)$

Metamath Proof Explorer

Theorem mgmhmeql

Proof