Home | Metamath
Proof Explorer Theorem List (p. 192 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dprdsplit 19101 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) | ||
Theorem | dmdprdpr 19102 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) | ||
Theorem | dprdpr 19103 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) ⇒ ⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉}) = (𝑆 ⊕ 𝑇)) | ||
Theorem | dpjlem 19104 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋)) | ||
Theorem | dpjcntz 19105 | The two subgroups that appear in dpjval 19109 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjdisj 19106 | The two subgroups that appear in dpjval 19109 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 }) | ||
Theorem | dpjlsm 19107 | The two subgroups that appear in dpjval 19109 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjfval 19108* | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ 𝑄 = (proj1‘𝐺) ⇒ ⊢ (𝜑 → 𝑃 = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) | ||
Theorem | dpjval 19109 | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ 𝑄 = (proj1‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) = ((𝑆‘𝑋)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjf 19110 | The 𝑋-th index projection is a function from the direct product to the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋):(𝐺 DProd 𝑆)⟶(𝑆‘𝑋)) | ||
Theorem | dpjidcl 19111* | The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆)) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴)) ∈ 𝑊 ∧ 𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴))))) | ||
Theorem | dpjeq 19112* | Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆)) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐶) ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ 𝐶)) ↔ ∀𝑥 ∈ 𝐼 ((𝑃‘𝑥)‘𝐴) = 𝐶)) | ||
Theorem | dpjid 19113* | The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴)))) | ||
Theorem | dpjlid 19114 | The 𝑋-th index projection acts as the identity on elements of the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋)) ⇒ ⊢ (𝜑 → ((𝑃‘𝑋)‘𝐴) = 𝐴) | ||
Theorem | dpjrid 19115 | The 𝑌-th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ≠ 𝑋) ⇒ ⊢ (𝜑 → ((𝑃‘𝑌)‘𝐴) = 0 ) | ||
Theorem | dpjghm 19116 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ ((𝐺 ↾s (𝐺 DProd 𝑆)) GrpHom 𝐺)) | ||
Theorem | dpjghm2 19117 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ ((𝐺 ↾s (𝐺 DProd 𝑆)) GrpHom (𝐺 ↾s (𝑆‘𝑋)))) | ||
Theorem | ablfacrplem 19118* | Lemma for ablfacrp2 19120. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) ⇒ ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) | ||
Theorem | ablfacrp 19119* | A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups 𝐾, 𝐿 that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵)) | ||
Theorem | ablfacrp2 19120* | The factors 𝐾, 𝐿 of ablfacrp 19119 have the expected orders (which allows for repeated application to decompose 𝐺 into subgroups of prime-power order). Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) ⇒ ⊢ (𝜑 → ((♯‘𝐾) = 𝑀 ∧ (♯‘𝐿) = 𝑁)) | ||
Theorem | ablfac1lem 19121* | Lemma for ablfac1b 19123. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵))) & ⊢ 𝑁 = ((♯‘𝐵) / 𝑀) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁))) | ||
Theorem | ablfac1a 19122* | The factors of ablfac1b 19123 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵)))) | ||
Theorem | ablfac1b 19123* | Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) ⇒ ⊢ (𝜑 → 𝐺dom DProd 𝑆) | ||
Theorem | ablfac1c 19124* | The factors of ablfac1b 19123 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) | ||
Theorem | ablfac1eulem 19125* | Lemma for ablfac1eu 19126. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) & ⊢ (𝜑 → dom 𝑇 = 𝐴) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃}))))) | ||
Theorem | ablfac1eu 19126* | The factorization of ablfac1b 19123 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to 𝑆. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) & ⊢ (𝜑 → dom 𝑇 = 𝐴) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) ⇒ ⊢ (𝜑 → 𝑇 = 𝑆) | ||
Theorem | pgpfac1lem1 19127* | Lemma for pgpfac1 19133. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈) | ||
Theorem | pgpfac1lem2 19128* | Lemma for pgpfac1 19133. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝜑 → (𝑃 · 𝐶) ∈ (𝑆 ⊕ 𝑊)) | ||
Theorem | pgpfac1lem3a 19129* | Lemma for pgpfac1 19133. (Contributed by Mario Carneiro, 4-Jun-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ((𝑃 · 𝐶)(+g‘𝐺)(𝑀 · 𝐴)) ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀)) | ||
Theorem | pgpfac1lem3 19130* | Lemma for pgpfac1 19133. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ((𝑃 · 𝐶)(+g‘𝐺)(𝑀 · 𝐴)) ∈ 𝑊) & ⊢ 𝐷 = (𝐶(+g‘𝐺)((𝑀 / 𝑃) · 𝐴)) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | ||
Theorem | pgpfac1lem4 19131* | Lemma for pgpfac1 19133. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | ||
Theorem | pgpfac1lem5 19132* | Lemma for pgpfac1 19133. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑠))) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | ||
Theorem | pgpfac1 19133* | Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝐵)) | ||
Theorem | pgpfaclem1 19134* | Lemma for pgpfac 19137. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) & ⊢ 𝐻 = (𝐺 ↾s 𝑈) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻)) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝐸 = (gEx‘𝐻) & ⊢ 0 = (0g‘𝐻) & ⊢ ⊕ = (LSSum‘𝐻) & ⊢ (𝜑 → 𝐸 ≠ 1) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐶) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) & ⊢ 𝑇 = (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
Theorem | pgpfaclem2 19135* | Lemma for pgpfac 19137. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) & ⊢ 𝐻 = (𝐺 ↾s 𝑈) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻)) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝐸 = (gEx‘𝐻) & ⊢ 0 = (0g‘𝐻) & ⊢ ⊕ = (LSSum‘𝐻) & ⊢ (𝜑 → 𝐸 ≠ 1) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
Theorem | pgpfaclem3 19136* | Lemma for pgpfac 19137. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
Theorem | pgpfac 19137* | Full factorization of a finite abelian p-group, by iterating pgpfac1 19133. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) | ||
Theorem | ablfaclem1 19138* | Lemma for ablfac 19141. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊‘𝑈) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)}) | ||
Theorem | ablfaclem2 19139* | Lemma for ablfac 19141. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) & ⊢ (𝜑 → 𝐹:𝐴⟶Word 𝐶) & ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) & ⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦)) & ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐿))–1-1-onto→𝐿) ⇒ ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) | ||
Theorem | ablfaclem3 19140* | Lemma for ablfac 19141. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) ⇒ ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) | ||
Theorem | ablfac 19141* | The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) | ||
Theorem | ablfac2 19142* | Choose generators for each cyclic group in ablfac 19141. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤‘𝑘)))) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤⟶𝐶 ∧ 𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)) | ||
Syntax | csimpg 19143 | Extend class notation with the class of simple groups. |
class SimpGrp | ||
Definition | df-simpg 19144 | Define class of all simple groups. A simple group is a group (df-grp 18046) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 19156). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} | ||
Theorem | issimpg 19145 | The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o)) | ||
Theorem | issimpgd 19146 | Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
Theorem | simpggrp 19147 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp) | ||
Theorem | simpggrpd 19148 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | simpg2nsg 19149 | A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o) | ||
Theorem | trivnsimpgd 19150 | Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp) | ||
Theorem | simpgntrivd 19151 | Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ¬ 𝐵 = { 0 }) | ||
Theorem | simpgnideld 19152* | A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ) | ||
Theorem | simpgnsgd 19153 | The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) = {{ 0 }, 𝐵}) | ||
Theorem | simpgnsgeqd 19154 | A normal subgroup of a simple group is either the whole group or the trivial subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) & ⊢ (𝜑 → 𝐴 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐴 = { 0 } ∨ 𝐴 = 𝐵)) | ||
Theorem | 2nsgsimpgd 19155* | If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → ¬ { 0 } = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (NrmSGrp‘𝐺)) → (𝑥 = { 0 } ∨ 𝑥 = 𝐵)) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
Theorem | simpgnsgbid 19156 | A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → ¬ { 0 } = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (NrmSGrp‘𝐺) = {{ 0 }, 𝐵})) | ||
Theorem | ablsimpnosubgd 19157 | A subgroup of an abelian simple group containing a nonidentity element is the whole group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → ¬ 𝐴 = 0 ) ⇒ ⊢ (𝜑 → 𝑆 = 𝐵) | ||
Theorem | ablsimpg1gend 19158* | An abelian simple group is generated by any non-identity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 = 0 ) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℤ 𝐶 = (𝑛 · 𝐴)) | ||
Theorem | ablsimpgcygd 19159 | An abelian simple group is cyclic. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.) |
⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐺 ∈ CycGrp) | ||
Theorem | ablsimpgfindlem1 19160* | Lemma for ablsimpgfind 19163. An element of an abelian finite simple group which doesn't square to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2 · 𝑥) ≠ 0 ) → (𝑂‘𝑥) ≠ 0) | ||
Theorem | ablsimpgfindlem2 19161* | Lemma for ablsimpgfind 19163. An element of an abelian finite simple group which squares to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2 · 𝑥) = 0 ) → (𝑂‘𝑥) ≠ 0) | ||
Theorem | cycsubggenodd 19162* | Relationship between the order of a subgroup and the order of a generator of the subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) = if(𝐶 ∈ Fin, (♯‘𝐶), 0)) | ||
Theorem | ablsimpgfind 19163 | An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | fincygsubgd 19164* | The subgroup referenced in fincygsubgodd 19165 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺)) | ||
Theorem | fincygsubgodd 19165* | Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐷 = ((♯‘𝐵) / 𝐶) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) & ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ran 𝐹 = 𝐵) & ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → (♯‘ran 𝐻) = 𝐷) | ||
Theorem | fincygsubgodexd 19166* | A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶) | ||
Theorem | prmgrpsimpgd 19167 | A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
Theorem | ablsimpgprmd 19168 | An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ) | ||
Theorem | ablsimpgd 19169 | An abelian group is simple if and only if its order is prime. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (♯‘𝐵) ∈ ℙ)) | ||
Syntax | cmgp 19170 | Multiplicative group. |
class mulGrp | ||
Definition | df-mgp 19171 | Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp 19348 shows that we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" (ringmgp 19234) or "the multiplicative identity" in terms of the identity of a monoid (df-1r 10472). (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), (.r‘𝑤)〉)) | ||
Theorem | fnmgp 19172 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ mulGrp Fn V | ||
Theorem | mgpval 19173 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), · 〉) | ||
Theorem | mgpplusg 19174 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ · = (+g‘𝑀) | ||
Theorem | mgplem 19175 | Lemma for mgpbas 19176. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 2 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑀) | ||
Theorem | mgpbas 19176 | Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑀) | ||
Theorem | mgpsca 19177 | The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 19299. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ 𝑆 = (Scalar‘𝑀) | ||
Theorem | mgptset 19178 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (TopSet‘𝑅) = (TopSet‘𝑀) | ||
Theorem | mgptopn 19179 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑀) | ||
Theorem | mgpds 19180 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (dist‘𝑅) ⇒ ⊢ 𝐵 = (dist‘𝑀) | ||
Theorem | mgpress 19181 | Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) | ||
Syntax | cur 19182 | Extend class notation with ring unit. |
class 1r | ||
Definition | df-ur 19183 | Define the multiplicative neutral element of a ring. This definition works by extracting the 0g element, i.e. the neutral element in a group or monoid, and transferring it to the multiplicative monoid via the mulGrp function (df-mgp 19171). See also dfur2 19185, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 1r = (0g ∘ mulGrp) | ||
Theorem | ringidval 19184 | The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (0g‘𝐺) | ||
Theorem | dfur2 19185* | The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑒) = 𝑥))) | ||
Syntax | csrg 19186 | Extend class notation with the class of all semirings. |
class SRing | ||
Definition | df-srg 19187* | Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Compared to the definition of a ring, this definition also adds that the additive identity is an absorbing element of the multiplicative law, as this cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))} | ||
Theorem | issrg 19188* | The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 )))) | ||
Theorem | srgcmn 19189 | A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) | ||
Theorem | srgmnd 19190 | A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) | ||
Theorem | srgmgp 19191 | A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) | ||
Theorem | srgi 19192 | Properties of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) | ||
Theorem | srgcl 19193 | Closure of the multiplication operation of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | srgass 19194 | Associative law for the multiplication operation of a semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍))) | ||
Theorem | srgideu 19195* | The unit element of a semiring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑢) = 𝑥)) | ||
Theorem | srgfcl 19196 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by AV, 24-Aug-2021.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ · Fn (𝐵 × 𝐵)) → · :(𝐵 × 𝐵)⟶𝐵) | ||
Theorem | srgdi 19197 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
Theorem | srgdir 19198 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
Theorem | srgidcl 19199 | The unit element of a semiring belongs to the base set of the semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 1 ∈ 𝐵) | ||
Theorem | srg0cl 19200 | The zero element of a semiring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 0 ∈ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |