Theorem mndractf1o

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

	Ref	Expression
Hypotheses	mndractf1o.b	$$⊢B={\mathrm{Base}}_E$$
	mndractf1o.z	$$⊢\underset{\dot{}}{0}=0_E$$
	mndractf1o.p	$$⊢\underset{\dot{}}{+}={+}_E$$
	mndractf1o.f	$$⊢G=\left(a\in B⟼a\underset{\dot{}}{+}X\right)$$
	mndractf1o.e	$$⊢\phi \to E\in \mathrm{Mnd}$$
	mndractf1o.x	$$⊢\phi \to X\in B$$
Assertion	mndractf1o	$$⊢\phi \to \left(G:B\underset{1-1\; onto}{⟶}B\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{+}y=\underset{\dot{}}{0}\wedge y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mndractf1o.b	$$⊢B={\mathrm{Base}}_E$$
2		mndractf1o.z	$$⊢\underset{\dot{}}{0}=0_E$$
3		mndractf1o.p	$$⊢\underset{\dot{}}{+}={+}_E$$
4		mndractf1o.f	$$⊢G=\left(a\in B⟼a\underset{\dot{}}{+}X\right)$$
5		mndractf1o.e	$$⊢\phi \to E\in \mathrm{Mnd}$$
6		mndractf1o.x	$$⊢\phi \to X\in B$$
7		oveq2	$$⊢v=G^{-1}\left(\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{+}v=X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)$$
8	7	eqeq1d	$$⊢v=G^{-1}\left(\underset{\dot{}}{0}\right)\to \left(X\underset{\dot{}}{+}v=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\right)$$
9		f1ocnv	$$⊢G:B\underset{1-1\; onto}{⟶}B\to G^{-1}:B\underset{1-1\; onto}{⟶}B$$
10		f1of	$$⊢G^{-1}:B\underset{1-1\; onto}{⟶}B\to G^{-1}:B⟶B$$
11	9 10	syl	$$⊢G:B\underset{1-1\; onto}{⟶}B\to G^{-1}:B⟶B$$
12	11	adantl	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G^{-1}:B⟶B$$
13	1 2	mndidcl	$$⊢E\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
14	5 13	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
15	14	adantr	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \underset{\dot{}}{0}\in B$$
16	12 15	ffvelcdmd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G^{-1}\left(\underset{\dot{}}{0}\right)\in B$$
17		f1of1	$$⊢G:B\underset{1-1\; onto}{⟶}B\to G:B\underset{1-1}{⟶}B$$
18	17	adantl	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G:B\underset{1-1}{⟶}B$$
19	5	adantr	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to E\in \mathrm{Mnd}$$
20	6	adantr	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to X\in B$$
21	1 3 19 20 16	mndcld	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\in B$$
22	21 15	jca	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\in B\wedge \underset{\dot{}}{0}\in B\right)$$
23	1 3 2	mndlid	$$⊢\left(E\in \mathrm{Mnd}\wedge X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
24	19 20 23	syl2anc	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X=X$$
25		oveq1	$$⊢a=\underset{\dot{}}{0}\to a\underset{\dot{}}{+}X=\underset{\dot{}}{0}\underset{\dot{}}{+}X$$
26		ovexd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}X\in \mathrm{V}$$
27	4 25 15 26	fvmptd3	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\underset{\dot{}}{+}X$$
28		oveq1	$$⊢a=X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\to a\underset{\dot{}}{+}X=\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{+}X$$
29		ovexd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{+}X\in \mathrm{V}$$
30	4 28 21 29	fvmptd3	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)=\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{+}X$$
31	1 3 19 20 16 20	mndassd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{+}X=X\underset{\dot{}}{+}\left(G^{-1}\left(\underset{\dot{}}{0}\right)\underset{\dot{}}{+}X\right)$$
32		oveq1	$$⊢a=G^{-1}\left(\underset{\dot{}}{0}\right)\to a\underset{\dot{}}{+}X=G^{-1}\left(\underset{\dot{}}{0}\right)\underset{\dot{}}{+}X$$
33		ovexd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G^{-1}\left(\underset{\dot{}}{0}\right)\underset{\dot{}}{+}X\in \mathrm{V}$$
34	4 32 16 33	fvmptd3	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G\left(G^{-1}\left(\underset{\dot{}}{0}\right)\right)=G^{-1}\left(\underset{\dot{}}{0}\right)\underset{\dot{}}{+}X$$
35		simpr	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G:B\underset{1-1\; onto}{⟶}B$$
36		f1ocnvfv2	$$⊢\left(G:B\underset{1-1\; onto}{⟶}B\wedge \underset{\dot{}}{0}\in B\right)\to G\left(G^{-1}\left(\underset{\dot{}}{0}\right)\right)=\underset{\dot{}}{0}$$
37	35 15 36	syl2anc	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G\left(G^{-1}\left(\underset{\dot{}}{0}\right)\right)=\underset{\dot{}}{0}$$
38	34 37	eqtr3d	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G^{-1}\left(\underset{\dot{}}{0}\right)\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
39	38	oveq2d	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to X\underset{\dot{}}{+}\left(G^{-1}\left(\underset{\dot{}}{0}\right)\underset{\dot{}}{+}X\right)=X\underset{\dot{}}{+}\underset{\dot{}}{0}$$
40	1 3 2	mndrid	$$⊢\left(E\in \mathrm{Mnd}\wedge X\in B\right)\to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$
41	19 20 40	syl2anc	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to X\underset{\dot{}}{+}\underset{\dot{}}{0}=X$$
42	31 39 41	3eqtrd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{+}X=X$$
43	30 42	eqtrd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)=X$$
44	24 27 43	3eqtr4rd	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to G\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)=G\left(\underset{\dot{}}{0}\right)$$
45		f1fveq	$$⊢\left(G:B\underset{1-1}{⟶}B\wedge \left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\in B\wedge \underset{\dot{}}{0}\in B\right)\right)\to \left(G\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)=G\left(\underset{\dot{}}{0}\right)\leftrightarrow X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\right)$$
46	45	biimpa	$$⊢\left(\left(G:B\underset{1-1}{⟶}B\wedge \left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\in B\wedge \underset{\dot{}}{0}\in B\right)\right)\wedge G\left(X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)\right)=G\left(\underset{\dot{}}{0}\right)\right)\to X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
47	18 22 44 46	syl21anc	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to X\underset{\dot{}}{+}{G}^{-1}\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
48	8 16 47	rspcedvdw	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}$$
49		f1ofo	$$⊢G:B\underset{1-1\; onto}{⟶}B\to G:B\underset{onto}{⟶}B$$
50	1 2 3 4 5 6	mndractfo	$$⊢\phi \to \left(G:B\underset{onto}{⟶}B\leftrightarrow \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
51	50	biimpa	$$⊢\left(\phi \wedge G:B\underset{onto}{⟶}B\right)\to \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
52	49 51	sylan2	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}$$
53	48 52	jca	$$⊢\left(\phi \wedge G:B\underset{1-1\; onto}{⟶}B\right)\to \left(\exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}\wedge \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)$$
54	5	ad2antrr	$$⊢\left(\left(\phi \wedge v\in B\right)\wedge X\underset{\dot{}}{+}v=\underset{\dot{}}{0}\right)\to E\in \mathrm{Mnd}$$
55	6	ad2antrr	$$⊢\left(\left(\phi \wedge v\in B\right)\wedge X\underset{\dot{}}{+}v=\underset{\dot{}}{0}\right)\to X\in B$$
56		simplr	$$⊢\left(\left(\phi \wedge v\in B\right)\wedge X\underset{\dot{}}{+}v=\underset{\dot{}}{0}\right)\to v\in B$$
57		simpr	$$⊢\left(\left(\phi \wedge v\in B\right)\wedge X\underset{\dot{}}{+}v=\underset{\dot{}}{0}\right)\to X\underset{\dot{}}{+}v=\underset{\dot{}}{0}$$
58	1 2 3 4 54 55 56 57	mndractf1	$$⊢\left(\left(\phi \wedge v\in B\right)\wedge X\underset{\dot{}}{+}v=\underset{\dot{}}{0}\right)\to G:B\underset{1-1}{⟶}B$$
59	58	r19.29an	$$⊢\left(\phi \wedge \exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}\right)\to G:B\underset{1-1}{⟶}B$$
60	50	biimpar	$$⊢\left(\phi \wedge \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\to G:B\underset{onto}{⟶}B$$
61	59 60	anim12dan	$$⊢\left(\phi \wedge \left(\exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}\wedge \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\right)\to \left(G:B\underset{1-1}{⟶}B\wedge G:B\underset{onto}{⟶}B\right)$$
62		df-f1o	$$⊢G:B\underset{1-1\; onto}{⟶}B\leftrightarrow \left(G:B\underset{1-1}{⟶}B\wedge G:B\underset{onto}{⟶}B\right)$$
63	61 62	sylibr	$$⊢\left(\phi \wedge \left(\exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}\wedge \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\right)\to G:B\underset{1-1\; onto}{⟶}B$$
64	53 63	impbida	$$⊢\phi \to \left(G:B\underset{1-1\; onto}{⟶}B\leftrightarrow \left(\exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}\wedge \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\right)$$
65	1 2 3 5 6	mndlrinvb	$$⊢\phi \to \left(\left(\exists v\in BX\underset{\dot{}}{+}v=\underset{\dot{}}{0}\wedge \exists w\in Bw\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{+}y=\underset{\dot{}}{0}\wedge y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\right)$$
66	64 65	bitrd	$$⊢\phi \to \left(G:B\underset{1-1\; onto}{⟶}B\leftrightarrow \exists y\in B\left(X\underset{\dot{}}{+}y=\underset{\dot{}}{0}\wedge y\underset{\dot{}}{+}X=\underset{\dot{}}{0}\right)\right)$$