![]() |
Metamath
Proof Explorer Theorem List (p. 190 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efmndhash 18901 | The monoid of endofunctions on 𝑛 objects has cardinality 𝑛↑𝑛. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = ((♯‘𝐴)↑(♯‘𝐴))) | ||
Theorem | efmndbasfi 18902 | The monoid of endofunctions on a finite set 𝐴 is finite. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin) | ||
Theorem | efmndfv 18903 | The function value of an endofunction. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | efmndtset 18904 | The topology of the monoid of endofunctions on 𝐴. This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) = (TopSet‘𝐺)) | ||
Theorem | efmndplusg 18905* | The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) | ||
Theorem | efmndov 18906 | The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | efmndcl 18907 | The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | efmndtopn 18908 | The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
Theorem | symggrplem 18909* | Lemma for symggrp 19432 and efmndsgrp 18911. Conditions for an operation to be associative. Formerly part of proof for symggrp 19432. (Contributed by AV, 28-Jan-2024.) |
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦)) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | efmndmgm 18910 | The monoid of endofunctions on a class 𝐴 is a magma. (Contributed by AV, 28-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 ∈ Mgm | ||
Theorem | efmndsgrp 18911 | The monoid of endofunctions on a class 𝐴 is a semigroup. (Contributed by AV, 28-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 ∈ Smgrp | ||
Theorem | ielefmnd 18912 | The identity function restricted to a set 𝐴 is an element of the base set of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) | ||
Theorem | efmndid 18913 | The identity function restricted to a set 𝐴 is the identity element of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) = (0g‘𝐺)) | ||
Theorem | efmndmnd 18914 | The monoid of endofunctions on a set 𝐴 is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd) | ||
Theorem | efmnd0nmnd 18915 | Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
⊢ (EndoFMnd‘∅) ∈ Mnd | ||
Theorem | efmndbas0 18916 | The base set of the monoid of endofunctions on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 31-Mar-2024.) |
⊢ (Base‘(EndoFMnd‘∅)) = {∅} | ||
Theorem | efmnd1hash 18917 | The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1) | ||
Theorem | efmnd1bas 18918 | The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{〈𝐼, 𝐼〉}}) | ||
Theorem | efmnd2hash 18919 | The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 4) | ||
Theorem | submefmnd 18920* | If the base set of a monoid is contained in the base set of the monoid of endofunctions on a set 𝐴, contains the identity function and has the function composition as group operation, then its base set is a submonoid of the monoid of endofunctions on set 𝐴. Analogous to pgrpsubgsymg 19441. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐹 = (Base‘𝑆) ⇒ ⊢ (𝐴 ∈ 𝑉 → (((𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹) ∧ (+g‘𝑆) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubMnd‘𝑀))) | ||
Theorem | sursubmefmnd 18921* | The set of surjective endofunctions on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–onto→𝐴} ∈ (SubMnd‘𝑀)) | ||
Theorem | injsubmefmnd 18922* | The set of injective endofunctions on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∈ (SubMnd‘𝑀)) | ||
Theorem | idressubmefmnd 18923 | The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → {( I ↾ 𝐴)} ∈ (SubMnd‘𝐺)) | ||
Theorem | idresefmnd 18924 | The structure with the singleton containing only the identity function restricted to a set 𝐴 as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on 𝐴 to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on 𝐴. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐸 = (𝐺 ↾s {( I ↾ 𝐴)}) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐸 ∈ Mnd ∧ (Base‘𝐸) ⊆ (Base‘𝐺))) | ||
Theorem | smndex1ibas 18925 | The modulo function 𝐼 is an endofunction on ℕ0. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) ⇒ ⊢ 𝐼 ∈ (Base‘𝑀) | ||
Theorem | smndex1iidm 18926* | The modulo function 𝐼 is idempotent. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) ⇒ ⊢ (𝐼 ∘ 𝐼) = 𝐼 | ||
Theorem | smndex1gbas 18927* | The constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) ⇒ ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀)) | ||
Theorem | smndex1gid 18928* | The composition of a constant function (𝐺‘𝐾) with another endofunction on ℕ0 results in (𝐺‘𝐾) itself. (Contributed by AV, 14-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) ⇒ ⊢ ((𝐹 ∈ (Base‘𝑀) ∧ 𝐾 ∈ (0..^𝑁)) → ((𝐺‘𝐾) ∘ 𝐹) = (𝐺‘𝐾)) | ||
Theorem | smndex1igid 18929* | The composition of the modulo function 𝐼 and a constant function (𝐺‘𝐾) results in (𝐺‘𝐾) itself. (Contributed by AV, 14-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) ⇒ ⊢ (𝐾 ∈ (0..^𝑁) → (𝐼 ∘ (𝐺‘𝐾)) = (𝐺‘𝐾)) | ||
Theorem | smndex1basss 18930* | The modulo function 𝐼 and the constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) ⇒ ⊢ 𝐵 ⊆ (Base‘𝑀) | ||
Theorem | smndex1bas 18931* | The base set of the monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾). (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ (Base‘𝑆) = 𝐵 | ||
Theorem | smndex1mgm 18932* | The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a magma. (Contributed by AV, 14-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ 𝑆 ∈ Mgm | ||
Theorem | smndex1sgrp 18933* | The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a semigroup. (Contributed by AV, 14-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ 𝑆 ∈ Smgrp | ||
Theorem | smndex1mndlem 18934* | Lemma for smndex1mnd 18935 and smndex1id 18936. (Contributed by AV, 16-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ (𝑋 ∈ 𝐵 → ((𝐼 ∘ 𝑋) = 𝑋 ∧ (𝑋 ∘ 𝐼) = 𝑋)) | ||
Theorem | smndex1mnd 18935* | The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a monoid. (Contributed by AV, 16-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ 𝑆 ∈ Mnd | ||
Theorem | smndex1id 18936* | The modulo function 𝐼 is the identity of the monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾). (Contributed by AV, 16-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ 𝐼 = (0g‘𝑆) | ||
Theorem | smndex1n0mnd 18937* | The identity of the monoid 𝑀 of endofunctions on set ℕ0 is not contained in the base set of the constructed monoid 𝑆. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ (0g‘𝑀) ∉ 𝐵 | ||
Theorem | nsmndex1 18938* | The base set 𝐵 of the constructed monoid 𝑆 is not a submonoid of the monoid 𝑀 of endofunctions on set ℕ0, although 𝑀 ∈ Mnd and 𝑆 ∈ Mnd and 𝐵 ⊆ (Base‘𝑀) hold. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ 𝐵 ∉ (SubMnd‘𝑀) | ||
Theorem | smndex2dbas 18939 | The doubling function 𝐷 is an endofunction on ℕ0. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥)) ⇒ ⊢ 𝐷 ∈ 𝐵 | ||
Theorem | smndex2dnrinv 18940 | The doubling function 𝐷 has no right inverse in the monoid of endofunctions on ℕ0. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥)) ⇒ ⊢ ∀𝑓 ∈ 𝐵 (𝐷 ∘ 𝑓) ≠ 0 | ||
Theorem | smndex2hbas 18941 | The halving functions 𝐻 are endofunctions on ℕ0. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥)) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐻 = (𝑥 ∈ ℕ0 ↦ if(2 ∥ 𝑥, (𝑥 / 2), 𝑁)) ⇒ ⊢ 𝐻 ∈ 𝐵 | ||
Theorem | smndex2dlinvh 18942* | The halving functions 𝐻 are left inverses of the doubling function 𝐷. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥)) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐻 = (𝑥 ∈ ℕ0 ↦ if(2 ∥ 𝑥, (𝑥 / 2), 𝑁)) ⇒ ⊢ (𝐻 ∘ 𝐷) = 0 | ||
Theorem | mgm2nsgrplem1 18943* | Lemma 1 for mgm2nsgrp 18947: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 18680). (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
Theorem | mgm2nsgrplem2 18944* | Lemma 2 for mgm2nsgrp 18947. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴) | ||
Theorem | mgm2nsgrplem3 18945* | Lemma 3 for mgm2nsgrp 18947. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⚬ (𝐴 ⚬ 𝐵)) = 𝐵) | ||
Theorem | mgm2nsgrplem4 18946* | Lemma 4 for mgm2nsgrp 18947: M is not a semigroup. (Contributed by AV, 28-Jan-2020.) (Proof shortened by AV, 31-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Smgrp) | ||
Theorem | mgm2nsgrp 18947* | A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ Mgm ∧ 𝑀 ∉ Smgrp)) | ||
Theorem | sgrp2nmndlem1 18948* | Lemma 1 for sgrp2nmnd 18955: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 18680). (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
Theorem | sgrp2nmndlem2 18949* | Lemma 2 for sgrp2nmnd 18955. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ⚬ 𝐶) = 𝐴) | ||
Theorem | sgrp2nmndlem3 18950* | Lemma 3 for sgrp2nmnd 18955. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐶) = 𝐵) | ||
Theorem | sgrp2rid2 18951* | A small semigroup (with two elements) with two right identities which are different if 𝐴 ≠ 𝐵. (Contributed by AV, 10-Feb-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦) | ||
Theorem | sgrp2rid2ex 18952* | A small semigroup (with two elements) with two right identities which are different. (Contributed by AV, 10-Feb-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((♯‘𝑆) = 2 → ∃𝑥 ∈ 𝑆 ∃𝑧 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ≠ 𝑧 ∧ (𝑦 ⚬ 𝑥) = 𝑦 ∧ (𝑦 ⚬ 𝑧) = 𝑦)) | ||
Theorem | sgrp2nmndlem4 18953* | Lemma 4 for sgrp2nmnd 18955: M is a semigroup. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∈ Smgrp) | ||
Theorem | sgrp2nmndlem5 18954* | Lemma 5 for sgrp2nmnd 18955: M is not a monoid. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Mnd) | ||
Theorem | sgrp2nmnd 18955* | A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ Smgrp ∧ 𝑀 ∉ Mnd)) | ||
Theorem | mgmnsgrpex 18956 | There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.) |
⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ Smgrp | ||
Theorem | sgrpnmndex 18957 | There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.) |
⊢ ∃𝑚 ∈ Smgrp 𝑚 ∉ Mnd | ||
Theorem | sgrpssmgm 18958 | The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.) |
⊢ Smgrp ⊊ Mgm | ||
Theorem | mndsssgrp 18959 | The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.) |
⊢ Mnd ⊊ Smgrp | ||
Theorem | pwmndgplus 18960* | The operation of the monoid of the power set of a class 𝐴 under union. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋(+g‘𝑀)𝑌) = (𝑋 ∪ 𝑌)) | ||
Theorem | pwmndid 18961* | The identity of the monoid of the power set of a class 𝐴 under union is the empty set. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ (0g‘𝑀) = ∅ | ||
Theorem | pwmnd 18962* | The power set of a class 𝐴 is a monoid under union. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ 𝑀 ∈ Mnd | ||
Syntax | cgrp 18963 | Extend class notation with class of all groups. |
class Grp | ||
Syntax | cminusg 18964 | Extend class notation with inverse of group element. |
class invg | ||
Syntax | csg 18965 | Extend class notation with group subtraction (or division) operation. |
class -g | ||
Definition | df-grp 18966* | Define class of all groups. A group is a monoid (df-mnd 18760) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group 𝐺 is an algebraic structure formed from a base set of elements (notated (Base‘𝐺) per df-base 17245) and an internal group operation (notated (+g‘𝐺) per df-plusg 17310). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 18971), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 18972), identity (there must be an element 𝑒 = (0g‘𝐺) such that 𝑒+g𝑎 = 𝑎+g𝑒 = 𝑎 for any a), and inverse (for each element a in the base set, there must be an element 𝑏 = invg𝑎 in the base set such that 𝑎+g𝑏 = 𝑏+g𝑎 = 𝑒). It can be proven that the identity element is unique (grpideu 18974). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 19815). Subgroups can often be formed from groups, see df-subg 19153. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 19900; an Abelian group is a group as proven in ablgrp 19817. Other structures include groups, including unital rings (df-ring 20252) and fields (df-field 20748). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)} | ||
Definition | df-minusg 18967* | Define inverse of group element. (Contributed by NM, 24-Aug-2011.) |
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))) | ||
Definition | df-sbg 18968* | Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.) |
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))) | ||
Theorem | isgrp 18969* | The predicate "is a group". (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ 𝐵 ∃𝑚 ∈ 𝐵 (𝑚 + 𝑎) = 0 )) | ||
Theorem | grpmnd 18970 | A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | ||
Theorem | grpcl 18971 | Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | grpass 18972 | A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | grpinvex 18973* | Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 ) | ||
Theorem | grpideu 18974* | The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)) | ||
Theorem | grpassd 18975 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | grpmndd 18976 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
Theorem | grpcld 18977 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | grpplusf 18978 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | grpplusfo 18979 | The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)–onto→𝐵) | ||
Theorem | resgrpplusfrn 18980 | The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 𝐹 = (+𝑓‘𝐻) ⇒ ⊢ ((𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 = ran 𝐹) | ||
Theorem | grppropd 18981* | If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)) | ||
Theorem | grpprop 18982 | If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.) |
⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) ⇒ ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp) | ||
Theorem | grppropstr 18983 | Generalize a specific 2-element group 𝐿 to show that any set 𝐾 with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ (Base‘𝐾) = 𝐵 & ⊢ (+g‘𝐾) = + & ⊢ 𝐿 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp) | ||
Theorem | grpss 18984 | Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows to prove that a constructed potential ring 𝑅 is a group before we know that it is also a ring. (Theorem ringgrp 20255, on the other hand, requires that we know in advance that 𝑅 is a ring.) (Contributed by NM, 11-Oct-2013.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} & ⊢ 𝑅 ∈ V & ⊢ 𝐺 ⊆ 𝑅 & ⊢ Fun 𝑅 ⇒ ⊢ (𝐺 ∈ Grp ↔ 𝑅 ∈ Grp) | ||
Theorem | isgrpd2e 18985* | Deduce a group from its properties. In this version of isgrpd2 18986, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 = (0g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpd2 18986* | Deduce a group from its properties. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). Note: normally we don't use a 𝜑 antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2734, but we make an exception for theorems such as isgrpd2 18986, ismndd 18781, and islmodd 20880 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 = (0g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpde 18987* | Deduce a group from its properties. In this version of isgrpd 18988, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpd 18988* | Deduce a group from its properties. Unlike isgrpd2 18986, this one goes straight from the base properties rather than going through Mnd. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpi 18989* | Properties that determine a group. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 3-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ 0 ∈ 𝐵 & ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ 𝐺 ∈ Grp | ||
Theorem | grpsgrp 18990 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Smgrp) | ||
Theorem | grpmgmd 18991 | A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.) |
⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mgm) | ||
Theorem | dfgrp2 18992* | Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 18966, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛))) | ||
Theorem | dfgrp2e 18993* | Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛))) | ||
Theorem | isgrpix 18994* | Properties that determine a group. Read 𝑁 as 𝑁(𝑥). Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ + ∈ V & ⊢ 𝐺 = {〈1, 𝐵〉, 〈2, + 〉} & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ 0 ∈ 𝐵 & ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥) & ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵) & ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ 𝐺 ∈ Grp | ||
Theorem | grpidcl 18995 | The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) | ||
Theorem | grpbn0 18996 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) | ||
Theorem | grplid 18997 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | grprid 18998 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | grplidd 18999 | The identity element of a group is a left identity. Deduction associated with grplid 18997. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 0 + 𝑋) = 𝑋) | ||
Theorem | grpridd 19000 | The identity element of a group is a right identity. Deduction associated with grprid 18998. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 0 ) = 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |