ghmcmn

Description: The image of a commutative monoid G under a group homomorphism F is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ghmabl.x	$⊢ X = {Base}_{G}$
2		ghmabl.y	$⊢ Y = {Base}_{H}$
3		ghmabl.p	$⊢ \underset{˙}{+} = +_{G}$
4		ghmabl.q	$⊢ \underset{˙}{⨣} = +_{H}$
5		ghmabl.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
6		ghmabl.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
7		ghmcmn.3	$⊢ φ \to G \in CMnd$
8		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
9	7 8	syl	$⊢ φ \to G \in Mnd$
10	5 1 2 3 4 6 9	mhmmnd	$⊢ φ \to H \in Mnd$
11		simp-6l	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to φ$
12	11 7	syl	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to G \in CMnd$
13		simp-4r	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to a \in X$
14		simplr	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to b \in X$
15	1 3	cmncom	$⊢ (G \in CMnd \land a \in X \land b \in X) \to a \underset{˙}{+} b = b \underset{˙}{+} a$
16	12 13 14 15	syl3anc	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to a \underset{˙}{+} b = b \underset{˙}{+} a$
17	16	fveq2d	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (a \underset{˙}{+} b) = F (b \underset{˙}{+} a)$
18	11 5	syl3an1	$⊢ (((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
19	18 13 14	mhmlem	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (a \underset{˙}{+} b) = F (a) \underset{˙}{⨣} F (b)$
20	18 14 13	mhmlem	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (b \underset{˙}{+} a) = F (b) \underset{˙}{⨣} F (a)$
21	17 19 20	3eqtr3d	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (a) \underset{˙}{⨣} F (b) = F (b) \underset{˙}{⨣} F (a)$
22		simpllr	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (a) = i$
23		simpr	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (b) = j$
24	22 23	oveq12d	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (a) \underset{˙}{⨣} F (b) = i \underset{˙}{⨣} j$
25	23 22	oveq12d	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to F (b) \underset{˙}{⨣} F (a) = j \underset{˙}{⨣} i$
26	21 24 25	3eqtr3d	$⊢ ((((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \land b \in X) \land F (b) = j) \to i \underset{˙}{⨣} j = j \underset{˙}{⨣} i$
27		foelcdmi	$⊢ (F : X \underset{onto}{⟶} Y \land j \in Y) \to \exists b \in X F (b) = j$
28	6 27	sylan	$⊢ (φ \land j \in Y) \to \exists b \in X F (b) = j$
29	28	ad5ant13	$⊢ ((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \to \exists b \in X F (b) = j$
30	26 29	r19.29a	$⊢ ((((φ \land i \in Y) \land j \in Y) \land a \in X) \land F (a) = i) \to i \underset{˙}{⨣} j = j \underset{˙}{⨣} i$
31		foelcdmi	$⊢ (F : X \underset{onto}{⟶} Y \land i \in Y) \to \exists a \in X F (a) = i$
32	6 31	sylan	$⊢ (φ \land i \in Y) \to \exists a \in X F (a) = i$
33	32	adantr	$⊢ ((φ \land i \in Y) \land j \in Y) \to \exists a \in X F (a) = i$
34	30 33	r19.29a	$⊢ ((φ \land i \in Y) \land j \in Y) \to i \underset{˙}{⨣} j = j \underset{˙}{⨣} i$
35	34	anasss	$⊢ (φ \land (i \in Y \land j \in Y)) \to i \underset{˙}{⨣} j = j \underset{˙}{⨣} i$
36	35	ralrimivva	$⊢ φ \to \forall i \in Y \forall j \in Y i \underset{˙}{⨣} j = j \underset{˙}{⨣} i$
37	2 4	iscmn	$⊢ H \in CMnd \leftrightarrow (H \in Mnd \land \forall i \in Y \forall j \in Y i \underset{˙}{⨣} j = j \underset{˙}{⨣} i)$
38	10 36 37	sylanbrc	$⊢ φ \to H \in CMnd$

Metamath Proof Explorer

Theorem ghmcmn

Proof