mhmmnd

Description: The image of a monoid G under a monoid homomorphism F is a monoid. (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$
Assertion	mhmmnd	$⊢ φ \to H \in Mnd$

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		simpllr	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F (i) = a$
9		simpr	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F (j) = b$
10	8 9	oveq12d	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F (i) \underset{˙}{⨣} F (j) = a \underset{˙}{⨣} b$
11		simp-5l	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to φ$
12	11 1	syl3an1	$⊢ ((((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
13		simp-4r	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to i \in X$
14		simplr	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to j \in X$
15	12 13 14	mhmlem	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F (i \underset{˙}{+} j) = F (i) \underset{˙}{⨣} F (j)$
16		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
17	6 16	syl	$⊢ φ \to F : X ⟶ Y$
18	17	ad5antr	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F : X ⟶ Y$
19	7	ad5antr	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to G \in Mnd$
20	2 4	mndcl	$⊢ (G \in Mnd \land i \in X \land j \in X) \to i \underset{˙}{+} j \in X$
21	19 13 14 20	syl3anc	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to i \underset{˙}{+} j \in X$
22	18 21	ffvelcdmd	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F (i \underset{˙}{+} j) \in Y$
23	15 22	eqeltrrd	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to F (i) \underset{˙}{⨣} F (j) \in Y$
24	10 23	eqeltrrd	$⊢ (((((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to a \underset{˙}{⨣} b \in Y$
25		simpr	$⊢ (a \in Y \land b \in Y) \to b \in Y$
26		foelcdmi	$⊢ (F : X \underset{onto}{⟶} Y \land b \in Y) \to \exists j \in X F (j) = b$
27	6 25 26	syl2an	$⊢ (φ \land (a \in Y \land b \in Y)) \to \exists j \in X F (j) = b$
28	27	ad2antrr	$⊢ (((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \to \exists j \in X F (j) = b$
29	24 28	r19.29a	$⊢ (((φ \land (a \in Y \land b \in Y)) \land i \in X) \land F (i) = a) \to a \underset{˙}{⨣} b \in Y$
30		simpl	$⊢ (a \in Y \land b \in Y) \to a \in Y$
31		foelcdmi	$⊢ (F : X \underset{onto}{⟶} Y \land a \in Y) \to \exists i \in X F (i) = a$
32	6 30 31	syl2an	$⊢ (φ \land (a \in Y \land b \in Y)) \to \exists i \in X F (i) = a$
33	29 32	r19.29a	$⊢ (φ \land (a \in Y \land b \in Y)) \to a \underset{˙}{⨣} b \in Y$
34		simpll	$⊢ ((φ \land (a \in Y \land b \in Y)) \land c \in Y) \to φ$
35		simplrl	$⊢ ((φ \land (a \in Y \land b \in Y)) \land c \in Y) \to a \in Y$
36		simplrr	$⊢ ((φ \land (a \in Y \land b \in Y)) \land c \in Y) \to b \in Y$
37		simpr	$⊢ ((φ \land (a \in Y \land b \in Y)) \land c \in Y) \to c \in Y$
38	7	ad2antrr	$⊢ ((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \to G \in Mnd$
39	38	ad5antr	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to G \in Mnd$
40		simp-6r	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to i \in X$
41		simp-4r	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to j \in X$
42		simplr	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to k \in X$
43	2 4	mndass	$⊢ (G \in Mnd \land (i \in X \land j \in X \land k \in X)) \to (i \underset{˙}{+} j) \underset{˙}{+} k = i \underset{˙}{+} (j \underset{˙}{+} k)$
44	39 40 41 42 43	syl13anc	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to (i \underset{˙}{+} j) \underset{˙}{+} k = i \underset{˙}{+} (j \underset{˙}{+} k)$
45	44	fveq2d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F ((i \underset{˙}{+} j) \underset{˙}{+} k) = F (i \underset{˙}{+} (j \underset{˙}{+} k))$
46		simp-7l	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to φ$
47	46 1	syl3an1	$⊢ ((((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
48	39 40 41 20	syl3anc	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to i \underset{˙}{+} j \in X$
49	47 48 42	mhmlem	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F ((i \underset{˙}{+} j) \underset{˙}{+} k) = F (i \underset{˙}{+} j) \underset{˙}{⨣} F (k)$
50	2 4	mndcl	$⊢ (G \in Mnd \land j \in X \land k \in X) \to j \underset{˙}{+} k \in X$
51	39 41 42 50	syl3anc	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to j \underset{˙}{+} k \in X$
52	47 40 51	mhmlem	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i \underset{˙}{+} (j \underset{˙}{+} k)) = F (i) \underset{˙}{⨣} F (j \underset{˙}{+} k)$
53	45 49 52	3eqtr3d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i \underset{˙}{+} j) \underset{˙}{⨣} F (k) = F (i) \underset{˙}{⨣} F (j \underset{˙}{+} k)$
54		simp1	$⊢ (φ \land i \in X \land j \in X) \to φ$
55	54 1	syl3an1	$⊢ ((φ \land i \in X \land j \in X) \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
56		simp2	$⊢ (φ \land i \in X \land j \in X) \to i \in X$
57		simp3	$⊢ (φ \land i \in X \land j \in X) \to j \in X$
58	55 56 57	mhmlem	$⊢ (φ \land i \in X \land j \in X) \to F (i \underset{˙}{+} j) = F (i) \underset{˙}{⨣} F (j)$
59	46 40 41 58	syl3anc	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i \underset{˙}{+} j) = F (i) \underset{˙}{⨣} F (j)$
60	59	oveq1d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i \underset{˙}{+} j) \underset{˙}{⨣} F (k) = (F (i) \underset{˙}{⨣} F (j)) \underset{˙}{⨣} F (k)$
61	47 41 42	mhmlem	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (j \underset{˙}{+} k) = F (j) \underset{˙}{⨣} F (k)$
62	61	oveq2d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i) \underset{˙}{⨣} F (j \underset{˙}{+} k) = F (i) \underset{˙}{⨣} (F (j) \underset{˙}{⨣} F (k))$
63	53 60 62	3eqtr3d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to (F (i) \underset{˙}{⨣} F (j)) \underset{˙}{⨣} F (k) = F (i) \underset{˙}{⨣} (F (j) \underset{˙}{⨣} F (k))$
64		simp-5r	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i) = a$
65		simpllr	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (j) = b$
66	64 65	oveq12d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i) \underset{˙}{⨣} F (j) = a \underset{˙}{⨣} b$
67		simpr	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (k) = c$
68	66 67	oveq12d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to (F (i) \underset{˙}{⨣} F (j)) \underset{˙}{⨣} F (k) = (a \underset{˙}{⨣} b) \underset{˙}{⨣} c$
69	65 67	oveq12d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (j) \underset{˙}{⨣} F (k) = b \underset{˙}{⨣} c$
70	64 69	oveq12d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to F (i) \underset{˙}{⨣} (F (j) \underset{˙}{⨣} F (k)) = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
71	63 68 70	3eqtr3d	$⊢ (((((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \land k \in X) \land F (k) = c) \to (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
72		foelcdmi	$⊢ (F : X \underset{onto}{⟶} Y \land c \in Y) \to \exists k \in X F (k) = c$
73	6 72	sylan	$⊢ (φ \land c \in Y) \to \exists k \in X F (k) = c$
74	73	3ad2antr3	$⊢ (φ \land (a \in Y \land b \in Y \land c \in Y)) \to \exists k \in X F (k) = c$
75	74	ad4antr	$⊢ (((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to \exists k \in X F (k) = c$
76	71 75	r19.29a	$⊢ (((((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \land j \in X) \land F (j) = b) \to (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
77	27	3adantr3	$⊢ (φ \land (a \in Y \land b \in Y \land c \in Y)) \to \exists j \in X F (j) = b$
78	77	ad2antrr	$⊢ (((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \to \exists j \in X F (j) = b$
79	76 78	r19.29a	$⊢ (((φ \land (a \in Y \land b \in Y \land c \in Y)) \land i \in X) \land F (i) = a) \to (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
80	32	3adantr3	$⊢ (φ \land (a \in Y \land b \in Y \land c \in Y)) \to \exists i \in X F (i) = a$
81	79 80	r19.29a	$⊢ (φ \land (a \in Y \land b \in Y \land c \in Y)) \to (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
82	34 35 36 37 81	syl13anc	$⊢ ((φ \land (a \in Y \land b \in Y)) \land c \in Y) \to (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
83	82	ralrimiva	$⊢ (φ \land (a \in Y \land b \in Y)) \to \forall c \in Y (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)$
84	33 83	jca	$⊢ (φ \land (a \in Y \land b \in Y)) \to (a \underset{˙}{⨣} b \in Y \land \forall c \in Y (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c))$
85	84	ralrimivva	$⊢ φ \to \forall a \in Y \forall b \in Y (a \underset{˙}{⨣} b \in Y \land \forall c \in Y (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c))$
86		eqid	$⊢ 0_{G} = 0_{G}$
87	2 86	mndidcl	$⊢ G \in Mnd \to 0_{G} \in X$
88	7 87	syl	$⊢ φ \to 0_{G} \in X$
89	17 88	ffvelcdmd	$⊢ φ \to F (0_{G}) \in Y$
90		simplll	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to φ$
91	90 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)$
92	7	ad3antrrr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to G \in Mnd$
93	92 87	syl	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to 0_{G} \in X$
94		simplr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to i \in X$
95	91 93 94	mhmlem	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (0_{G} \underset{˙}{+} i) = F (0_{G}) \underset{˙}{⨣} F (i)$
96	2 4 86	mndlid	$⊢ (G \in Mnd \land i \in X) \to 0_{G} \underset{˙}{+} i = i$
97	92 94 96	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to 0_{G} \underset{˙}{+} i = i$
98	97	fveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (0_{G} \underset{˙}{+} i) = F (i)$
99	95 98	eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (0_{G}) \underset{˙}{⨣} F (i) = F (i)$
100		simpr	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) = a$
101	100	oveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (0_{G}) \underset{˙}{⨣} F (i) = F (0_{G}) \underset{˙}{⨣} a$
102	99 101 100	3eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (0_{G}) \underset{˙}{⨣} a = a$
103	91 94 93	mhmlem	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i \underset{˙}{+} 0_{G}) = F (i) \underset{˙}{⨣} F (0_{G})$
104	2 4 86	mndrid	$⊢ (G \in Mnd \land i \in X) \to i \underset{˙}{+} 0_{G} = i$
105	92 94 104	syl2anc	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to i \underset{˙}{+} 0_{G} = i$
106	105	fveq2d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i \underset{˙}{+} 0_{G}) = F (i)$
107	103 106	eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) \underset{˙}{⨣} F (0_{G}) = F (i)$
108	100	oveq1d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to F (i) \underset{˙}{⨣} F (0_{G}) = a \underset{˙}{⨣} F (0_{G})$
109	107 108 100	3eqtr3d	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to a \underset{˙}{⨣} F (0_{G}) = a$
110	102 109	jca	$⊢ (((φ \land a \in Y) \land i \in X) \land F (i) = a) \to (F (0_{G}) \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} F (0_{G}) = a)$
111	6 31	sylan	$⊢ (φ \land a \in Y) \to \exists i \in X F (i) = a$
112	110 111	r19.29a	$⊢ (φ \land a \in Y) \to (F (0_{G}) \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} F (0_{G}) = a)$
113	112	ralrimiva	$⊢ φ \to \forall a \in Y (F (0_{G}) \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} F (0_{G}) = a)$
114		oveq1	$⊢ d = F (0_{G}) \to d \underset{˙}{⨣} a = F (0_{G}) \underset{˙}{⨣} a$
115	114	eqeq1d	$⊢ d = F (0_{G}) \to (d \underset{˙}{⨣} a = a \leftrightarrow F (0_{G}) \underset{˙}{⨣} a = a)$
116	115	ovanraleqv	$⊢ d = F (0_{G}) \to (\forall a \in Y (d \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} d = a) \leftrightarrow \forall a \in Y (F (0_{G}) \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} F (0_{G}) = a))$
117	116	rspcev	$⊢ (F (0_{G}) \in Y \land \forall a \in Y (F (0_{G}) \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} F (0_{G}) = a)) \to \exists d \in Y \forall a \in Y (d \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} d = a)$
118	89 113 117	syl2anc	$⊢ φ \to \exists d \in Y \forall a \in Y (d \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} d = a)$
119	3 5	ismnd	$⊢ H \in Mnd \leftrightarrow (\forall a \in Y \forall b \in Y (a \underset{˙}{⨣} b \in Y \land \forall c \in Y (a \underset{˙}{⨣} b) \underset{˙}{⨣} c = a \underset{˙}{⨣} (b \underset{˙}{⨣} c)) \land \exists d \in Y \forall a \in Y (d \underset{˙}{⨣} a = a \land a \underset{˙}{⨣} d = a))$
120	85 118 119	sylanbrc	$⊢ φ \to H \in Mnd$

Metamath Proof Explorer

Theorem mhmmnd

Proof