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	submod 19601	The order of an element is the same in a submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.)
⊢ 𝐻 = (𝐺 ↾s 𝑌)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑃 = (od‘𝐻)    ⇒   ⊢ ((𝑌 ∈ (SubMnd‘𝐺) ∧ 𝐴 ∈ 𝑌) → (𝑂‘𝐴) = (𝑃‘𝐴))
Theorem	subgod 19602	The order of an element is the same in a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015.) (Proof shortened by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑌)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑃 = (od‘𝐻)    ⇒   ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑌) → (𝑂‘𝐴) = (𝑃‘𝐴))
Theorem	odsubdvds 19603	The order of an element of a subgroup divides the order of the subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆) → (𝑂‘𝐴) ∥ (♯‘𝑆))
Theorem	odf1o1 19604*	An element with zero order has infinitely many multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–1-1-onto→(𝐾‘{𝐴}))
Theorem	odf1o2 19605*	An element with nonzero order has as many multiples as its order. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑥 ∈ (0..^(𝑂‘𝐴)) ↦ (𝑥 · 𝐴)):(0..^(𝑂‘𝐴))–1-1-onto→(𝐾‘{𝐴}))
Theorem	odhash 19606	An element of zero order generates an infinite subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (♯‘(𝐾‘{𝐴})) = +∞)
Theorem	odhash2 19607	If an element has nonzero order, it generates a subgroup with size equal to the order. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘(𝐾‘{𝐴})) = (𝑂‘𝐴))
Theorem	odhash3 19608	An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝐾‘{𝐴}) ∈ Fin) → (𝑂‘𝐴) = (♯‘(𝐾‘{𝐴})))
Theorem	odngen 19609*	A cyclic subgroup of size (𝑂‘𝐴) has (ϕ‘(𝑂‘𝐴)) generators. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘{𝑥 ∈ (𝐾‘{𝐴}) ∣ (𝑂‘𝑥) = (𝑂‘𝐴)}) = (ϕ‘(𝑂‘𝐴)))
Theorem	gexval 19610*	Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016.) (Revised by AV, 26-Sep-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐸 = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )))
Theorem	gexlem1 19611*	The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }    ⇒   ⊢ (𝐺 ∈ 𝑉 → ((𝐸 = 0 ∧ 𝐼 = ∅) ∨ 𝐸 ∈ 𝐼))
Theorem	gexcl 19612	The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐸 ∈ ℕ0)
Theorem	gexid 19613	Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝐸 · 𝐴) = 0 )
Theorem	gexlem2 19614*	Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 ) → 𝐸 ∈ (1...𝑁))
Theorem	gexdvdsi 19615	Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁) → (𝑁 · 𝐴) = 0 )
Theorem	gexdvds 19616*	The only 𝑁 that annihilate all the elements of the group are the multiples of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 ))
Theorem	gexdvds2 19617*	An integer divides the group exponent iff it divides all the group orders. In other words, the group exponent is the LCM of the orders of all the elements. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑂‘𝑥) ∥ 𝑁))
Theorem	gexod 19618	Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∥ 𝐸)
Theorem	gexcl3 19619*	If the order of every group element is bounded by 𝑁, the group has finite exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (𝑂‘𝑥) ∈ (1...𝑁)) → 𝐸 ∈ ℕ)
Theorem	gexnnod 19620	Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ)
Theorem	gexcl2 19621	The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∈ ℕ)
Theorem	gexdvds3 19622	The exponent of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∥ (♯‘𝑋))
Theorem	gex1 19623	A group or monoid has exponent 1 iff it is trivial. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → (𝐸 = 1 ↔ 𝑋 ≈ 1o))
Theorem	ispgp 19624*	A group is a 𝑃-group if every element has some power of 𝑃 as its order. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ ℕ0 (𝑂‘𝑥) = (𝑃↑𝑛)))
Theorem	pgpprm 19625	Reverse closure for the first argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ)
Theorem	pgpgrp 19626	Reverse closure for the second argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ (𝑃 pGrp 𝐺 → 𝐺 ∈ Grp)
Theorem	pgpfi1 19627	A finite group with order a power of a prime 𝑃 is a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → ((♯‘𝑋) = (𝑃↑𝑁) → 𝑃 pGrp 𝐺))
Theorem	pgp0 19628	The identity subgroup is a 𝑃-group for every prime 𝑃. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) → 𝑃 pGrp (𝐺 ↾s { 0 }))
Theorem	subgpgp 19629	A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ ((𝑃 pGrp 𝐺 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑆))
Theorem	sylow1lem1 19630*	Lemma for sylow1 19635. The p-adic valuation of the size of 𝑆 is equal to the number of excess powers of 𝑃 in (♯‘𝑋) / (𝑃↑𝑁). (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋))    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)}    ⇒   ⊢ (𝜑 → ((♯‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (♯‘𝑆)) = ((𝑃 pCnt (♯‘𝑋)) − 𝑁)))
Theorem	sylow1lem2 19631*	Lemma for sylow1 19635. The function ⊕ is a group action on 𝑆. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋))    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)}    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    ⇒   ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆))
Theorem	sylow1lem3 19632*	Lemma for sylow1 19635. One of the orbits of the group action has p-adic valuation less than the prime count of the set 𝑆. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋))    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)}    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (♯‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))
Theorem	sylow1lem4 19633*	Lemma for sylow1 19635. The stabilizer subgroup of any element of 𝑆 is at most 𝑃↑𝑁 in size. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋))    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)}    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵}    ⇒   ⊢ (𝜑 → (♯‘𝐻) ≤ (𝑃↑𝑁))
Theorem	sylow1lem5 19634*	Lemma for sylow1 19635. Using Lagrange's theorem and the orbit-stabilizer theorem, show that there is a subgroup with size exactly 𝑃↑𝑁. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋))    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)}    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵}    &   ⊢ (𝜑 → (𝑃 pCnt (♯‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))    ⇒   ⊢ (𝜑 → ∃ℎ ∈ (SubGrp‘𝐺)(♯‘ℎ) = (𝑃↑𝑁))
Theorem	sylow1 19635*	Sylow's first theorem. If 𝑃↑𝑁 is a prime power that divides the cardinality of 𝐺, then 𝐺 has a supgroup with size 𝑃↑𝑁. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋))    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ (SubGrp‘𝐺)(♯‘𝑔) = (𝑃↑𝑁))
Theorem	odcau 19636*	Cauchy's theorem for the order of an element in a group. A finite group whose order divides a prime 𝑃 contains an element of order 𝑃. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (♯‘𝑋)) → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃)
Theorem	pgpfi 19637*	The converse to pgpfi1 19627. A finite group is a 𝑃-group iff it has size some power of 𝑃. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0 (♯‘𝑋) = (𝑃↑𝑛))))
Theorem	pgpfi2 19638	Alternate version of pgpfi 19637. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ (♯‘𝑋) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
Theorem	pgphash 19639	The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝑃 pGrp 𝐺 ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
Theorem	isslw 19640*	The property of being a Sylow subgroup. A Sylow 𝑃-subgroup is a 𝑃-group which has no proper supersets that are also 𝑃-groups. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ ∀𝑘 ∈ (SubGrp‘𝐺)((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘)))
Theorem	slwprm 19641	Reverse closure for the first argument of a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) (Revised by Mario Carneiro, 2-May-2015.)
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 ∈ ℙ)
Theorem	slwsubg 19642	A Sylow 𝑃-subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝐻 ∈ (SubGrp‘𝐺))
Theorem	slwispgp 19643	Defining property of a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑆 = (𝐺 ↾s 𝐾)    ⇒   ⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆) ↔ 𝐻 = 𝐾))
Theorem	slwpss 19644	A proper superset of a Sylow subgroup is not a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑆 = (𝐺 ↾s 𝐾)    ⇒   ⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐻 ⊊ 𝐾) → ¬ 𝑃 pGrp 𝑆)
Theorem	slwpgp 19645	A Sylow 𝑃-subgroup is a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑆 = (𝐺 ↾s 𝐻)    ⇒   ⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 pGrp 𝑆)
Theorem	pgpssslw 19646*	Every 𝑃-subgroup is contained in a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑆 = (𝐺 ↾s 𝐻)    &   ⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↦ (♯‘𝑥))    ⇒   ⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻 ⊆ 𝑘)
Theorem	slwn0 19647	Every finite group contains a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝑃 pSyl 𝐺) ≠ ∅)
Theorem	subgslw 19648	A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse need not be true.) (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ⊆ 𝑆) → 𝐾 ∈ (𝑃 pSyl 𝐻))
Theorem	sylow2alem1 19649*	Lemma for sylow2a 19651. An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌))    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ Fin)    &   ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢}    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ = {𝐴})
Theorem	sylow2alem2 19650*	Lemma for sylow2a 19651. All the orbits which are not for fixed points have size ∣ 𝐺 ∣ / ∣ 𝐺𝑥 ∣ (where 𝐺𝑥 is the stabilizer subgroup) and thus are powers of 𝑃. And since they are all nontrivial (because any orbit which is a singleton is a fixed point), they all divide 𝑃, and so does the sum of all of them. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌))    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ Fin)    &   ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢}    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(♯‘𝑧))
Theorem	sylow2a 19651*	A named lemma of Sylow's second and third theorems. If 𝐺 is a finite 𝑃-group that acts on the finite set 𝑌, then the set 𝑍 of all points of 𝑌 fixed by every element of 𝐺 has cardinality equivalent to the cardinality of 𝑌, mod 𝑃. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌))    &   ⊢ (𝜑 → 𝑃 pGrp 𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ Fin)    &   ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢}    &   ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ (𝜑 → 𝑃 ∥ ((♯‘𝑌) − (♯‘𝑍)))
Theorem	sylow2blem1 19652*	Lemma for sylow2b 19655. Evaluate the group action on a left coset. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))    &   ⊢ + = (+g‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝐾)    &   ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = [(𝐵 + 𝐶)] ∼ )
Theorem	sylow2blem2 19653*	Lemma for sylow2b 19655. Left multiplication in a subgroup 𝐻 is a group action on the set of all left cosets of 𝐾. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))    &   ⊢ + = (+g‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝐾)    &   ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)))    ⇒   ⊢ (𝜑 → · ∈ ((𝐺 ↾s 𝐻) GrpAct (𝑋 / ∼ )))
Theorem	sylow2blem3 19654*	Sylow's second theorem. Putting together the results of sylow2a 19651 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 19655*	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 19656	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 19657	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 19658*	Sylow's second theorem. See also sylow2b 19655 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 19657). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺))    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 = ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))
Theorem	sylow3lem1 19659*	Lemma for sylow3 19665, first part. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)))    ⇒   ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
Theorem	sylow3lem2 19660*	Lemma for sylow3 19665, 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 19661*	Lemma for sylow3 19665, 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 19662*	Lemma for sylow3 19665, 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 19663*	Lemma for sylow3 19665, second part. Reduce the group action of sylow3lem1 19659 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 19664*	Lemma for sylow3 19665, second part. Using the lemma sylow2a 19651, 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 19665	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 19666	Extend class notation with subgroup sum.
class LSSum
Syntax	cpj1 19667	Extend class notation with left projection.
class proj1
Definition	df-lsm 19668*	Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.)
⊢ LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦))))
Definition	df-pj1 19669*	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 19670*	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 19671*	Subspace sum value (for a group or vector space). Extended domain version of lsmval 19680. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦)))
Theorem	lsmelvalx 19672*	Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 19681. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧)))
Theorem	lsmelvalix 19673	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 19674	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 19675	Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) ⊆ 𝐵)
Theorem	lsmless1x 19676	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 19677	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 19678	Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ⊆ 𝐵 ∧ 𝑈 ∈ (SubMnd‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmub2x 19679	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 19680*	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 19681*	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 19682	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 19683*	Subgroup sum membership analogue of lsmelval 19681 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 19684	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 19685	The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ∈ (SubMnd‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubMnd‘𝐺))
Theorem	lsmsubg 19686	The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺))
Theorem	lsmcom2 19687	Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    &   ⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇))
10.2.12.1  Direct products (extension)
Theorem	smndlsmidm 19688	The direct product is idempotent for submonoids. (Contributed by AV, 27-Dec-2023.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (𝑈 ∈ (SubMnd‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈)
Theorem	lsmub1 19689	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 19690	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 19691	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 19692	Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑇) → (𝑆 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈))
Theorem	lsmless2 19693	Subset implies subgroup sum subset. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑆 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈))
Theorem	lsmless12 19694	Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈)) → (𝑅 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈))
Theorem	lsmidm 19695	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 19696	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 19697	Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑇 ⊕ 𝑈) = 𝑈)
Theorem	lsmss1b 19698	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊆ 𝑈 ↔ (𝑇 ⊕ 𝑈) = 𝑈))
Theorem	lsmss2 19699	Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑈 ⊆ 𝑇) → (𝑇 ⊕ 𝑈) = 𝑇)
Theorem	lsmss2b 19700	Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
⊢ ⊕ = (LSSum‘𝐺)    ⇒   ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑈 ⊆ 𝑇 ↔ (𝑇 ⊕ 𝑈) = 𝑇))