mndlactf1

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

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

Metamath Proof Explorer

Theorem mndlactf1

Proof