![]() |
Metamath
Proof Explorer Theorem List (p. 178 of 435) | < 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-28326) |
![]() (28327-29851) |
![]() (29852-43457) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mhmpropd 17701* | Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 7-Nov-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 MndHom 𝐾) = (𝐿 MndHom 𝑀)) | ||
Theorem | mhmlin 17702 | A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) | ||
Theorem | mhm0 17703 | A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑆) & ⊢ 𝑌 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌) | ||
Theorem | idmhm 17704 | The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀)) | ||
Theorem | mhmf1o 17705 | A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 MndHom 𝑅))) | ||
Theorem | submrcl 17706 | Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd) | ||
Theorem | issubm 17707* | Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) | ||
Theorem | issubm2 17708 | Submonoids are subsets that are also monoids with the same zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ 𝐻 ∈ Mnd))) | ||
Theorem | issubmd 17709* | Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂) & ⊢ (𝑧 = 0 → (𝜓 ↔ 𝜒)) & ⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃)) & ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂)) ⇒ ⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMnd‘𝑀)) | ||
Theorem | submss 17710 | Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵) | ||
Theorem | submid 17711 | Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀)) | ||
Theorem | subm0cl 17712 | Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆) | ||
Theorem | submcl 17713 | Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
Theorem | submmnd 17714 | Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd) | ||
Theorem | submbas 17715 | The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻)) | ||
Theorem | subm0 17716 | Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻)) | ||
Theorem | subsubm 17717 | A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
Theorem | 0mhm 17718 | The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 0 = (0g‘𝑁) & ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → (𝐵 × { 0 }) ∈ (𝑀 MndHom 𝑁)) | ||
Theorem | resmhm 17719 | Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇)) | ||
Theorem | resmhm2 17720 | One direction of resmhm2b 17721. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | resmhm2b 17721 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈))) | ||
Theorem | mhmco 17722 | The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈)) | ||
Theorem | mhmima 17723 | The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁)) | ||
Theorem | mhmeql 17724 | The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆)) | ||
Theorem | submacs 17725 | Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | mrcmndind 17726* | (( From SO's determinants branch )). TODO: Appropriate description to be added! (Contributed by SO, 14-Jul-2018.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 𝑧) → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 0 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐺 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 = ((mrCls‘(SubMnd‘𝑀))‘𝐺)) & ⊢ (𝜑 → 𝜏) & ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺) ∧ 𝜒) → 𝜃) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | prdspjmhm 17727* | A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴))) | ||
Theorem | pwspjmhm 17728* | A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom 𝑅)) | ||
Theorem | pwsdiagmhm 17729* | Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) | ||
Theorem | pwsco1mhm 17730* | Right composition with a function on the index sets yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐴) & ⊢ 𝑍 = (𝑅 ↑s 𝐵) & ⊢ 𝐶 = (Base‘𝑍) & ⊢ (𝜑 → 𝑅 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌)) | ||
Theorem | pwsco2mhm 17731* | Left composition with a monoid homomorphism yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐴) & ⊢ 𝑍 = (𝑆 ↑s 𝐴) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆)) ⇒ ⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍)) | ||
One important use of words is as formal composites in cases where order is significant, using the general sum operator df-gsum 16463. If order is not significant, it is simpler to use families instead. | ||
Theorem | gsumvallem2 17732* | Lemma for properties of the set of identities of 𝐺. The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ⇒ ⊢ (𝐺 ∈ Mnd → 𝑂 = { 0 }) | ||
Theorem | gsumsubm 17733 | Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumz 17734* | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) | ||
Theorem | gsumwsubmcl 17735 | Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) |
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) → (𝐺 Σg 𝑊) ∈ 𝑆) | ||
Theorem | gsumws1 17736 | A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg 〈“𝑆”〉) = 𝑆) | ||
Theorem | gsumwcl 17737 | Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) | ||
Theorem | gsumccat 17738 | Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) | ||
Theorem | gsumws2 17739 | Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵) → (𝐺 Σg 〈“𝑆𝑇”〉) = (𝑆 + 𝑇)) | ||
Theorem | gsumccatsn 17740 | Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) + 𝑍)) | ||
Theorem | gsumspl 17741 | The primary purpose of the splice construction is to enable local rewrites. Thus, in any monoidal valuation, if a splice does not cause a local change it does not cause a global change. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) & ⊢ (𝜑 → 𝑋 ∈ Word 𝐵) & ⊢ (𝜑 → 𝑌 ∈ Word 𝐵) & ⊢ (𝜑 → (𝑀 Σg 𝑋) = (𝑀 Σg 𝑌)) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑆 splice 〈𝐹, 𝑇, 𝑋〉)) = (𝑀 Σg (𝑆 splice 〈𝐹, 𝑇, 𝑌〉))) | ||
Theorem | gsumsplOLD 17742 | Obsolete proof of gsumspl 17741 as of 12-Oct-2022. (Contributed by Stefan O'Rear, 23-Aug-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐵) & ⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) & ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) & ⊢ (𝜑 → 𝑋 ∈ Word 𝐵) & ⊢ (𝜑 → 𝑌 ∈ Word 𝐵) & ⊢ (𝜑 → (𝑀 Σg 𝑋) = (𝑀 Σg 𝑌)) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑆 spliceOLD 〈𝐹, 𝑇, 𝑋〉)) = (𝑀 Σg (𝑆 spliceOLD 〈𝐹, 𝑇, 𝑌〉))) | ||
Theorem | gsumwmhm 17743 | Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) | ||
Theorem | gsumwspan 17744* | The submonoid generated by a set of elements is precisely the set of elements which can be expressed as finite products of the generator. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (mrCls‘(SubMnd‘𝑀)) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) | ||
Syntax | cfrmd 17745 | Extend class definition with the free monoid construction. |
class freeMnd | ||
Syntax | cvrmd 17746 | Extend class notation with free monoid injection. |
class varFMnd | ||
Definition | df-frmd 17747 | Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ freeMnd = (𝑖 ∈ V ↦ {〈(Base‘ndx), Word 𝑖〉, 〈(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))〉}) | ||
Definition | df-vrmd 17748* | Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ varFMnd = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ 〈“𝑗”〉)) | ||
Theorem | frmdval 17749 | Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼) & ⊢ + = ( ++ ↾ (𝐵 × 𝐵)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉}) | ||
Theorem | frmdbas 17750 | The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼) | ||
Theorem | frmdelbas 17751 | An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝐼) | ||
Theorem | frmdplusg 17752 | The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ + = ( ++ ↾ (𝐵 × 𝐵)) | ||
Theorem | frmdadd 17753 | Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌)) | ||
Theorem | vrmdfval 17754* | The canonical injection from the generating set 𝐼 to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑈 = (𝑗 ∈ 𝐼 ↦ 〈“𝑗”〉)) | ||
Theorem | vrmdval 17755 | The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = 〈“𝐴”〉) | ||
Theorem | vrmdf 17756 | The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶Word 𝐼) | ||
Theorem | frmdmnd 17757 | A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) | ||
Theorem | frmd0 17758 | The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ ∅ = (0g‘𝑀) | ||
Theorem | frmdsssubm 17759 | The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼) → Word 𝐽 ∈ (SubMnd‘𝑀)) | ||
Theorem | frmdgsum 17760 | Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊) | ||
Theorem | frmdss2 17761 | A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of 𝐽 is Word 𝐽". (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ (SubMnd‘𝑀)) → ((𝑈 “ 𝐽) ⊆ 𝐴 ↔ Word 𝐽 ⊆ 𝐴)) | ||
Theorem | frmdup1 17762* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ (𝜑 → 𝐴:𝐼⟶𝐵) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝑀 MndHom 𝐺)) | ||
Theorem | frmdup2 17763* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐼 ∈ 𝑋) & ⊢ (𝜑 → 𝐴:𝐼⟶𝐵) & ⊢ 𝑈 = (varFMnd‘𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐸‘(𝑈‘𝑌)) = (𝐴‘𝑌)) | ||
Theorem | frmdup3lem 17764* | Lemma for frmdup3 17765. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))) | ||
Theorem | frmdup3 17765* | Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝑀 MndHom 𝐺)(𝑚 ∘ 𝑈) = 𝐴) | ||
Theorem | mgm2nsgrplem1 17766* | Lemma 1 for mgm2nsgrp 17770: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 17614). (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
Theorem | mgm2nsgrplem2 17767* | Lemma 2 for mgm2nsgrp 17770. (Contributed by AV, 27-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴) | ||
Theorem | mgm2nsgrplem3 17768* | Lemma 3 for mgm2nsgrp 17770. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⚬ (𝐴 ⚬ 𝐵)) = 𝐵) | ||
Theorem | mgm2nsgrplem4 17769* | Lemma 4 for mgm2nsgrp 17770: M is not a semigroup. (Contributed by AV, 28-Jan-2020.) (Proof shortened by AV, 31-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ SGrp) | ||
Theorem | mgm2nsgrp 17770* | A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ Mgm ∧ 𝑀 ∉ SGrp)) | ||
Theorem | sgrp2nmndlem1 17771* | Lemma 1 for sgrp2nmnd 17778: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 17614). (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
Theorem | sgrp2nmndlem2 17772* | Lemma 2 for sgrp2nmnd 17778. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ⚬ 𝐶) = 𝐴) | ||
Theorem | sgrp2nmndlem3 17773* | Lemma 3 for sgrp2nmnd 17778. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐶) = 𝐵) | ||
Theorem | sgrp2rid2 17774* | 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 17775* | 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 17776* | Lemma 4 for sgrp2nmnd 17778: M is a semigroup. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∈ SGrp) | ||
Theorem | sgrp2nmndlem5 17777* | Lemma 5 for sgrp2nmnd 17778: M is not a monoid. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Mnd) | ||
Theorem | sgrp2nmnd 17778* | A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.) |
⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ SGrp ∧ 𝑀 ∉ Mnd)) | ||
Theorem | mgmnsgrpex 17779 | There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.) |
⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ SGrp | ||
Theorem | sgrpnmndex 17780 | There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.) |
⊢ ∃𝑚 ∈ SGrp 𝑚 ∉ Mnd | ||
Theorem | sgrpssmgm 17781 | The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.) |
⊢ SGrp ⊊ Mgm | ||
Theorem | mndsssgrp 17782 | The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.) |
⊢ Mnd ⊊ SGrp | ||
Syntax | cgrp 17783 | Extend class notation with class of all groups. |
class Grp | ||
Syntax | cminusg 17784 | Extend class notation with inverse of group element. |
class invg | ||
Syntax | csg 17785 | Extend class notation with group subtraction (or division) operation. |
class -g | ||
Definition | df-grp 17786* | Define class of all groups. A group is a monoid (df-mnd 17655) 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 16235) and an internal group operation (notated (+g‘𝐺) per df-plusg 16325). 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 17791), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 17792), 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 17794). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 18556). Subgroups can often be formed from groups, see df-subg 17949. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 18631; an Abelian group is a group as proven in ablgrp 18558. Other structures include groups, including unital rings (df-ring 18910) and fields (df-field 19113). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)} | ||
Definition | df-minusg 17787* | Define inverse of group element. (Contributed by NM, 24-Aug-2011.) |
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔)))) | ||
Definition | df-sbg 17788* | Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.) |
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦)))) | ||
Theorem | isgrp 17789* | 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 17790 | A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | ||
Theorem | grpcl 17791 | Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | grpass 17792 | A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | grpinvex 17793* | 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 17794* | 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 | grpplusf 17795 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | grpplusfo 17796 | 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 17797 | 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 17798* | 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 17799 | 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 17800 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |