mndractf1

Description: If an element X of a monoid E is right-invertible, with inverse Y , then its left-translation G is injective. See also grplactf1o . Remark in chapter I. of BourbakiAlg1 p. 17 . (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$
	mndractf1.1	$⊢ φ \to Y \in B$
	mndractf1.2	$⊢ φ \to X \underset{˙}{+} Y = \underset{˙}{0}$
Assertion	mndractf1	$⊢ φ \to G : B \underset{1-1}{⟶} B$

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		mndractf1.1	$⊢ φ \to Y \in B$
8		mndractf1.2	$⊢ φ \to X \underset{˙}{+} Y = \underset{˙}{0}$
9	5	adantr	$⊢ (φ \land a \in B) \to E \in Mnd$
10		simpr	$⊢ (φ \land a \in B) \to a \in B$
11	6	adantr	$⊢ (φ \land a \in B) \to X \in B$
12	1 3 9 10 11	mndcld	$⊢ (φ \land a \in B) \to a \underset{˙}{+} X \in B$
13	12 4	fmptd	$⊢ φ \to G : B ⟶ B$
14		simpr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to G (i) = G (j)$
15		oveq1	$⊢ a = i \to a \underset{˙}{+} X = i \underset{˙}{+} X$
16		simpllr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \in B$
17		ovexd	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \underset{˙}{+} X \in V$
18	4 15 16 17	fvmptd3	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to G (i) = i \underset{˙}{+} X$
19		oveq1	$⊢ a = j \to a \underset{˙}{+} X = j \underset{˙}{+} X$
20		simplr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to j \in B$
21		ovexd	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to j \underset{˙}{+} X \in V$
22	4 19 20 21	fvmptd3	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to G (j) = j \underset{˙}{+} X$
23	14 18 22	3eqtr3d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \underset{˙}{+} X = j \underset{˙}{+} X$
24	23	oveq1d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to (i \underset{˙}{+} X) \underset{˙}{+} Y = (j \underset{˙}{+} X) \underset{˙}{+} Y$
25	5	ad3antrrr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to E \in Mnd$
26	6	ad3antrrr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to X \in B$
27	7	ad3antrrr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to Y \in B$
28	1 3 25 16 26 27	mndassd	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to (i \underset{˙}{+} X) \underset{˙}{+} Y = i \underset{˙}{+} (X \underset{˙}{+} Y)$
29	1 3 25 20 26 27	mndassd	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to (j \underset{˙}{+} X) \underset{˙}{+} Y = j \underset{˙}{+} (X \underset{˙}{+} Y)$
30	24 28 29	3eqtr3d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \underset{˙}{+} (X \underset{˙}{+} Y) = j \underset{˙}{+} (X \underset{˙}{+} Y)$
31	8	ad3antrrr	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to X \underset{˙}{+} Y = \underset{˙}{0}$
32	31	oveq2d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \underset{˙}{+} (X \underset{˙}{+} Y) = i \underset{˙}{+} \underset{˙}{0}$
33	31	oveq2d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to j \underset{˙}{+} (X \underset{˙}{+} Y) = j \underset{˙}{+} \underset{˙}{0}$
34	30 32 33	3eqtr3d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \underset{˙}{+} \underset{˙}{0} = j \underset{˙}{+} \underset{˙}{0}$
35	1 3 2	mndrid	$⊢ (E \in Mnd \land i \in B) \to i \underset{˙}{+} \underset{˙}{0} = i$
36	25 16 35	syl2anc	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i \underset{˙}{+} \underset{˙}{0} = i$
37	1 3 2	mndrid	$⊢ (E \in Mnd \land j \in B) \to j \underset{˙}{+} \underset{˙}{0} = j$
38	25 20 37	syl2anc	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to j \underset{˙}{+} \underset{˙}{0} = j$
39	34 36 38	3eqtr3d	$⊢ (((φ \land i \in B) \land j \in B) \land G (i) = G (j)) \to i = j$
40	39	ex	$⊢ ((φ \land i \in B) \land j \in B) \to (G (i) = G (j) \to i = j)$
41	40	anasss	$⊢ (φ \land (i \in B \land j \in B)) \to (G (i) = G (j) \to i = j)$
42	41	ralrimivva	$⊢ φ \to \forall i \in B \forall j \in B (G (i) = G (j) \to i = j)$
43		dff13	$⊢ G : B \underset{1-1}{⟶} B \leftrightarrow (G : B ⟶ B \land \forall i \in B \forall j \in B (G (i) = G (j) \to i = j))$
44	13 42 43	sylanbrc	$⊢ φ \to G : B \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem mndractf1

Proof