mndractfo

Description: An element X of a monoid E is right-invertible iff its right-translation G is surjective. (Contributed by Thierry Arnoux, 3-Aug-2025)

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

Proof

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

Metamath Proof Explorer

Theorem mndractfo

Proof