P. 197 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19601-19700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sylow2blem3 19601*	Sylow's second theorem. Putting together the results of sylow2a 19598 and the orbit-stabilizer theorem to show that 𝑃 does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some 𝑔 ∈ 𝑋 with ℎ𝑔𝐾 = 𝑔𝐾 for all ℎ ∈ 𝐻. This implies that invg(𝑔)ℎ𝑔 ∈ 𝐾, so ℎ is in the conjugated subgroup 𝑔𝐾invg(𝑔). (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))    &   ⊢ + = (+g‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝐾)    &   ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    &   ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻))    &   ⊢ (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
Theorem	sylow2b 19602*	Sylow's second theorem. Any 𝑃-group 𝐻 is a subgroup of a conjugated 𝑃-group 𝐾 of order 𝑃↑𝑛 ∥ (♯‘𝑋) with 𝑛 maximal. This is usually stated under the assumption that 𝐾 is a Sylow subgroup, but we use a slightly different definition, whose equivalence to this one requires this theorem. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻))    &   ⊢ (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
Theorem	slwhash 19603	A sylow subgroup has cardinality equal to the maximum power of 𝑃 dividing the group. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺))    ⇒   ⊢ (𝜑 → (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
Theorem	fislw 19604	The sylow subgroups of a finite group are exactly the groups which have cardinality equal to the maximum power of 𝑃 dividing the group. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
Theorem	sylow2 19605*	Sylow's second theorem. See also sylow2b 19602 for the "hard" part of the proof. Any two Sylow 𝑃-subgroups are conjugate to one another, and hence the same size, namely 𝑃↑(𝑃 pCnt ∣ 𝑋 ∣ ) (see fislw 19604). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 = ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
Theorem	sylow3lem1 19606*	Lemma for sylow3 19612, first part. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    ⇒   ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
Theorem	sylow3lem2 19607*	Lemma for sylow3 19612, first part. The stabilizer of a given Sylow subgroup 𝐾 in the group action ⊕ acting on all of 𝐺 is the normalizer NG(K). (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}    &   ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}    ⇒   ⊢ (𝜑 → 𝐻 = 𝑁)
Theorem	sylow3lem3 19608*	Lemma for sylow3 19612, first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup 𝐾. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}    &   ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}    ⇒   ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~QG 𝑁))))
Theorem	sylow3lem4 19609*	Lemma for sylow3 19612, first part. The number of Sylow subgroups is a divisor of the size of 𝐺 reduced by the size of a Sylow subgroup of 𝐺. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}    &   ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}    ⇒   ⊢ (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
Theorem	sylow3lem5 19610*	Lemma for sylow3 19612, second part. Reduce the group action of sylow3lem1 19606 to a given Sylow subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ ⊕ = (𝑥 ∈ 𝐾, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    ⇒   ⊢ (𝜑 → ⊕ ∈ ((𝐺 ↾s 𝐾) GrpAct (𝑃 pSyl 𝐺)))
Theorem	sylow3lem6 19611*	Lemma for sylow3 19612, second part. Using the lemma sylow2a 19598, show that the number of sylow subgroups is equivalent mod 𝑃 to the number of fixed points under the group action. But 𝐾 is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ((♯‘(𝑃 pSyl 𝐺)) mod 𝑃) = 1. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ ⊕ = (𝑥 ∈ 𝐾, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    &   ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}    ⇒   ⊢ (𝜑 → ((♯‘(𝑃 pSyl 𝐺)) mod 𝑃) = 1)
Theorem	sylow3 19612	Sylow's third theorem. The number of Sylow subgroups is a divisor of ∣ 𝐺 ∣ / 𝑑, where 𝑑 is the common order of a Sylow subgroup, and is equivalent to 1 mod 𝑃. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ 𝑁 = (♯‘(𝑃 pSyl 𝐺))    ⇒   ⊢ (𝜑 → (𝑁 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) ∧ (𝑁 mod 𝑃) = 1))
10.2.12  Direct products
Syntax	clsm 19613	Extend class notation with subgroup sum.
class LSSum
Syntax	cpj1 19614	Extend class notation with left projection.
class proj1
Definition	df-lsm 19615*	Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.)
⊢ LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦))))
Definition	df-pj1 19616*	Define the left projection function, which takes two subgroups 𝑡, 𝑢 with trivial intersection and returns a function mapping the elements of the subgroup sum 𝑡 + 𝑢 to their projections onto 𝑡. (The other projection function can be obtained by swapping the roles of 𝑡 and 𝑢.) (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ proj1 = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦)))))
Theorem	lsmfval 19617*	The subgroup sum function (for a group or vector space). (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ⊕ = (𝑡 ∈ 𝒫 𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥 + 𝑦))))
Theorem	lsmvalx 19618*	Subspace sum value (for a group or vector space). Extended domain version of lsmval 19627. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦)))
Theorem	lsmelvalx 19619*	Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 19628. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧)))
Theorem	lsmelvalix 19620	Subspace sum membership (for a group or vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ (𝑇 ⊕ 𝑈))
Theorem	oppglsm 19621	The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝑂 = (oppg‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝑇(LSSum‘𝑂)𝑈) = (𝑈 ⊕ 𝑇)
Theorem	lsmssv 19622	Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) ⊆ 𝐵)
Theorem	lsmless1x 19623	Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑅 ⊆ 𝑇) → (𝑅 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmless2x 19624	Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑅 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑇 ⊆ 𝑈) → (𝑅 ⊕ 𝑇) ⊆ (𝑅 ⊕ 𝑈))
Theorem	lsmub1x 19625	Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ⊆ 𝐵 ∧ 𝑈 ∈ (SubMnd‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmub2x 19626	Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ⊆ 𝐵) → 𝑈 ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmval 19627*	Subgroup sum value (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦)))
Theorem	lsmelval 19628*	Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧)))
Theorem	lsmelvali 19629	Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ (𝑇 ⊕ 𝑈))
Theorem	lsmelvalm 19630*	Subgroup sum membership analogue of lsmelval 19628 using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 − 𝑧)))
Theorem	lsmelvalmi 19631	Membership of vector subtraction in subgroup sum. (Contributed by NM, 27-Apr-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝑇 ⊕ 𝑈))
Theorem	lsmsubm 19632	The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ∈ (SubMnd‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubMnd‘𝐺))
Theorem	lsmsubg 19633	The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺))
Theorem	lsmcom2 19634	Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇))
10.2.12.1  Direct products (extension)
Theorem	smndlsmidm 19635	The direct product is idempotent for submonoids. (Contributed by AV, 27-Dec-2023.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝑈 ∈ (SubMnd‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈)
Theorem	lsmub1 19636	Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmub2 19637	Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑈 ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmunss 19638	Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ∪ 𝑈) ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmless1 19639	Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑇) → (𝑆 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmless2 19640	Subset implies subgroup sum subset. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑆 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈))
Theorem	lsmless12 19641	Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈)) → (𝑅 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈))
Theorem	lsmidm 19642	Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) (Proof shortened by AV, 27-Dec-2023.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈)
Theorem	lsmlub 19643	The least upper bound property of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑆 ⊆ 𝑈 ∧ 𝑇 ⊆ 𝑈) ↔ (𝑆 ⊕ 𝑇) ⊆ 𝑈))
Theorem	lsmss1 19644	Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑇 ⊕ 𝑈) = 𝑈)
Theorem	lsmss1b 19645	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊆ 𝑈 ↔ (𝑇 ⊕ 𝑈) = 𝑈))
Theorem	lsmss2 19646	Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑈 ⊆ 𝑇) → (𝑇 ⊕ 𝑈) = 𝑇)
Theorem	lsmss2b 19647	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑈 ⊆ 𝑇 ↔ (𝑇 ⊕ 𝑈) = 𝑇))
Theorem	lsmass 19648	Subgroup sum is associative. (Contributed by NM, 2-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈)))
Theorem	mndlsmidm 19649	Subgroup sum is idempotent for monoids. This corresponds to the observation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → (𝐵 ⊕ 𝐵) = 𝐵)
Theorem	lsm01 19650	Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝑋 ∈ (SubGrp‘𝐺) → (𝑋 ⊕ { 0 }) = 𝑋)
Theorem	lsm02 19651	Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 0 = (0g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝑋 ∈ (SubGrp‘𝐺) → ({ 0 } ⊕ 𝑋) = 𝑋)
Theorem	subglsm 19652	The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝐴 = (LSSum‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆) → (𝑇 ⊕ 𝑈) = (𝑇𝐴𝑈))
Theorem	lssnle 19653	Equivalent expressions for "not less than". (chnlei 31412 analog.) (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → (¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ⊊ (𝑇 ⊕ 𝑈)))
Theorem	lsmmod 19654	The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑆 ⊆ 𝑈) → (𝑆 ⊕ (𝑇 ∩ 𝑈)) = ((𝑆 ⊕ 𝑇) ∩ 𝑈))
Theorem	lsmmod2 19655	Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 8-Jan-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑈 ⊆ 𝑆) → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = ((𝑆 ∩ 𝑇) ⊕ 𝑈))
Theorem	lsmpropd 19656*	If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015.) (Revised by AV, 25-Apr-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (LSSum‘𝐾) = (LSSum‘𝐿))
Theorem	cntzrecd 19657	Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    ⇒   ⊢ (𝜑 → 𝑈 ⊆ (𝑍‘𝑇))
Theorem	lsmcntz 19658	The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ⊆ (𝑍‘𝑈) ↔ (𝑆 ⊆ (𝑍‘𝑈) ∧ 𝑇 ⊆ (𝑍‘𝑈))))
Theorem	lsmcntzr 19659	The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ (𝜑 → (𝑆 ⊆ (𝑍‘(𝑇 ⊕ 𝑈)) ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ 𝑆 ⊆ (𝑍‘𝑈))))
Theorem	lsmdisj 19660	Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 })    ⇒   ⊢ (𝜑 → ((𝑆 ∩ 𝑈) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 }))
Theorem	lsmdisj2 19661	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 })    ⇒   ⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 })
Theorem	lsmdisj3 19662	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 })    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇))    ⇒   ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 })
Theorem	lsmdisjr 19663	Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 })    ⇒   ⊢ (𝜑 → ((𝑆 ∩ 𝑇) = { 0 } ∧ (𝑆 ∩ 𝑈) = { 0 }))
Theorem	lsmdisj2r 19664	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 })    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    ⇒   ⊢ (𝜑 → ((𝑆 ⊕ 𝑈) ∩ 𝑇) = { 0 })
Theorem	lsmdisj3r 19665	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 })    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    ⇒   ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 })
Theorem	lsmdisj2a 19666	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → ((((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 } ∧ (𝑆 ∩ 𝑇) = { 0 }) ↔ ((𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 } ∧ (𝑆 ∩ 𝑈) = { 0 })))
Theorem	lsmdisj2b 19667	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → ((((𝑆 ⊕ 𝑈) ∩ 𝑇) = { 0 } ∧ (𝑆 ∩ 𝑈) = { 0 }) ↔ ((𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 })))
Theorem	lsmdisj3a 19668	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇))    ⇒   ⊢ (𝜑 → ((((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 } ∧ (𝑆 ∩ 𝑇) = { 0 }) ↔ ((𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 })))
Theorem	lsmdisj3b 19669	Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    ⇒   ⊢ (𝜑 → ((((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 } ∧ (𝑆 ∩ 𝑇) = { 0 }) ↔ ((𝑆 ∩ (𝑇 ⊕ 𝑈)) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 })))
Theorem	subgdisj1 19670	Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	subgdisj2 19671	Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 12-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷))    ⇒   ⊢ (𝜑 → 𝐵 = 𝐷)
Theorem	subgdisjb 19672	Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth 5451, this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-Jul-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	pj1fval 19673*	The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇𝑃𝑈) = (𝑧 ∈ (𝑇 ⊕ 𝑈) ↦ (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑧 = (𝑥 + 𝑦))))
Theorem	pj1val 19674*	The left projection function (for a direct product of group subspaces). (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇𝑃𝑈)‘𝑋) = (℩𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦)))
Theorem	pj1eu 19675*	Uniqueness of a left projection. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → ∃!𝑥 ∈ 𝑇 ∃𝑦 ∈ 𝑈 𝑋 = (𝑥 + 𝑦))
Theorem	pj1f 19676	The left projection function maps a direct subspace sum onto the left factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈):(𝑇 ⊕ 𝑈)⟶𝑇)
Theorem	pj2f 19677	The right projection function maps a direct subspace sum onto the right factor. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑈𝑃𝑇):(𝑇 ⊕ 𝑈)⟶𝑈)
Theorem	pj1id 19678	Any element of a direct subspace sum can be decomposed into projections onto the left and right factors. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by Mario Carneiro, 21-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ (𝑇 ⊕ 𝑈)) → 𝑋 = (((𝑇𝑃𝑈)‘𝑋) + ((𝑈𝑃𝑇)‘𝑋)))
Theorem	pj1eq 19679	Any element of a direct subspace sum can be decomposed uniquely into projections onto the left and right factors. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ (𝑇 ⊕ 𝑈))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑋 = (𝐵 + 𝐶) ↔ (((𝑇𝑃𝑈)‘𝑋) = 𝐵 ∧ ((𝑈𝑃𝑇)‘𝑋) = 𝐶)))
Theorem	pj1lid 19680	The left projection function is the identity on the left subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑇) → ((𝑇𝑃𝑈)‘𝑋) = 𝑋)
Theorem	pj1rid 19681	The left projection function is the zero operator on the right subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ((𝑇𝑃𝑈)‘𝑋) = 0 )
Theorem	pj1ghm 19682	The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝐺 ↾s (𝑇 ⊕ 𝑈)) GrpHom 𝐺))
Theorem	pj1ghm2 19683	The left projection function is a group homomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ 𝑃 = (proj1‘𝐺)    ⇒   ⊢ (𝜑 → (𝑇𝑃𝑈) ∈ ((𝐺 ↾s (𝑇 ⊕ 𝑈)) GrpHom (𝐺 ↾s 𝑇)))
Theorem	lsmhash 19684	The order of the direct product of groups. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 })    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈))    &   ⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘(𝑇 ⊕ 𝑈)) = ((♯‘𝑇) · (♯‘𝑈)))
10.2.13  Free groups
Syntax	cefg 19685	Extend class notation with the free group equivalence relation.
class ~FG
Syntax	cfrgp 19686	Extend class notation with the free group construction.
class freeGrp
Syntax	cvrgp 19687	Extend class notation with free group injection.
class varFGrp
Definition	df-efg 19688*	Define the free group equivalence relation, which is the smallest equivalence relation ≈ such that for any words 𝐴, 𝐵 and formal symbol 𝑥 with inverse invg𝑥, 𝐴𝐵 ≈ 𝐴𝑥(invg𝑥)𝐵. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ ~FG = (𝑖 ∈ V ↦ ∩ {𝑟 ∣ (𝑟 Er Word (𝑖 × 2o) ∧ ∀𝑥 ∈ Word (𝑖 × 2o)∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝑖 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))})
Definition	df-frgp 19689	Define the free group on a set 𝐼 of generators, defined as the quotient of the free monoid on 𝐼 × 2o (representing the generator elements and their formal inverses) by the free group equivalence relation df-efg 19688. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ freeGrp = (𝑖 ∈ V ↦ ((freeMnd‘(𝑖 × 2o)) /s ( ~FG ‘𝑖)))
Definition	df-vrgp 19690*	Define the canonical injection from the generating set 𝐼 into the base set of the free group. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ varFGrp = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ [⟨“⟨𝑗, ∅⟩”⟩]( ~FG ‘𝑖)))
Theorem	efgmval 19691*	Value of the formal inverse operation for the generating set of a free group. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ ((𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 2o) → (𝐴𝑀𝐵) = ⟨𝐴, (1o ∖ 𝐵)⟩)
Theorem	efgmf 19692*	The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
Theorem	efgmnvl 19693*	The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩)    ⇒   ⊢ (𝐴 ∈ (𝐼 × 2o) → (𝑀‘(𝑀‘𝐴)) = 𝐴)
Theorem	efgrcl 19694	Lemma for efgval 19696. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    ⇒   ⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o)))
Theorem	efglem 19695*	Lemma for efgval 19696. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    ⇒   ⊢ ∃𝑟(𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))
Theorem	efgval 19696*	Value of the free group construction. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ∼ = ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑥 ∈ 𝑊 ∀𝑛 ∈ (0...(♯‘𝑥))∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 2o 𝑥𝑟(𝑥 splice ⟨𝑛, 𝑛, ⟨“⟨𝑦, 𝑧⟩⟨𝑦, (1o ∖ 𝑧)⟩”⟩⟩))}
Theorem	efger 19697	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ∼ Er 𝑊
Theorem	efgi 19698	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ (((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐴))) ∧ (𝐽 ∈ 𝐼 ∧ 𝐾 ∈ 2o)) → 𝐴 ∼ (𝐴 splice ⟨𝑁, 𝑁, ⟨“⟨𝐽, 𝐾⟩⟨𝐽, (1o ∖ 𝐾)⟩”⟩⟩))
Theorem	efgi0 19699	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐴)) ∧ 𝐽 ∈ 𝐼) → 𝐴 ∼ (𝐴 splice ⟨𝑁, 𝑁, ⟨“⟨𝐽, ∅⟩⟨𝐽, 1o⟩”⟩⟩))
Theorem	efgi1 19700	Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑊 = ( I ‘Word (𝐼 × 2o))    &   ⊢ ∼ = ( ~FG ‘𝐼)    ⇒   ⊢ ((𝐴 ∈ 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐴)) ∧ 𝐽 ∈ 𝐼) → 𝐴 ∼ (𝐴 splice ⟨𝑁, 𝑁, ⟨“⟨𝐽, 1o⟩⟨𝐽, ∅⟩”⟩⟩))