mndlactfo

Description: An element X of a monoid E is left-invertible iff its left-translation F is surjective. See also grplactf1o . (Contributed by Thierry Arnoux, 3-Aug-2025)

	Ref	Expression
Hypotheses	mndlactfo.b	$⊢ B = {Base}_{E}$
	mndlactfo.z	$⊢ \underset{˙}{0} = 0_{E}$
	mndlactfo.p	$⊢ \underset{˙}{+} = +_{E}$
	mndlactfo.f	$⊢ F = (a \in B ⟼ X \underset{˙}{+} a)$
	mndlactfo.e	$⊢ φ \to E \in Mnd$
	mndlactfo.x	$⊢ φ \to X \in B$
Assertion	mndlactfo	$⊢ φ \to (F : B \underset{onto}{⟶} B \leftrightarrow \exists y \in B X \underset{˙}{+} y = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		mndlactfo.b	$⊢ B = {Base}_{E}$
2		mndlactfo.z	$⊢ \underset{˙}{0} = 0_{E}$
3		mndlactfo.p	$⊢ \underset{˙}{+} = +_{E}$
4		mndlactfo.f	$⊢ F = (a \in B ⟼ X \underset{˙}{+} a)$
5		mndlactfo.e	$⊢ φ \to E \in Mnd$
6		mndlactfo.x	$⊢ φ \to X \in B$
7		simpr	$⊢ (φ \land F : B \underset{onto}{⟶} B) \to F : B \underset{onto}{⟶} B$
8	1 2	mndidcl	$⊢ E \in Mnd \to \underset{˙}{0} \in B$
9	5 8	syl	$⊢ φ \to \underset{˙}{0} \in B$
10	9	adantr	$⊢ (φ \land F : B \underset{onto}{⟶} B) \to \underset{˙}{0} \in B$
11		foelcdmi	$⊢ (F : B \underset{onto}{⟶} B \land \underset{˙}{0} \in B) \to \exists y \in B F (y) = \underset{˙}{0}$
12	7 10 11	syl2anc	$⊢ (φ \land F : B \underset{onto}{⟶} B) \to \exists y \in B F (y) = \underset{˙}{0}$
13		oveq2	$⊢ a = y \to X \underset{˙}{+} a = X \underset{˙}{+} y$
14		simpr	$⊢ ((φ \land F : B \underset{onto}{⟶} B) \land y \in B) \to y \in B$
15		ovexd	$⊢ ((φ \land F : B \underset{onto}{⟶} B) \land y \in B) \to X \underset{˙}{+} y \in V$
16	4 13 14 15	fvmptd3	$⊢ ((φ \land F : B \underset{onto}{⟶} B) \land y \in B) \to F (y) = X \underset{˙}{+} y$
17	16	eqeq1d	$⊢ ((φ \land F : B \underset{onto}{⟶} B) \land y \in B) \to (F (y) = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} y = \underset{˙}{0})$
18	17	biimpd	$⊢ ((φ \land F : B \underset{onto}{⟶} B) \land y \in B) \to (F (y) = \underset{˙}{0} \to X \underset{˙}{+} y = \underset{˙}{0})$
19	18	reximdva	$⊢ (φ \land F : B \underset{onto}{⟶} B) \to (\exists y \in B F (y) = \underset{˙}{0} \to \exists y \in B X \underset{˙}{+} y = \underset{˙}{0})$
20	12 19	mpd	$⊢ (φ \land F : B \underset{onto}{⟶} B) \to \exists y \in B X \underset{˙}{+} y = \underset{˙}{0}$
21	5	adantr	$⊢ (φ \land a \in B) \to E \in Mnd$
22	6	adantr	$⊢ (φ \land a \in B) \to X \in B$
23		simpr	$⊢ (φ \land a \in B) \to a \in B$
24	1 3 21 22 23	mndcld	$⊢ (φ \land a \in B) \to X \underset{˙}{+} a \in B$
25	24 4	fmptd	$⊢ φ \to F : B ⟶ B$
26	25	ad2antrr	$⊢ ((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \to F : B ⟶ B$
27		fveq2	$⊢ x = y \underset{˙}{+} z \to F (x) = F (y \underset{˙}{+} z)$
28	27	eqeq2d	$⊢ x = y \underset{˙}{+} z \to (z = F (x) \leftrightarrow z = F (y \underset{˙}{+} z))$
29	5	ad3antrrr	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to E \in Mnd$
30		simpllr	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to y \in B$
31		simpr	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to z \in B$
32	1 3 29 30 31	mndcld	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to y \underset{˙}{+} z \in B$
33	6	ad3antrrr	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to X \in B$
34	1 3 29 33 30 31	mndassd	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to (X \underset{˙}{+} y) \underset{˙}{+} z = X \underset{˙}{+} (y \underset{˙}{+} z)$
35		simplr	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to X \underset{˙}{+} y = \underset{˙}{0}$
36	35	oveq1d	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to (X \underset{˙}{+} y) \underset{˙}{+} z = \underset{˙}{0} \underset{˙}{+} z$
37	1 3 2	mndlid	$⊢ (E \in Mnd \land z \in B) \to \underset{˙}{0} \underset{˙}{+} z = z$
38	29 31 37	syl2anc	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to \underset{˙}{0} \underset{˙}{+} z = z$
39	36 38	eqtr2d	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to z = (X \underset{˙}{+} y) \underset{˙}{+} z$
40		oveq2	$⊢ a = y \underset{˙}{+} z \to X \underset{˙}{+} a = X \underset{˙}{+} (y \underset{˙}{+} z)$
41		ovexd	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to X \underset{˙}{+} (y \underset{˙}{+} z) \in V$
42	4 40 32 41	fvmptd3	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to F (y \underset{˙}{+} z) = X \underset{˙}{+} (y \underset{˙}{+} z)$
43	34 39 42	3eqtr4d	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to z = F (y \underset{˙}{+} z)$
44	28 32 43	rspcedvdw	$⊢ (((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \land z \in B) \to \exists x \in B z = F (x)$
45	44	ralrimiva	$⊢ ((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \to \forall z \in B \exists x \in B z = F (x)$
46		dffo3	$⊢ F : B \underset{onto}{⟶} B \leftrightarrow (F : B ⟶ B \land \forall z \in B \exists x \in B z = F (x))$
47	26 45 46	sylanbrc	$⊢ ((φ \land y \in B) \land X \underset{˙}{+} y = \underset{˙}{0}) \to F : B \underset{onto}{⟶} B$
48	47	r19.29an	$⊢ (φ \land \exists y \in B X \underset{˙}{+} y = \underset{˙}{0}) \to F : B \underset{onto}{⟶} B$
49	20 48	impbida	$⊢ φ \to (F : B \underset{onto}{⟶} B \leftrightarrow \exists y \in B X \underset{˙}{+} y = \underset{˙}{0})$

Metamath Proof Explorer

Theorem mndlactfo

Proof