Theorem lagsubg2

Description: 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)

	Ref	Expression
Hypotheses	lagsubg.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	lagsubg.2	⊢ ∼ = ( 𝐺 ~QG 𝑌 )
	lagsubg.3	⊢ ( 𝜑 → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
	lagsubg.4	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	lagsubg2	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lagsubg.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		lagsubg.2	⊢ ∼ = ( 𝐺 ~QG 𝑌 )
3		lagsubg.3	⊢ ( 𝜑 → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
4		lagsubg.4	⊢ ( 𝜑 → 𝑋 ∈ Fin )
5	1 2	eqger	⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
6	3 5	syl	⊢ ( 𝜑 → ∼ Er 𝑋 )
7	6 4	qshash	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = Σ 𝑥 ∈ ( 𝑋 / ∼ ) ( ♯ ‘ 𝑥 ) )
8	1 2	eqgen	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑌 ≈ 𝑥 )
9	3 8	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑌 ≈ 𝑥 )
10	1	subgss	⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 )
11	3 10	syl	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
12	4 11	ssfid	⊢ ( 𝜑 → 𝑌 ∈ Fin )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑌 ∈ Fin )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑋 ∈ Fin )
15	6	qsss	⊢ ( 𝜑 → ( 𝑋 / ∼ ) ⊆ 𝒫 𝑋 )
16	15	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑥 ∈ 𝒫 𝑋 )
17	16	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑥 ⊆ 𝑋 )
18	14 17	ssfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → 𝑥 ∈ Fin )
19		hashen	⊢ ( ( 𝑌 ∈ Fin ∧ 𝑥 ∈ Fin ) → ( ( ♯ ‘ 𝑌 ) = ( ♯ ‘ 𝑥 ) ↔ 𝑌 ≈ 𝑥 ) )
20	13 18 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → ( ( ♯ ‘ 𝑌 ) = ( ♯ ‘ 𝑥 ) ↔ 𝑌 ≈ 𝑥 ) )
21	9 20	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 / ∼ ) ) → ( ♯ ‘ 𝑌 ) = ( ♯ ‘ 𝑥 ) )
22	21	sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ ( 𝑋 / ∼ ) ( ♯ ‘ 𝑌 ) = Σ 𝑥 ∈ ( 𝑋 / ∼ ) ( ♯ ‘ 𝑥 ) )
23		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
24	4 23	sylib	⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
25	24 15	ssfid	⊢ ( 𝜑 → ( 𝑋 / ∼ ) ∈ Fin )
26		hashcl	⊢ ( 𝑌 ∈ Fin → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
27	12 26	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
28	27	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℂ )
29		fsumconst	⊢ ( ( ( 𝑋 / ∼ ) ∈ Fin ∧ ( ♯ ‘ 𝑌 ) ∈ ℂ ) → Σ 𝑥 ∈ ( 𝑋 / ∼ ) ( ♯ ‘ 𝑌 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝑌 ) ) )
30	25 28 29	syl2anc	⊢ ( 𝜑 → Σ 𝑥 ∈ ( 𝑋 / ∼ ) ( ♯ ‘ 𝑌 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝑌 ) ) )
31	7 22 30	3eqtr2d	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝑌 ) ) )