![]() |
Metamath
Proof Explorer Theorem List (p. 184 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nsgbi 18301 | Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆)) | ||
Theorem | nsgsubg 18302 | A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺)) | ||
Theorem | nsgconj 18303 | The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐵) − 𝐴) ∈ 𝑆) | ||
Theorem | isnsg3 18304* | A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑆 ((𝑥 + 𝑦) − 𝑥) ∈ 𝑆)) | ||
Theorem | subgacs 18305 | Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | nsgacs 18306 | Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (NrmSGrp‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | elnmz 18307* | Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⇒ ⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ((𝐴 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝐴) ∈ 𝑆))) | ||
Theorem | nmzbi 18308* | Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} ⇒ ⊢ ((𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆)) | ||
Theorem | nmzsubg 18309* | The normalizer NG(S) of a subset 𝑆 of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) | ||
Theorem | ssnmz 18310* | A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁) | ||
Theorem | isnsg4 18311* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 = 𝑋)) | ||
Theorem | nmznsg 18312* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑁) ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻)) | ||
Theorem | 0nsg 18313 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → { 0 } ∈ (NrmSGrp‘𝐺)) | ||
Theorem | nsgid 18314 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (NrmSGrp‘𝐺)) | ||
Theorem | 0idnsgd 18315 | The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → {{ 0 }, 𝐵} ⊆ (NrmSGrp‘𝐺)) | ||
Theorem | trivnsgd 18316 | The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) = {𝐵}) | ||
Theorem | triv1nsgd 18317 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o) | ||
Theorem | 1nsgtrivd 18318 | A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o) ⇒ ⊢ (𝜑 → 𝐵 = { 0 }) | ||
Theorem | releqg 18319 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ Rel 𝑅 | ||
Theorem | eqgfval 18320* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) | ||
Theorem | eqgval 18321 | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) | ||
Theorem | eqger 18322 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) ⇒ ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) | ||
Theorem | eqglact 18323* | A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) “ 𝑌)) | ||
Theorem | eqgid 18324 | The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑌 ∈ (SubGrp‘𝐺) → [ 0 ] ∼ = 𝑌) | ||
Theorem | eqgen 18325 | Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) ⇒ ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝐴) | ||
Theorem | eqgcpbl 18326 | The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷))) | ||
Theorem | qusgrp 18327 | If 𝑌 is a normal subgroup of 𝐺, then 𝐻 = 𝐺 / 𝑌 is a group, called the quotient of 𝐺 by 𝑌. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp) | ||
Theorem | quseccl 18328 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → [𝑋](𝐺 ~QG 𝑆) ∈ 𝐵) | ||
Theorem | qusadd 18329 | Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ✚ = (+g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋](𝐺 ~QG 𝑆) ✚ [𝑌](𝐺 ~QG 𝑆)) = [(𝑋 + 𝑌)](𝐺 ~QG 𝑆)) | ||
Theorem | qus0 18330 | Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → [ 0 ](𝐺 ~QG 𝑆) = (0g‘𝐻)) | ||
Theorem | qusinv 18331 | Value of the group inverse operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝑁 = (invg‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → (𝑁‘[𝑋](𝐺 ~QG 𝑆)) = [(𝐼‘𝑋)](𝐺 ~QG 𝑆)) | ||
Theorem | qussub 18332 | Value of the group subtraction operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) & ⊢ 𝑉 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (-g‘𝐻) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋](𝐺 ~QG 𝑆)𝑁[𝑌](𝐺 ~QG 𝑆)) = [(𝑋 − 𝑌)](𝐺 ~QG 𝑆)) | ||
Theorem | lagsubg2 18333 | Lagrange's theorem for finite groups. Call the "order" of a group the cardinal number of the basic set of the group, and "index of a subgroup" the cardinal number of the set of left (or right, this is the same) cosets of this subgroup. Then the order of the group is the (cardinal) product of the order of any of its subgroups by the index of this subgroup. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑌) & ⊢ (𝜑 → 𝑌 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ Fin) ⇒ ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌))) | ||
Theorem | lagsubg 18334 | Lagrange's theorem for Groups: the order of any subgroup of a finite group is a divisor of the order of the group. This is Metamath 100 proof #71. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝑌) ∥ (♯‘𝑋)) | ||
This section contains some preliminary results about cyclic monoids and groups before the class CycGrp of cyclic groups (see df-cyg 18990) is defined in the context of Abelian groups. | ||
Theorem | cycsubmel 18335* | Characterization of an element of the set of nonnegative integer powers of an element 𝐴. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 ⇒ ⊢ (𝑋 ∈ 𝐶 ↔ ∃𝑖 ∈ ℕ0 𝑋 = (𝑖 · 𝐴)) | ||
Theorem | cycsubmcl 18336* | The set of nonnegative integer powers of an element 𝐴 contains 𝐴. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶) | ||
Theorem | cycsubm 18337* | The set of nonnegative integer powers of an element 𝐴 of a monoid forms a submonoid containing 𝐴 (see cycsubmcl 18336), called the cyclic monoid generated by the element 𝐴. This corresponds to the statement in [Lang] p. 6. (Contributed by AV, 28-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ (SubMnd‘𝐺)) | ||
Theorem | cyccom 18338* | Condition for an operation to be commutative. Lemma for cycsubmcom 18339 and cygabl 19003. Formerly part of proof for cygabl 19003. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.) |
⊢ (𝜑 → ∀𝑐 ∈ 𝐶 ∃𝑥 ∈ 𝑍 𝑐 = (𝑥 · 𝐴)) & ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑛 ∈ 𝑍 ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴) + (𝑛 · 𝐴))) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐶) & ⊢ (𝜑 → 𝑍 ⊆ ℂ) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | cycsubmcom 18339* | The operation of a monoid is commutative over the set of nonnegative integer powers of an element 𝐴 of the monoid. (Contributed by AV, 20-Jan-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴)) & ⊢ 𝐶 = ran 𝐹 & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | cycsubggend 18340* | The cyclic subgroup generated by 𝐴 includes its generator. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ ran 𝐹) | ||
Theorem | cycsubgcl 18341* | The set of integer powers of an element 𝐴 of a group forms a subgroup containing 𝐴, called the cyclic group generated by the element 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (ran 𝐹 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ran 𝐹)) | ||
Theorem | cycsubgss 18342* | The cyclic subgroup generated by an element 𝐴 is a subset of any subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑆) → ran 𝐹 ⊆ 𝑆) | ||
Theorem | cycsubg 18343* | The cyclic group generated by 𝐴 is the smallest subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 = ∩ {𝑠 ∈ (SubGrp‘𝐺) ∣ 𝐴 ∈ 𝑠}) | ||
Theorem | cycsubgcld 18344* | The cyclic subgroup generated by 𝐴 is a subgroup. Deduction related to cycsubgcl 18341. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (SubGrp‘𝐺)) | ||
Theorem | cycsubg2 18345* | The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐾‘{𝐴}) = ran 𝐹) | ||
Theorem | cycsubg2cl 18346 | Any multiple of an element is contained in the generated cyclic subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝐴) ∈ (𝐾‘{𝐴})) | ||
Syntax | cghm 18347 | Extend class notation with the generator of group hom-sets. |
class GrpHom | ||
Definition | df-ghm 18348* | A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))}) | ||
Theorem | reldmghm 18349 | Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ Rel dom GrpHom | ||
Theorem | isghm 18350* | Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) | ||
Theorem | isghm3 18351* | Property of a group homomorphism, similar to ismhm 17950. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣))))) | ||
Theorem | ghmgrp1 18352 | A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) | ||
Theorem | ghmgrp2 18353 | A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp) | ||
Theorem | ghmf 18354 | A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌) | ||
Theorem | ghmlin 18355 | A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉))) | ||
Theorem | ghmid 18356 | A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝑌 = (0g‘𝑆) & ⊢ 0 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘𝑌) = 0 ) | ||
Theorem | ghminv 18357 | A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑀 = (invg‘𝑆) & ⊢ 𝑁 = (invg‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) = (𝑁‘(𝐹‘𝑋))) | ||
Theorem | ghmsub 18358 | Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ − = (-g‘𝑆) & ⊢ 𝑁 = (-g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)𝑁(𝐹‘𝑉))) | ||
Theorem | isghmd 18359* | Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ (𝜑 → 𝑆 ∈ Grp) & ⊢ (𝜑 → 𝑇 ∈ Grp) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | ghmmhm 18360 | A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | ghmmhmb 18361 | Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015.) |
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = (𝑆 MndHom 𝑇)) | ||
Theorem | ghmmulg 18362 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ × = (.g‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) | ||
Theorem | ghmrn 18363 | The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇)) | ||
Theorem | 0ghm 18364 | The constant zero linear function between two groups. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 0 = (0g‘𝑁) & ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝑀 ∈ Grp ∧ 𝑁 ∈ Grp) → (𝐵 × { 0 }) ∈ (𝑀 GrpHom 𝑁)) | ||
Theorem | idghm 18365 | The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → ( I ↾ 𝐵) ∈ (𝐺 GrpHom 𝐺)) | ||
Theorem | resghm 18366 | Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 GrpHom 𝑇)) | ||
Theorem | resghm2 18367 | One direction of resghm2b 18368. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑈) ∧ 𝑋 ∈ (SubGrp‘𝑇)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
Theorem | resghm2b 18368 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubGrp‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ (𝑆 GrpHom 𝑈))) | ||
Theorem | ghmghmrn 18369 | A group homomorphism from 𝐺 to 𝐻 is also a group homomorphism from 𝐺 to its image in 𝐻. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by AV, 26-Aug-2021.) |
⊢ 𝑈 = (𝑇 ↾s ran 𝐹) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑈)) | ||
Theorem | ghmco 18370 | The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐹 ∈ (𝑇 GrpHom 𝑈) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpHom 𝑈)) | ||
Theorem | ghmima 18371 | The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑆)) → (𝐹 “ 𝑈) ∈ (SubGrp‘𝑇)) | ||
Theorem | ghmpreima 18372 | The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (SubGrp‘𝑆)) | ||
Theorem | ghmeql 18373 | The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆)) | ||
Theorem | ghmnsgima 18374 | The image of a normal subgroup under a surjective homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 𝑌 = (Base‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (NrmSGrp‘𝑆) ∧ ran 𝐹 = 𝑌) → (𝐹 “ 𝑈) ∈ (NrmSGrp‘𝑇)) | ||
Theorem | ghmnsgpreima 18375 | The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (NrmSGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (NrmSGrp‘𝑆)) | ||
Theorem | ghmker 18376 | The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
⊢ 0 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝑆)) | ||
Theorem | ghmeqker 18377 | Two source points map to the same destination point under a group homomorphism iff their difference belongs to the kernel. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ − = (-g‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈) = (𝐹‘𝑉) ↔ (𝑈 − 𝑉) ∈ 𝐾)) | ||
Theorem | pwsdiagghm 18378* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 GrpHom 𝑌)) | ||
Theorem | ghmf1 18379* | Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑈 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1→𝑌 ↔ ∀𝑥 ∈ 𝑋 ((𝐹‘𝑥) = 𝑈 → 𝑥 = 0 ))) | ||
Theorem | ghmf1o 18380 | A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝑆) & ⊢ 𝑌 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆))) | ||
Theorem | conjghm 18381* | Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝐴 + 𝑥) − 𝐴)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ (𝐺 GrpHom 𝐺) ∧ 𝐹:𝑋–1-1-onto→𝑋)) | ||
Theorem | conjsubg 18382* | A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ∈ (SubGrp‘𝐺)) | ||
Theorem | conjsubgen 18383* | A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 ≈ ran 𝐹) | ||
Theorem | conjnmz 18384* | A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) & ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 = ran 𝐹) | ||
Theorem | conjnmzb 18385* | Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) & ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)} ⇒ ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹))) | ||
Theorem | conjnsg 18386* | A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴)) ⇒ ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 = ran 𝐹) | ||
Theorem | qusghm 18387* | If 𝑌 is a normal subgroup of 𝐺, then the "natural map" from elements to their cosets is a group homomorphism from 𝐺 to 𝐺 / 𝑌. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌)) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌)) ⇒ ⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | ghmpropd 18388* | Group homomorphism depends only on the group attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐽)) & ⊢ (𝜑 → 𝐶 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐶 = (Base‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦)) ⇒ ⊢ (𝜑 → (𝐽 GrpHom 𝐾) = (𝐿 GrpHom 𝑀)) | ||
Syntax | cgim 18389 | The class of group isomorphism sets. |
class GrpIso | ||
Syntax | cgic 18390 | The class of the group isomorphism relation. |
class ≃𝑔 | ||
Definition | df-gim 18391* | An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ GrpIso = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}) | ||
Definition | df-gic 18392 | Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic groups share all global group properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ ≃𝑔 = (◡ GrpIso “ (V ∖ 1o)) | ||
Theorem | gimfn 18393 | The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ GrpIso Fn (Grp × Grp) | ||
Theorem | isgim 18394 | An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶)) | ||
Theorem | gimf1o 18395 | An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (Base‘𝑆) ⇒ ⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶) | ||
Theorem | gimghm 18396 | An isomorphism of groups is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) | ||
Theorem | isgim2 18397 | A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 22364. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 GrpHom 𝑅))) | ||
Theorem | subggim 18398 | Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝐹 “ 𝐴) ∈ (SubGrp‘𝑆))) | ||
Theorem | gimcnv 18399 | The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ (𝐹 ∈ (𝑆 GrpIso 𝑇) → ◡𝐹 ∈ (𝑇 GrpIso 𝑆)) | ||
Theorem | gimco 18400 | The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ ((𝐹 ∈ (𝑇 GrpIso 𝑈) ∧ 𝐺 ∈ (𝑆 GrpIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpIso 𝑈)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |