mndractf1o - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mndractf1o		Structured version Visualization version GIF version

Theorem mndractf1o 33264

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

**Hypotheses**
Ref	Expression
mndractf1o.b	⊢ 𝐵 = (Base‘𝐸)
mndractf1o.z	⊢ 0 = (0_g‘𝐸)
mndractf1o.p	⊢ + = (+_g‘𝐸)
mndractf1o.f	⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
mndractf1o.e	⊢ (𝜑 → 𝐸 ∈ Mnd)
mndractf1o.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

**Assertion**
Ref	Expression
mndractf1o	⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))

Distinct variable groups: + ,𝑎,𝑦 0 ,𝑎,𝑦 𝐵,𝑎,𝑦 𝐺,𝑎,𝑦 𝑋,𝑎,𝑦 𝜑,𝑎,𝑦 Allowed substitution hints: 𝐸(𝑦,𝑎)

Proof of Theorem mndractf1o Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7408	. . . . . 6 ⊢ (𝑣 = (^◡𝐺‘ 0 ) → (𝑋 + 𝑣) = (𝑋 + (^◡𝐺‘ 0 )))
2	1	eqeq1d 2767	. . . . 5 ⊢ (𝑣 = (^◡𝐺‘ 0 ) → ((𝑋 + 𝑣) = 0 ↔ (𝑋 + (^◡𝐺‘ 0 )) = 0 ))
3		f1ocnv 6823	. . . . . . . 8 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ^◡𝐺:𝐵–1-1-onto→𝐵)
4		f1of 6810	. . . . . . . 8 ⊢ (^◡𝐺:𝐵–1-1-onto→𝐵 → ^◡𝐺:𝐵⟶𝐵)
5	3, 4	syl 18	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → ^◡𝐺:𝐵⟶𝐵)
6	5	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ^◡𝐺:𝐵⟶𝐵)
7		mndractf1o.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Mnd)
8		mndractf1o.b	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝐸)
9		mndractf1o.z	. . . . . . . . 9 ⊢ 0 = (0_g‘𝐸)
10	8, 9	mndidcl 18797	. . . . . . . 8 ⊢ (𝐸 ∈ Mnd → 0 ∈ 𝐵)
11	7, 10	syl 18	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
12	11	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 0 ∈ 𝐵)
13	6, 12	ffvelcdmd 7070	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (^◡𝐺‘ 0 ) ∈ 𝐵)
14		f1of1 6809	. . . . . . 7 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–1-1→𝐵)
15	14	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1→𝐵)
16		mndractf1o.p	. . . . . . . 8 ⊢ + = (+_g‘𝐸)
17	7	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐸 ∈ Mnd)
18		mndractf1o.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
19	18	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝑋 ∈ 𝐵)
20	8, 16, 17, 19, 13	mndcld 33255	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (^◡𝐺‘ 0 )) ∈ 𝐵)
21	20, 12	jca 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (^◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵))
22	8, 16, 9	mndlid 18802	. . . . . . . 8 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
23	17, 19, 22	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) = 𝑋)
24		mndractf1o.f	. . . . . . . 8 ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋))
25		oveq1 7407	. . . . . . . 8 ⊢ (𝑎 = 0 → (𝑎 + 𝑋) = ( 0 + 𝑋))
26		ovexd 7435	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ( 0 + 𝑋) ∈ V)
27	24, 25, 12, 26	fvmptd3 7003	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘ 0 ) = ( 0 + 𝑋))
28		oveq1 7407	. . . . . . . . 9 ⊢ (𝑎 = (𝑋 + (^◡𝐺‘ 0 )) → (𝑎 + 𝑋) = ((𝑋 + (^◡𝐺‘ 0 )) + 𝑋))
29		ovexd 7435	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (^◡𝐺‘ 0 )) + 𝑋) ∈ V)
30	24, 28, 20, 29	fvmptd3 7003	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (^◡𝐺‘ 0 ))) = ((𝑋 + (^◡𝐺‘ 0 )) + 𝑋))
31	8, 16, 17, 19, 13, 19	mndassd 33256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (^◡𝐺‘ 0 )) + 𝑋) = (𝑋 + ((^◡𝐺‘ 0 ) + 𝑋)))
32		oveq1 7407	. . . . . . . . . . . 12 ⊢ (𝑎 = (^◡𝐺‘ 0 ) → (𝑎 + 𝑋) = ((^◡𝐺‘ 0 ) + 𝑋))
33		ovexd 7435	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((^◡𝐺‘ 0 ) + 𝑋) ∈ V)
34	24, 32, 13, 33	fvmptd3 7003	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(^◡𝐺‘ 0 )) = ((^◡𝐺‘ 0 ) + 𝑋))
35		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → 𝐺:𝐵–1-1-onto→𝐵)
36		f1ocnvfv2 7265	. . . . . . . . . . . 12 ⊢ ((𝐺:𝐵–1-1-onto→𝐵 ∧ 0 ∈ 𝐵) → (𝐺‘(^◡𝐺‘ 0 )) = 0 )
37	35, 12, 36	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(^◡𝐺‘ 0 )) = 0 )
38	34, 37	eqtr3d 2802	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((^◡𝐺‘ 0 ) + 𝑋) = 0 )
39	38	oveq2d 7416	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + ((^◡𝐺‘ 0 ) + 𝑋)) = (𝑋 + 0 ))
40	8, 16, 9	mndrid 18803	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
41	17, 19, 40	syl2anc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + 0 ) = 𝑋)
42	31, 39, 41	3eqtrd 2804	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ((𝑋 + (^◡𝐺‘ 0 )) + 𝑋) = 𝑋)
43	30, 42	eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (^◡𝐺‘ 0 ))) = 𝑋)
44	23, 27, 43	3eqtr4rd 2811	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝐺‘(𝑋 + (^◡𝐺‘ 0 ))) = (𝐺‘ 0 ))
45		f1fveq 7250	. . . . . . 7 ⊢ ((𝐺:𝐵–1-1→𝐵 ∧ ((𝑋 + (^◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵)) → ((𝐺‘(𝑋 + (^◡𝐺‘ 0 ))) = (𝐺‘ 0 ) ↔ (𝑋 + (^◡𝐺‘ 0 )) = 0 ))
46	45	biimpa 481	. . . . . 6 ⊢ (((𝐺:𝐵–1-1→𝐵 ∧ ((𝑋 + (^◡𝐺‘ 0 )) ∈ 𝐵 ∧ 0 ∈ 𝐵)) ∧ (𝐺‘(𝑋 + (^◡𝐺‘ 0 ))) = (𝐺‘ 0 )) → (𝑋 + (^◡𝐺‘ 0 )) = 0 )
47	15, 21, 44, 46	syl21anc 850	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (𝑋 + (^◡𝐺‘ 0 )) = 0 )
48	2, 13, 47	rspcedvdw 3587	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 )
49		f1ofo 6818	. . . . 5 ⊢ (𝐺:𝐵–1-1-onto→𝐵 → 𝐺:𝐵–onto→𝐵)
50	8, 9, 16, 24, 7, 18	mndractfo 33262	. . . . . 6 ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
51	50	biimpa 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐺:𝐵–onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
52	49, 51	sylan2 604	. . . 4 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )
53	48, 52	jca 520	. . 3 ⊢ ((𝜑 ∧ 𝐺:𝐵–1-1-onto→𝐵) → (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ))
54	7	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐸 ∈ Mnd)
55	18	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑋 ∈ 𝐵)
56		simplr 780	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝑣 ∈ 𝐵)
57		simpr 489	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → (𝑋 + 𝑣) = 0 )
58	8, 9, 16, 24, 54, 55, 56, 57	mndractf1 33261	. . . . . 6 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
59	58	r19.29an 3169	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ) → 𝐺:𝐵–1-1→𝐵)
60	50	biimpar 482	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) → 𝐺:𝐵–onto→𝐵)
61	59, 60	anim12dan 630	. . . 4 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
62		df-f1o 6532	. . . 4 ⊢ (𝐺:𝐵–1-1-onto→𝐵 ↔ (𝐺:𝐵–1-1→𝐵 ∧ 𝐺:𝐵–onto→𝐵))
63	61, 62	sylibr 237	. . 3 ⊢ ((𝜑 ∧ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )) → 𝐺:𝐵–1-1-onto→𝐵)
64	53, 63	impbida 812	. 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ (∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 )))
65	8, 9, 16, 7, 18	mndlrinvb 33258	. 2 ⊢ (𝜑 → ((∃𝑣 ∈ 𝐵 (𝑋 + 𝑣) = 0 ∧ ∃𝑤 ∈ 𝐵 (𝑤 + 𝑋) = 0 ) ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
66	64, 65	bitrd 282	1 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1563 ∈ wcel 2145 ∃wrex 3089 Vcvv 3457 ↦ cmpt 5186 ^◡ccnv 5651 ⟶wf 6521 –1-1→wf1 6522 –onto→wfo 6523 –1-1-onto→wf1o 6524 ‘cfv 6525 (class class class)co 7400 Basecbs 17259 +_gcplusg 17300 0_gc0g 17482 Mndcmnd 18782

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pr 5395

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-0g 17484 df-mgm 18688 df-sgrp 18767 df-mnd 18783

This theorem is referenced by: (None)

W3C validator