mndlactf1o

Description: An element X of a monoid E is invertible iff its left-translation F is bijective. See also grplactf1o . Remark in chapter I. of BourbakiAlg1 p. 17. (Contributed by Thierry Arnoux, 3-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		mndlactf1o.b	$⊢ B = {Base}_{E}$
2		mndlactf1o.z	$⊢ \underset{˙}{0} = 0_{E}$
3		mndlactf1o.p	$⊢ \underset{˙}{+} = +_{E}$
4		mndlactf1o.f	$⊢ F = (a \in B ⟼ X \underset{˙}{+} a)$
5		mndlactf1o.e	$⊢ φ \to E \in Mnd$
6		mndlactf1o.x	$⊢ φ \to X \in B$
7		oveq2	$⊢ y = u \to X \underset{˙}{+} y = X \underset{˙}{+} u$
8	7	eqeq1d	$⊢ y = u \to (X \underset{˙}{+} y = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} u = \underset{˙}{0})$
9		oveq1	$⊢ y = u \to y \underset{˙}{+} X = u \underset{˙}{+} X$
10	9	eqeq1d	$⊢ y = u \to (y \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow u \underset{˙}{+} X = \underset{˙}{0})$
11	8 10	anbi12d	$⊢ y = u \to ((X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0}) \leftrightarrow (X \underset{˙}{+} u = \underset{˙}{0} \land u \underset{˙}{+} X = \underset{˙}{0}))$
12		simplr	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to u \in B$
13		simpr	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to X \underset{˙}{+} u = \underset{˙}{0}$
14	5	ad5antr	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to E \in Mnd$
15	6	ad5antr	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to X \in B$
16		simp-4r	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v \in B$
17		simpllr	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v \underset{˙}{+} X = \underset{˙}{0}$
18	1 2 3 14 15 16 12 17 13	mndlrinv	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v = u$
19	18	oveq1d	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to v \underset{˙}{+} X = u \underset{˙}{+} X$
20	19 17	eqtr3d	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to u \underset{˙}{+} X = \underset{˙}{0}$
21	13 20	jca	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to (X \underset{˙}{+} u = \underset{˙}{0} \land u \underset{˙}{+} X = \underset{˙}{0})$
22	11 12 21	rspcedvdw	$⊢ (((((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \land u \in B) \land X \underset{˙}{+} u = \underset{˙}{0}) \to \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})$
23		f1ofo	$⊢ F : B \underset{1-1 onto}{⟶} B \to F : B \underset{onto}{⟶} B$
24	23	adantl	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F : B \underset{onto}{⟶} B$
25	1 2 3 4 5 6	mndlactfo	$⊢ φ \to (F : B \underset{onto}{⟶} B \leftrightarrow \exists u \in B X \underset{˙}{+} u = \underset{˙}{0})$
26	25	biimpa	$⊢ (φ \land F : B \underset{onto}{⟶} B) \to \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}$
27	24 26	syldan	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}$
28	27	ad2antrr	$⊢ (((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}$
29	22 28	r19.29a	$⊢ (((φ \land F : B \underset{1-1 onto}{⟶} B) \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})$
30		oveq1	$⊢ v = F^{-1} (\underset{˙}{0}) \to v \underset{˙}{+} X = F^{-1} (\underset{˙}{0}) \underset{˙}{+} X$
31	30	eqeq1d	$⊢ v = F^{-1} (\underset{˙}{0}) \to (v \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow F^{-1} (\underset{˙}{0}) \underset{˙}{+} X = \underset{˙}{0})$
32		f1ocnv	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} B$
33		f1of	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} B \to F^{-1} : B ⟶ B$
34	32 33	syl	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} : B ⟶ B$
35	34	adantl	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F^{-1} : B ⟶ B$
36	1 2	mndidcl	$⊢ E \in Mnd \to \underset{˙}{0} \in B$
37	5 36	syl	$⊢ φ \to \underset{˙}{0} \in B$
38	37	adantr	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to \underset{˙}{0} \in B$
39	35 38	ffvelcdmd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F^{-1} (\underset{˙}{0}) \in B$
40		f1of1	$⊢ F : B \underset{1-1 onto}{⟶} B \to F : B \underset{1-1}{⟶} B$
41	40	adantl	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F : B \underset{1-1}{⟶} B$
42	5	adantr	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to E \in Mnd$
43	6	adantr	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \in B$
44	1 3 42 39 43	mndcld	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F^{-1} (\underset{˙}{0}) \underset{˙}{+} X \in B$
45	44 38	jca	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X \in B \land \underset{˙}{0} \in B)$
46	1 3 2	mndrid	$⊢ (E \in Mnd \land X \in B) \to X \underset{˙}{+} \underset{˙}{0} = X$
47	42 43 46	syl2anc	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \underset{˙}{+} \underset{˙}{0} = X$
48		oveq2	$⊢ a = \underset{˙}{0} \to X \underset{˙}{+} a = X \underset{˙}{+} \underset{˙}{0}$
49		ovexd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \underset{˙}{+} \underset{˙}{0} \in V$
50	4 48 38 49	fvmptd3	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F (\underset{˙}{0}) = X \underset{˙}{+} \underset{˙}{0}$
51		oveq2	$⊢ a = F^{-1} (\underset{˙}{0}) \underset{˙}{+} X \to X \underset{˙}{+} a = X \underset{˙}{+} (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X)$
52		ovexd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \underset{˙}{+} (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) \in V$
53	4 51 44 52	fvmptd3	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) = X \underset{˙}{+} (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X)$
54		oveq2	$⊢ a = F^{-1} (\underset{˙}{0}) \to X \underset{˙}{+} a = X \underset{˙}{+} F^{-1} (\underset{˙}{0})$
55		ovexd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \underset{˙}{+} F^{-1} (\underset{˙}{0}) \in V$
56	4 54 39 55	fvmptd3	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F (F^{-1} (\underset{˙}{0})) = X \underset{˙}{+} F^{-1} (\underset{˙}{0})$
57		simpr	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F : B \underset{1-1 onto}{⟶} B$
58		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} B \land \underset{˙}{0} \in B) \to F (F^{-1} (\underset{˙}{0})) = \underset{˙}{0}$
59	57 38 58	syl2anc	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F (F^{-1} (\underset{˙}{0})) = \underset{˙}{0}$
60	56 59	eqtr3d	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \underset{˙}{+} F^{-1} (\underset{˙}{0}) = \underset{˙}{0}$
61	60	oveq1d	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to (X \underset{˙}{+} F^{-1} (\underset{˙}{0})) \underset{˙}{+} X = \underset{˙}{0} \underset{˙}{+} X$
62	1 3 42 43 39 43	mndassd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to (X \underset{˙}{+} F^{-1} (\underset{˙}{0})) \underset{˙}{+} X = X \underset{˙}{+} (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X)$
63	1 3 2	mndlid	$⊢ (E \in Mnd \land X \in B) \to \underset{˙}{0} \underset{˙}{+} X = X$
64	42 43 63	syl2anc	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to \underset{˙}{0} \underset{˙}{+} X = X$
65	61 62 64	3eqtr3d	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to X \underset{˙}{+} (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) = X$
66	53 65	eqtrd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) = X$
67	47 50 66	3eqtr4rd	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) = F (\underset{˙}{0})$
68		f1fveq	$⊢ (F : B \underset{1-1}{⟶} B \land (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X \in B \land \underset{˙}{0} \in B)) \to (F (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) = F (\underset{˙}{0}) \leftrightarrow F^{-1} (\underset{˙}{0}) \underset{˙}{+} X = \underset{˙}{0})$
69	68	biimpa	$⊢ ((F : B \underset{1-1}{⟶} B \land (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X \in B \land \underset{˙}{0} \in B)) \land F (F^{-1} (\underset{˙}{0}) \underset{˙}{+} X) = F (\underset{˙}{0})) \to F^{-1} (\underset{˙}{0}) \underset{˙}{+} X = \underset{˙}{0}$
70	41 45 67 69	syl21anc	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to F^{-1} (\underset{˙}{0}) \underset{˙}{+} X = \underset{˙}{0}$
71	31 39 70	rspcedvdw	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}$
72	29 71	r19.29a	$⊢ (φ \land F : B \underset{1-1 onto}{⟶} B) \to \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})$
73		oveq1	$⊢ v = y \to v \underset{˙}{+} X = y \underset{˙}{+} X$
74	73	eqeq1d	$⊢ v = y \to (v \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow y \underset{˙}{+} X = \underset{˙}{0})$
75		simplr	$⊢ ((φ \land y \in B) \land (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to y \in B$
76		simprr	$⊢ ((φ \land y \in B) \land (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to y \underset{˙}{+} X = \underset{˙}{0}$
77	74 75 76	rspcedvdw	$⊢ ((φ \land y \in B) \land (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}$
78		oveq2	$⊢ u = y \to X \underset{˙}{+} u = X \underset{˙}{+} y$
79	78	eqeq1d	$⊢ u = y \to (X \underset{˙}{+} u = \underset{˙}{0} \leftrightarrow X \underset{˙}{+} y = \underset{˙}{0})$
80		simprl	$⊢ ((φ \land y \in B) \land (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to X \underset{˙}{+} y = \underset{˙}{0}$
81	79 75 80	rspcedvdw	$⊢ ((φ \land y \in B) \land (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}$
82	77 81	jca	$⊢ ((φ \land y \in B) \land (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to (\exists v \in B v \underset{˙}{+} X = \underset{˙}{0} \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0})$
83	82	r19.29an	$⊢ (φ \land \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to (\exists v \in B v \underset{˙}{+} X = \underset{˙}{0} \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0})$
84	5	ad2antrr	$⊢ ((φ \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to E \in Mnd$
85	6	ad2antrr	$⊢ ((φ \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to X \in B$
86		simplr	$⊢ ((φ \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to v \in B$
87		simpr	$⊢ ((φ \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to v \underset{˙}{+} X = \underset{˙}{0}$
88	1 2 3 4 84 85 86 87	mndlactf1	$⊢ ((φ \land v \in B) \land v \underset{˙}{+} X = \underset{˙}{0}) \to F : B \underset{1-1}{⟶} B$
89	88	r19.29an	$⊢ (φ \land \exists v \in B v \underset{˙}{+} X = \underset{˙}{0}) \to F : B \underset{1-1}{⟶} B$
90	25	biimpar	$⊢ (φ \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0}) \to F : B \underset{onto}{⟶} B$
91	89 90	anim12dan	$⊢ (φ \land (\exists v \in B v \underset{˙}{+} X = \underset{˙}{0} \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0})) \to (F : B \underset{1-1}{⟶} B \land F : B \underset{onto}{⟶} B)$
92		df-f1o	$⊢ F : B \underset{1-1 onto}{⟶} B \leftrightarrow (F : B \underset{1-1}{⟶} B \land F : B \underset{onto}{⟶} B)$
93	91 92	sylibr	$⊢ (φ \land (\exists v \in B v \underset{˙}{+} X = \underset{˙}{0} \land \exists u \in B X \underset{˙}{+} u = \underset{˙}{0})) \to F : B \underset{1-1 onto}{⟶} B$
94	83 93	syldan	$⊢ (φ \land \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0})) \to F : B \underset{1-1 onto}{⟶} B$
95	72 94	impbida	$⊢ φ \to (F : B \underset{1-1 onto}{⟶} B \leftrightarrow \exists y \in B (X \underset{˙}{+} y = \underset{˙}{0} \land y \underset{˙}{+} X = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem mndlactf1o

Proof