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

Theorem mndlactf1o 33018
Description: An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19075. Remark in chapter I. of [BourbakiAlg1] p. 17. (Contributed by Thierry Arnoux, 3-Aug-2025.)
Hypotheses
Ref Expression
mndlactf1o.b 𝐵 = (Base‘𝐸)
mndlactf1o.z 0 = (0g𝐸)
mndlactf1o.p + = (+g𝐸)
mndlactf1o.f 𝐹 = (𝑎𝐵 ↦ (𝑋 + 𝑎))
mndlactf1o.e (𝜑𝐸 ∈ Mnd)
mndlactf1o.x (𝜑𝑋𝐵)
Assertion
Ref Expression
mndlactf1o (𝜑 → (𝐹:𝐵1-1-onto𝐵 ↔ ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
Distinct variable groups:   + ,𝑎,𝑦   0 ,𝑎,𝑦   𝐵,𝑎,𝑦   𝐹,𝑎,𝑦   𝑋,𝑎,𝑦   𝜑,𝑎,𝑦
Allowed substitution hints:   𝐸(𝑦,𝑎)

Proof of Theorem mndlactf1o
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7439 . . . . . . 7 (𝑦 = 𝑢 → (𝑋 + 𝑦) = (𝑋 + 𝑢))
21eqeq1d 2737 . . . . . 6 (𝑦 = 𝑢 → ((𝑋 + 𝑦) = 0 ↔ (𝑋 + 𝑢) = 0 ))
3 oveq1 7438 . . . . . . 7 (𝑦 = 𝑢 → (𝑦 + 𝑋) = (𝑢 + 𝑋))
43eqeq1d 2737 . . . . . 6 (𝑦 = 𝑢 → ((𝑦 + 𝑋) = 0 ↔ (𝑢 + 𝑋) = 0 ))
52, 4anbi12d 632 . . . . 5 (𝑦 = 𝑢 → (((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ) ↔ ((𝑋 + 𝑢) = 0 ∧ (𝑢 + 𝑋) = 0 )))
6 simplr 769 . . . . 5 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑢𝐵)
7 simpr 484 . . . . . 6 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑋 + 𝑢) = 0 )
8 mndlactf1o.b . . . . . . . . 9 𝐵 = (Base‘𝐸)
9 mndlactf1o.z . . . . . . . . 9 0 = (0g𝐸)
10 mndlactf1o.p . . . . . . . . 9 + = (+g𝐸)
11 mndlactf1o.e . . . . . . . . . 10 (𝜑𝐸 ∈ Mnd)
1211ad5antr 734 . . . . . . . . 9 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝐸 ∈ Mnd)
13 mndlactf1o.x . . . . . . . . . 10 (𝜑𝑋𝐵)
1413ad5antr 734 . . . . . . . . 9 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑋𝐵)
15 simp-4r 784 . . . . . . . . 9 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑣𝐵)
16 simpllr 776 . . . . . . . . 9 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑣 + 𝑋) = 0 )
178, 9, 10, 12, 14, 15, 6, 16, 7mndlrinv 33012 . . . . . . . 8 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → 𝑣 = 𝑢)
1817oveq1d 7446 . . . . . . 7 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑣 + 𝑋) = (𝑢 + 𝑋))
1918, 16eqtr3d 2777 . . . . . 6 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → (𝑢 + 𝑋) = 0 )
207, 19jca 511 . . . . 5 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → ((𝑋 + 𝑢) = 0 ∧ (𝑢 + 𝑋) = 0 ))
215, 6, 20rspcedvdw 3625 . . . 4 ((((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) ∧ 𝑢𝐵) ∧ (𝑋 + 𝑢) = 0 ) → ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))
22 f1ofo 6856 . . . . . . 7 (𝐹:𝐵1-1-onto𝐵𝐹:𝐵onto𝐵)
2322adantl 481 . . . . . 6 ((𝜑𝐹:𝐵1-1-onto𝐵) → 𝐹:𝐵onto𝐵)
24 mndlactf1o.f . . . . . . . 8 𝐹 = (𝑎𝐵 ↦ (𝑋 + 𝑎))
258, 9, 10, 24, 11, 13mndlactfo 33015 . . . . . . 7 (𝜑 → (𝐹:𝐵onto𝐵 ↔ ∃𝑢𝐵 (𝑋 + 𝑢) = 0 ))
2625biimpa 476 . . . . . 6 ((𝜑𝐹:𝐵onto𝐵) → ∃𝑢𝐵 (𝑋 + 𝑢) = 0 )
2723, 26syldan 591 . . . . 5 ((𝜑𝐹:𝐵1-1-onto𝐵) → ∃𝑢𝐵 (𝑋 + 𝑢) = 0 )
2827ad2antrr 726 . . . 4 ((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → ∃𝑢𝐵 (𝑋 + 𝑢) = 0 )
2921, 28r19.29a 3160 . . 3 ((((𝜑𝐹:𝐵1-1-onto𝐵) ∧ 𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))
30 oveq1 7438 . . . . 5 (𝑣 = (𝐹0 ) → (𝑣 + 𝑋) = ((𝐹0 ) + 𝑋))
3130eqeq1d 2737 . . . 4 (𝑣 = (𝐹0 ) → ((𝑣 + 𝑋) = 0 ↔ ((𝐹0 ) + 𝑋) = 0 ))
32 f1ocnv 6861 . . . . . . 7 (𝐹:𝐵1-1-onto𝐵𝐹:𝐵1-1-onto𝐵)
33 f1of 6849 . . . . . . 7 (𝐹:𝐵1-1-onto𝐵𝐹:𝐵𝐵)
3432, 33syl 17 . . . . . 6 (𝐹:𝐵1-1-onto𝐵𝐹:𝐵𝐵)
3534adantl 481 . . . . 5 ((𝜑𝐹:𝐵1-1-onto𝐵) → 𝐹:𝐵𝐵)
368, 9mndidcl 18775 . . . . . . 7 (𝐸 ∈ Mnd → 0𝐵)
3711, 36syl 17 . . . . . 6 (𝜑0𝐵)
3837adantr 480 . . . . 5 ((𝜑𝐹:𝐵1-1-onto𝐵) → 0𝐵)
3935, 38ffvelcdmd 7105 . . . 4 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹0 ) ∈ 𝐵)
40 f1of1 6848 . . . . . 6 (𝐹:𝐵1-1-onto𝐵𝐹:𝐵1-1𝐵)
4140adantl 481 . . . . 5 ((𝜑𝐹:𝐵1-1-onto𝐵) → 𝐹:𝐵1-1𝐵)
4211adantr 480 . . . . . . 7 ((𝜑𝐹:𝐵1-1-onto𝐵) → 𝐸 ∈ Mnd)
4313adantr 480 . . . . . . 7 ((𝜑𝐹:𝐵1-1-onto𝐵) → 𝑋𝐵)
448, 10, 42, 39, 43mndcld 33010 . . . . . 6 ((𝜑𝐹:𝐵1-1-onto𝐵) → ((𝐹0 ) + 𝑋) ∈ 𝐵)
4544, 38jca 511 . . . . 5 ((𝜑𝐹:𝐵1-1-onto𝐵) → (((𝐹0 ) + 𝑋) ∈ 𝐵0𝐵))
468, 10, 9mndrid 18781 . . . . . . 7 ((𝐸 ∈ Mnd ∧ 𝑋𝐵) → (𝑋 + 0 ) = 𝑋)
4742, 43, 46syl2anc 584 . . . . . 6 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝑋 + 0 ) = 𝑋)
48 oveq2 7439 . . . . . . 7 (𝑎 = 0 → (𝑋 + 𝑎) = (𝑋 + 0 ))
49 ovexd 7466 . . . . . . 7 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝑋 + 0 ) ∈ V)
5024, 48, 38, 49fvmptd3 7039 . . . . . 6 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹0 ) = (𝑋 + 0 ))
51 oveq2 7439 . . . . . . . 8 (𝑎 = ((𝐹0 ) + 𝑋) → (𝑋 + 𝑎) = (𝑋 + ((𝐹0 ) + 𝑋)))
52 ovexd 7466 . . . . . . . 8 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝑋 + ((𝐹0 ) + 𝑋)) ∈ V)
5324, 51, 44, 52fvmptd3 7039 . . . . . . 7 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹‘((𝐹0 ) + 𝑋)) = (𝑋 + ((𝐹0 ) + 𝑋)))
54 oveq2 7439 . . . . . . . . . . 11 (𝑎 = (𝐹0 ) → (𝑋 + 𝑎) = (𝑋 + (𝐹0 )))
55 ovexd 7466 . . . . . . . . . . 11 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝑋 + (𝐹0 )) ∈ V)
5624, 54, 39, 55fvmptd3 7039 . . . . . . . . . 10 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹‘(𝐹0 )) = (𝑋 + (𝐹0 )))
57 simpr 484 . . . . . . . . . . 11 ((𝜑𝐹:𝐵1-1-onto𝐵) → 𝐹:𝐵1-1-onto𝐵)
58 f1ocnvfv2 7297 . . . . . . . . . . 11 ((𝐹:𝐵1-1-onto𝐵0𝐵) → (𝐹‘(𝐹0 )) = 0 )
5957, 38, 58syl2anc 584 . . . . . . . . . 10 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹‘(𝐹0 )) = 0 )
6056, 59eqtr3d 2777 . . . . . . . . 9 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝑋 + (𝐹0 )) = 0 )
6160oveq1d 7446 . . . . . . . 8 ((𝜑𝐹:𝐵1-1-onto𝐵) → ((𝑋 + (𝐹0 )) + 𝑋) = ( 0 + 𝑋))
628, 10, 42, 43, 39, 43mndassd 33011 . . . . . . . 8 ((𝜑𝐹:𝐵1-1-onto𝐵) → ((𝑋 + (𝐹0 )) + 𝑋) = (𝑋 + ((𝐹0 ) + 𝑋)))
638, 10, 9mndlid 18780 . . . . . . . . 9 ((𝐸 ∈ Mnd ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)
6442, 43, 63syl2anc 584 . . . . . . . 8 ((𝜑𝐹:𝐵1-1-onto𝐵) → ( 0 + 𝑋) = 𝑋)
6561, 62, 643eqtr3d 2783 . . . . . . 7 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝑋 + ((𝐹0 ) + 𝑋)) = 𝑋)
6653, 65eqtrd 2775 . . . . . 6 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹‘((𝐹0 ) + 𝑋)) = 𝑋)
6747, 50, 663eqtr4rd 2786 . . . . 5 ((𝜑𝐹:𝐵1-1-onto𝐵) → (𝐹‘((𝐹0 ) + 𝑋)) = (𝐹0 ))
68 f1fveq 7282 . . . . . 6 ((𝐹:𝐵1-1𝐵 ∧ (((𝐹0 ) + 𝑋) ∈ 𝐵0𝐵)) → ((𝐹‘((𝐹0 ) + 𝑋)) = (𝐹0 ) ↔ ((𝐹0 ) + 𝑋) = 0 ))
6968biimpa 476 . . . . 5 (((𝐹:𝐵1-1𝐵 ∧ (((𝐹0 ) + 𝑋) ∈ 𝐵0𝐵)) ∧ (𝐹‘((𝐹0 ) + 𝑋)) = (𝐹0 )) → ((𝐹0 ) + 𝑋) = 0 )
7041, 45, 67, 69syl21anc 838 . . . 4 ((𝜑𝐹:𝐵1-1-onto𝐵) → ((𝐹0 ) + 𝑋) = 0 )
7131, 39, 70rspcedvdw 3625 . . 3 ((𝜑𝐹:𝐵1-1-onto𝐵) → ∃𝑣𝐵 (𝑣 + 𝑋) = 0 )
7229, 71r19.29a 3160 . 2 ((𝜑𝐹:𝐵1-1-onto𝐵) → ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))
73 oveq1 7438 . . . . . . 7 (𝑣 = 𝑦 → (𝑣 + 𝑋) = (𝑦 + 𝑋))
7473eqeq1d 2737 . . . . . 6 (𝑣 = 𝑦 → ((𝑣 + 𝑋) = 0 ↔ (𝑦 + 𝑋) = 0 ))
75 simplr 769 . . . . . 6 (((𝜑𝑦𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → 𝑦𝐵)
76 simprr 773 . . . . . 6 (((𝜑𝑦𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (𝑦 + 𝑋) = 0 )
7774, 75, 76rspcedvdw 3625 . . . . 5 (((𝜑𝑦𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → ∃𝑣𝐵 (𝑣 + 𝑋) = 0 )
78 oveq2 7439 . . . . . . 7 (𝑢 = 𝑦 → (𝑋 + 𝑢) = (𝑋 + 𝑦))
7978eqeq1d 2737 . . . . . 6 (𝑢 = 𝑦 → ((𝑋 + 𝑢) = 0 ↔ (𝑋 + 𝑦) = 0 ))
80 simprl 771 . . . . . 6 (((𝜑𝑦𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (𝑋 + 𝑦) = 0 )
8179, 75, 80rspcedvdw 3625 . . . . 5 (((𝜑𝑦𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → ∃𝑢𝐵 (𝑋 + 𝑢) = 0 )
8277, 81jca 511 . . . 4 (((𝜑𝑦𝐵) ∧ ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (∃𝑣𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢𝐵 (𝑋 + 𝑢) = 0 ))
8382r19.29an 3156 . . 3 ((𝜑 ∧ ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → (∃𝑣𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢𝐵 (𝑋 + 𝑢) = 0 ))
8411ad2antrr 726 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝐸 ∈ Mnd)
8513ad2antrr 726 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝑋𝐵)
86 simplr 769 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝑣𝐵)
87 simpr 484 . . . . . . 7 (((𝜑𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → (𝑣 + 𝑋) = 0 )
888, 9, 10, 24, 84, 85, 86, 87mndlactf1 33014 . . . . . 6 (((𝜑𝑣𝐵) ∧ (𝑣 + 𝑋) = 0 ) → 𝐹:𝐵1-1𝐵)
8988r19.29an 3156 . . . . 5 ((𝜑 ∧ ∃𝑣𝐵 (𝑣 + 𝑋) = 0 ) → 𝐹:𝐵1-1𝐵)
9025biimpar 477 . . . . 5 ((𝜑 ∧ ∃𝑢𝐵 (𝑋 + 𝑢) = 0 ) → 𝐹:𝐵onto𝐵)
9189, 90anim12dan 619 . . . 4 ((𝜑 ∧ (∃𝑣𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢𝐵 (𝑋 + 𝑢) = 0 )) → (𝐹:𝐵1-1𝐵𝐹:𝐵onto𝐵))
92 df-f1o 6570 . . . 4 (𝐹:𝐵1-1-onto𝐵 ↔ (𝐹:𝐵1-1𝐵𝐹:𝐵onto𝐵))
9391, 92sylibr 234 . . 3 ((𝜑 ∧ (∃𝑣𝐵 (𝑣 + 𝑋) = 0 ∧ ∃𝑢𝐵 (𝑋 + 𝑢) = 0 )) → 𝐹:𝐵1-1-onto𝐵)
9483, 93syldan 591 . 2 ((𝜑 ∧ ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )) → 𝐹:𝐵1-1-onto𝐵)
9572, 94impbida 801 1 (𝜑 → (𝐹:𝐵1-1-onto𝐵 ↔ ∃𝑦𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wrex 3068  Vcvv 3478  cmpt 5231  ccnv 5688  wf 6559  1-1wf1 6560  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  Basecbs 17245  +gcplusg 17298  0gc0g 17486  Mndcmnd 18760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-0g 17488  df-mgm 18666  df-sgrp 18745  df-mnd 18761
This theorem is referenced by:  assarrginv  33664
  Copyright terms: Public domain W3C validator