mhmid

Description: A surjective monoid morphism preserves identity element. (Contributed by Thierry Arnoux, 25-Jan-2020)

	Ref	Expression
Hypotheses	ghmgrp.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
	ghmgrp.x	$⊢ X = {Base}_{G}$
	ghmgrp.y	$⊢ Y = {Base}_{H}$
	ghmgrp.p	$⊢ \underset{˙}{+} = +_{G}$
	ghmgrp.q	$⊢ \underset{˙}{⨣} = +_{H}$
	ghmgrp.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
	mhmmnd.3	$⊢ φ \to G \in Mnd$
	mhmid.0	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	mhmid	$⊢ φ \to F (\underset{˙}{0}) = 0_{H}$

Proof

Step	Hyp	Ref	Expression
1		ghmgrp.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
2		ghmgrp.x	$⊢ X = {Base}_{G}$
3		ghmgrp.y	$⊢ Y = {Base}_{H}$
4		ghmgrp.p	$⊢ \underset{˙}{+} = +_{G}$
5		ghmgrp.q	$⊢ \underset{˙}{⨣} = +_{H}$
6		ghmgrp.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
7		mhmmnd.3	$⊢ φ \to G \in Mnd$
8		mhmid.0	$⊢ \underset{˙}{0} = 0_{G}$
9		eqid	$⊢ 0_{H} = 0_{H}$
10		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
11	6 10	syl	$⊢ φ \to F : X ⟶ Y$
12	2 8	mndidcl	$⊢ G \in Mnd \to \underset{˙}{0} \in X$
13	7 12	syl	$⊢ φ \to \underset{˙}{0} \in X$
14	11 13	ffvelrnd	$⊢ φ \to F (\underset{˙}{0}) \in Y$
15		simplll	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to φ$
16	15 1	syl3an1	$⊢ ((((φ \land a \in Y) \land i \in X) \land F (i) = a) \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
17	7	ad3antrrr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to G \in Mnd$
18	17 12	syl	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to \underset{˙}{0} \in X$
19		simplr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to i \in X$
20	16 18 19	mhmlem	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (\underset{˙}{0} \underset{˙}{+} i) = F (\underset{˙}{0}) \underset{˙}{⨣} F (i)$
21	2 4 8	mndlid	$⊢ (G \in Mnd \land i \in X) \to \underset{˙}{0} \underset{˙}{+} i = i$
22	17 19 21	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to \underset{˙}{0} \underset{˙}{+} i = i$
23	22	fveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (\underset{˙}{0} \underset{˙}{+} i) = F (i)$
24	20 23	eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (\underset{˙}{0}) \underset{˙}{⨣} F (i) = F (i)$
25		simpr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) = a$
26	25	oveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (\underset{˙}{0}) \underset{˙}{⨣} F (i) = F (\underset{˙}{0}) \underset{˙}{⨣} a$
27	24 26 25	3eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (\underset{˙}{0}) \underset{˙}{⨣} a = a$
28		foelrni	$⊢ (F : X \underset{onto}{⟶} Y \land a \in Y) \to \exists i \in X F (i) = a$
29	6 28	sylan	$⊢ (φ \land a \in Y) \to \exists i \in X F (i) = a$
30	27 29	r19.29a	$⊢ (φ \land a \in Y) \to F (\underset{˙}{0}) \underset{˙}{⨣} a = a$
31	16 19 18	mhmlem	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i \underset{˙}{+} \underset{˙}{0}) = F (i) \underset{˙}{⨣} F (\underset{˙}{0})$
32	2 4 8	mndrid	$⊢ (G \in Mnd \land i \in X) \to i \underset{˙}{+} \underset{˙}{0} = i$
33	17 19 32	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to i \underset{˙}{+} \underset{˙}{0} = i$
34	33	fveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i \underset{˙}{+} \underset{˙}{0}) = F (i)$
35	31 34	eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) \underset{˙}{⨣} F (\underset{˙}{0}) = F (i)$
36	25	oveq1d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) \underset{˙}{⨣} F (\underset{˙}{0}) = a \underset{˙}{⨣} F (\underset{˙}{0})$
37	35 36 25	3eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to a \underset{˙}{⨣} F (\underset{˙}{0}) = a$
38	37 29	r19.29a	$⊢ (φ \land a \in Y) \to a \underset{˙}{⨣} F (\underset{˙}{0}) = a$
39	3 9 5 14 30 38	ismgmid2	$⊢ φ \to F (\underset{˙}{0}) = 0_{H}$

Metamath Proof Explorer

Theorem mhmid

Proof