![]() |
Metamath
Proof Explorer Theorem List (p. 202 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 | ablfacrp2 20101* | The factors 𝐾, 𝐿 of ablfacrp 20100 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 20102* | Lemma for ablfac1b 20104. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵))) & ⊢ 𝑁 = ((♯‘𝐵) / 𝑀) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁))) | ||
Theorem | ablfac1a 20103* | The factors of ablfac1b 20104 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵)))) | ||
Theorem | ablfac1b 20104* | 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 20105* | The factors of ablfac1b 20104 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) | ||
Theorem | ablfac1eulem 20106* | Lemma for ablfac1eu 20107. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) & ⊢ (𝜑 → dom 𝑇 = 𝐴) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃}))))) | ||
Theorem | ablfac1eu 20107* | The factorization of ablfac1b 20104 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 20108* | Lemma for pgpfac1 20114. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈) | ||
Theorem | pgpfac1lem2 20109* | Lemma for pgpfac1 20114. (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 20110* | Lemma for pgpfac1 20114. (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 20111* | Lemma for pgpfac1 20114. (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 20112* | Lemma for pgpfac1 20114. (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 20113* | Lemma for pgpfac1 20114. (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 20114* | 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 20115* | Lemma for pgpfac 20118. (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 20116* | Lemma for pgpfac 20118. (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 20117* | Lemma for pgpfac 20118. (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 20118* | Full factorization of a finite abelian p-group, by iterating pgpfac1 20114. 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 20119* | Lemma for ablfac 20122. (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 20120* | Lemma for ablfac 20122. (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 20121* | Lemma for ablfac 20122. (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 20122* | 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 20123* | Choose generators for each cyclic group in ablfac 20122. (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 20124 | Extend class notation with the class of simple groups. |
class SimpGrp | ||
Definition | df-simpg 20125 | Define class of all simple groups. A simple group is a group (df-grp 18966) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20137). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} | ||
Theorem | issimpg 20126 | The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o)) | ||
Theorem | issimpgd 20127 | Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
Theorem | simpggrp 20128 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp) | ||
Theorem | simpggrpd 20129 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | simpg2nsg 20130 | A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o) | ||
Theorem | trivnsimpgd 20131 | Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp) | ||
Theorem | simpgntrivd 20132 | Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ¬ 𝐵 = { 0 }) | ||
Theorem | simpgnideld 20133* | A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ) | ||
Theorem | simpgnsgd 20134 | 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 20135 | 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 20136* | 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 20137 | 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 20138 | 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 20139* | 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 20140 | 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 20141* | Lemma for ablsimpgfind 20144. 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 20142* | Lemma for ablsimpgfind 20144. 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 20143* | 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 20144 | An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
Theorem | fincygsubgd 20145* | The subgroup referenced in fincygsubgodd 20146 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺)) | ||
Theorem | fincygsubgodd 20146* | 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 20147* | A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶) | ||
Theorem | prmgrpsimpgd 20148 | A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
Theorem | ablsimpgprmd 20149 | An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ) | ||
Theorem | ablsimpgd 20150 | 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 20151 | Multiplicative group. |
class mulGrp | ||
Definition | df-mgp 20152 | 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 20399 shows that we get a group if we restrict to the elements that have inverses. This allows to formalize such notions as "the multiplication operation of a ring is a monoid" (ringmgp 20256) or "the multiplicative identity" in terms of the identity of a monoid (df-ur 20199). (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), (.r‘𝑤)〉)) | ||
Theorem | fnmgp 20153 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ mulGrp Fn V | ||
Theorem | mgpval 20154 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), · 〉) | ||
Theorem | mgpplusg 20155 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ · = (+g‘𝑀) | ||
Theorem | mgplemOLD 20156 | Obsolete version of setsplusg 19380 as of 18-Oct-2024. Lemma for mgpbas 20157. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 2 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑀) | ||
Theorem | mgpbas 20157 | Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑀) | ||
Theorem | mgpbasOLD 20158 | Obsolete version of mgpbas 20157 as of 18-Oct-2024. Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑀) | ||
Theorem | mgpsca 20159 | The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20340. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ 𝑆 = (Scalar‘𝑀) | ||
Theorem | mgpscaOLD 20160 | Obsolete version of mgpsca 20159 as of 18-Oct-2024. The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20340. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ 𝑆 = (Scalar‘𝑀) | ||
Theorem | mgptset 20161 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (TopSet‘𝑅) = (TopSet‘𝑀) | ||
Theorem | mgptsetOLD 20162 | Obsolete version of mgptset 20161 as of 18-Oct-2024. Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (TopSet‘𝑅) = (TopSet‘𝑀) | ||
Theorem | mgptopn 20163 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑀) | ||
Theorem | mgpds 20164 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (dist‘𝑅) ⇒ ⊢ 𝐵 = (dist‘𝑀) | ||
Theorem | mgpdsOLD 20165 | Obsolete version of mgpds 20164 as of 18-Oct-2024. Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (dist‘𝑅) ⇒ ⊢ 𝐵 = (dist‘𝑀) | ||
Theorem | mgpress 20166 | Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) | ||
Theorem | mgpressOLD 20167 | Obsolete version of mgpress 20166 as of 18-Oct-2024. Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) | ||
Theorem | prdsmgp 20168 | The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) ⇒ ⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧ (+g‘𝑀) = (+g‘𝑍))) | ||
According to Wikipedia, "... in abstract algebra, a rng (or non-unital ring or pseudo-ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 28-Mar-2025). | ||
Syntax | crng 20169 | Extend class notation with class of all non-unital rings. |
class Rng | ||
Definition | df-rng 20170* | Define the class of all non-unital rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.) |
⊢ Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))} | ||
Theorem | isrng 20171* | The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) | ||
Theorem | rngabl 20172 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) | ||
Theorem | rngmgp 20173 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp) | ||
Theorem | rngmgpf 20174 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 20265 analog). (Contributed by AV, 22-Feb-2025.) |
⊢ (mulGrp ↾ Rng):Rng⟶Smgrp | ||
Theorem | rnggrp 20175 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) | ||
Theorem | rngass 20176 | Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍))) | ||
Theorem | rngdi 20177 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
Theorem | rngdir 20178 | Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
Theorem | rngacl 20179 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | rng0cl 20180 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 0 ∈ 𝐵) | ||
Theorem | rngcl 20181 | Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | rnglz 20182 | The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 20306. (Revised by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
Theorem | rngrz 20183 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 20307. (Revised by AV, 16-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) | ||
Theorem | rngmneg1 20184 | Negation of a product in a non-unital ring (mulneg1 11696 analog). In contrast to ringmneg1 20317, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · 𝑌) = (𝑁‘(𝑋 · 𝑌))) | ||
Theorem | rngmneg2 20185 | Negation of a product in a non-unital ring (mulneg2 11697 analog). In contrast to ringmneg2 20318, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑁‘𝑌)) = (𝑁‘(𝑋 · 𝑌))) | ||
Theorem | rngm2neg 20186 | Double negation of a product in a non-unital ring (mul2neg 11699 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 20319. (Revised by AV, 17-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌)) | ||
Theorem | rngansg 20187 | Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.) |
⊢ (𝑅 ∈ Rng → (NrmSGrp‘𝑅) = (SubGrp‘𝑅)) | ||
Theorem | rngsubdi 20188 | Ring multiplication distributes over subtraction. (subdi 11693 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 20320. (Revised by AV, 23-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍))) | ||
Theorem | rngsubdir 20189 | Ring multiplication distributes over subtraction. (subdir 11694 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 20321. (Revised by AV, 23-Feb-2025.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍))) | ||
Theorem | isrngd 20190* | Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Abel) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ⇒ ⊢ (𝜑 → 𝑅 ∈ Rng) | ||
Theorem | rngpropd 20191* | If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Rng ↔ 𝐿 ∈ Rng)) | ||
Theorem | prdsmulrngcl 20192 | Closure of the multiplication in a structure product of non-unital rings. (Contributed by Mario Carneiro, 11-Mar-2015.) Generalization of prdsmulrcl 20333. (Revised by AV, 21-Feb-2025.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Rng) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) | ||
Theorem | prdsrngd 20193 | A product of non-unital rings is a non-unital ring. (Contributed by AV, 22-Feb-2025.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Rng) ⇒ ⊢ (𝜑 → 𝑌 ∈ Rng) | ||
Theorem | imasrng 20194* | The image structure of a non-unital ring is a non-unital ring (imasring 20343 analog). (Contributed by AV, 22-Feb-2025.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ Rng) ⇒ ⊢ (𝜑 → 𝑈 ∈ Rng) | ||
Theorem | imasrngf1 20195 | The image of a non-unital ring under an injection is a non-unital ring (imasmndf1 18801 analog). (Contributed by AV, 22-Feb-2025.) |
⊢ 𝑈 = (𝐹 “s 𝑅) & ⊢ 𝑉 = (Base‘𝑅) ⇒ ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Rng) → 𝑈 ∈ Rng) | ||
Theorem | xpsrngd 20196 | A product of two non-unital rings is a non-unital ring (xpsmnd 18802 analog). (Contributed by AV, 22-Feb-2025.) |
⊢ 𝑌 = (𝑆 ×s 𝑅) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ (𝜑 → 𝑅 ∈ Rng) ⇒ ⊢ (𝜑 → 𝑌 ∈ Rng) | ||
Theorem | qusrng 20197* | The quotient structure of a non-unital ring is a non-unital ring (qusring2 20347 analog). (Contributed by AV, 23-Feb-2025.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ (𝜑 → 𝑅 ∈ Rng) ⇒ ⊢ (𝜑 → 𝑈 ∈ Rng) | ||
In Wikipedia "Identity element", see https://en.wikipedia.org/wiki/Identity_element (18-Jan-2025): "... an identity with respect to multiplication is called a multiplicative identity (often denoted as 1). ... The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity). This should not be confused with a unit in ring theory, which is any element having a multiplicative inverse. By its own definition, unity itself is necessarily a unit." Calling the multiplicative identity of a ring a unity is taken from the definition of a ring with unity in section 17.3 of [BeauregardFraleigh] p. 135, "A ring ( R , + , . ) is a ring with unity if R is not the zero ring and ( R , . ) is a monoid. In this case, the identity element of ( R , . ) is denoted by 1 and is called the unity of R." This definition of a "ring with unity" corresponds to our definition of a unital ring (see df-ring 20252). Some authors call the multiplicative identity "unit" or "unit element" (for example in section I, 2.2 of [BourbakiAlg1] p. 14, definition in section 1.3 of [Hall] p. 4, or in section I, 1 of [Lang] p. 3), whereas other authors use the term "unit" for an element having a multiplicative inverse (for example in section 17.3 of [BeauregardFraleigh] p. 135, in definition in [Roman] p. 26, or even in section II, 1 of [Lang] p. 84). Sometimes, the multiplicative identity is simply called "one" (see, for example, chapter 8 in [Schechter] p. 180). To avoid this ambiguity of the term "unit", also mentioned in Wikipedia, we call the multiplicative identity of a structure with a multiplication (usually a ring) a "ring unity", or straightly "multiplicative identity". The term "unit" will be used for an element having a multiplicative inverse (see df-unit 20374), and we have "the ring unity is a unit", see 1unit 20390. | ||
Syntax | cur 20198 | Extend class notation with ring unity. |
class 1r | ||
Definition | df-ur 20199 |
Define the multiplicative identity, i.e., the monoid identity (df-0g 17487)
of the multiplicative monoid (df-mgp 20152) of a ring-like structure. This
multiplicative identity is also called "ring unity" or
"unity element".
This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot. See also dfur2 20201, 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 20200 | 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‘𝐺) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |