![]() |
Metamath
Proof Explorer Theorem List (p. 189 of 481) | < 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-30603) |
![]() (30604-32126) |
![]() (32127-48013) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | efmndfv 18801 | The function value of an endofunction. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | efmndtset 18802 | 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 18803* | The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) | ||
Theorem | efmndov 18804 | The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | efmndcl 18805 | The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | efmndtopn 18806 | The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
Theorem | symggrplem 18807* | Lemma for symggrp 19316 and efmndsgrp 18809. Conditions for an operation to be associative. Formerly part of proof for symggrp 19316. (Contributed by AV, 28-Jan-2024.) |
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦)) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | efmndmgm 18808 | The monoid of endofunctions on a class 𝐴 is a magma. (Contributed by AV, 28-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 ∈ Mgm | ||
Theorem | efmndsgrp 18809 | The monoid of endofunctions on a class 𝐴 is a semigroup. (Contributed by AV, 28-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 ∈ Smgrp | ||
Theorem | ielefmnd 18810 | 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 18811 | 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 18812 | The monoid of endofunctions on a set 𝐴 is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd) | ||
Theorem | efmnd0nmnd 18813 | Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
⊢ (EndoFMnd‘∅) ∈ Mnd | ||
Theorem | efmndbas0 18814 | 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 18815 | The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1) | ||
Theorem | efmnd1bas 18816 | The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{〈𝐼, 𝐼〉}}) | ||
Theorem | efmnd2hash 18817 | The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 4) | ||
Theorem | submefmnd 18818* | 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 19325. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐹 = (Base‘𝑆) ⇒ ⊢ (𝐴 ∈ 𝑉 → (((𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹) ∧ (+g‘𝑆) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubMnd‘𝑀))) | ||
Theorem | sursubmefmnd 18819* | 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 18820* | 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 18821 | 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 18822 | 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 18823 | The modulo function 𝐼 is an endofunction on ℕ0. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) ⇒ ⊢ 𝐼 ∈ (Base‘𝑀) | ||
Theorem | smndex1iidm 18824* | The modulo function 𝐼 is idempotent. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) ⇒ ⊢ (𝐼 ∘ 𝐼) = 𝐼 | ||
Theorem | smndex1gbas 18825* | The constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) ⇒ ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀)) | ||
Theorem | smndex1gid 18826* | 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 18827* | 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 18828* | 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 18829* | 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 18830* | 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 18831* | 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 18832* | Lemma for smndex1mnd 18833 and smndex1id 18834. (Contributed by AV, 16-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ (𝑋 ∈ 𝐵 → ((𝐼 ∘ 𝑋) = 𝑋 ∧ (𝑋 ∘ 𝐼) = 𝑋)) | ||
Theorem | smndex1mnd 18833* | 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 18834* | 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 18835* | 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 18836* | 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 18837 | The doubling function 𝐷 is an endofunction on ℕ0. (Contributed by AV, 18-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥)) ⇒ ⊢ 𝐷 ∈ 𝐵 | ||
Theorem | smndex2dnrinv 18838 | 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 18839 | 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 18840* | 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 18841* | Lemma 1 for mgm2nsgrp 18845: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 18586). (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
Theorem | mgm2nsgrplem2 18842* | Lemma 2 for mgm2nsgrp 18845. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴) | ||
Theorem | mgm2nsgrplem3 18843* | Lemma 3 for mgm2nsgrp 18845. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⚬ (𝐴 ⚬ 𝐵)) = 𝐵) | ||
Theorem | mgm2nsgrplem4 18844* | Lemma 4 for mgm2nsgrp 18845: 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 18845* | 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 18846* | Lemma 1 for sgrp2nmnd 18853: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 18586). (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
Theorem | sgrp2nmndlem2 18847* | Lemma 2 for sgrp2nmnd 18853. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ⚬ 𝐶) = 𝐴) | ||
Theorem | sgrp2nmndlem3 18848* | Lemma 3 for sgrp2nmnd 18853. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐶) = 𝐵) | ||
Theorem | sgrp2rid2 18849* | 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 18850* | 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 18851* | Lemma 4 for sgrp2nmnd 18853: M is a semigroup. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∈ Smgrp) | ||
Theorem | sgrp2nmndlem5 18852* | Lemma 5 for sgrp2nmnd 18853: M is not a monoid. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Mnd) | ||
Theorem | sgrp2nmnd 18853* | 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 18854 | There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.) |
⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ Smgrp | ||
Theorem | sgrpnmndex 18855 | There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.) |
⊢ ∃𝑚 ∈ Smgrp 𝑚 ∉ Mnd | ||
Theorem | sgrpssmgm 18856 | 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 18857 | 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 18858* | 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 18859* | 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 18860* | The power set of a class 𝐴 is a monoid under union. (Contributed by AV, 27-Feb-2024.) |
⊢ (Base‘𝑀) = 𝒫 𝐴 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦)) ⇒ ⊢ 𝑀 ∈ Mnd | ||
Syntax | cgrp 18861 | Extend class notation with class of all groups. |
class Grp | ||
Syntax | cminusg 18862 | Extend class notation with inverse of group element. |
class invg | ||
Syntax | csg 18863 | Extend class notation with group subtraction (or division) operation. |
class -g | ||
Definition | df-grp 18864* | Define class of all groups. A group is a monoid (df-mnd 18666) 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 17152) and an internal group operation (notated (+g‘𝐺) per df-plusg 17217). 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 18869), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 18870), 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 18872). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 19699). Subgroups can often be formed from groups, see df-subg 19046. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 19784; an Abelian group is a group as proven in ablgrp 19701. Other structures include groups, including unital rings (df-ring 20136) and fields (df-field 20586). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)} | ||
Definition | df-minusg 18865* | Define inverse of group element. (Contributed by NM, 24-Aug-2011.) |
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))) | ||
Definition | df-sbg 18866* | Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.) |
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))) | ||
Theorem | isgrp 18867* | 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 18868 | A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | ||
Theorem | grpcl 18869 | Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | grpass 18870 | A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | grpinvex 18871* | 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 18872* | 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 18873 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | grpmndd 18874 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
Theorem | grpcld 18875 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | grpplusf 18876 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | grpplusfo 18877 | 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 18878 | 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 18879* | 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 18880 | 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 18881 | 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 18882 | 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 20139, 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 18883* | Deduce a group from its properties. In this version of isgrpd2 18884, 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 18884* | 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 2731, but we make an exception for theorems such as isgrpd2 18884, ismndd 18687, and islmodd 20708 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 0 = (0g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 ) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | isgrpde 18885* | Deduce a group from its properties. In this version of isgrpd 18886, 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 18886* | Deduce a group from its properties. Unlike isgrpd2 18884, 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 18887* | 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 18888 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Smgrp) | ||
Theorem | grpmgmd 18889 | A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.) |
⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mgm) | ||
Theorem | dfgrp2 18890* | 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 18864, 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 18891* | 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 18892* | 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 18893 | 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 18894 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) | ||
Theorem | grplid 18895 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | grprid 18896 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | grplidd 18897 | The identity element of a group is a left identity. Deduction associated with grplid 18895. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ( 0 + 𝑋) = 𝑋) | ||
Theorem | grpridd 18898 | The identity element of a group is a right identity. Deduction associated with grprid 18896. (Contributed by SN, 29-Jan-2025.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 0 ) = 𝑋) | ||
Theorem | grpn0 18899 | A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.) |
⊢ (𝐺 ∈ Grp → 𝐺 ≠ ∅) | ||
Theorem | hashfingrpnn 18900 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |