qusima

Description: The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024)

	Ref	Expression
Hypotheses	qusima.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	qusima.q	⊢ 𝑄 = ( 𝐺 /_s ( 𝐺 ~_QG 𝑁 ) )
	qusima.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	qusima.e	⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
	qusima.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) )
	qusima.n	⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
	qusima.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
	qusima.s	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
Assertion	qusima	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐻 ) = ( 𝐹 “ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		qusima.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		qusima.q	⊢ 𝑄 = ( 𝐺 /_s ( 𝐺 ~_QG 𝑁 ) )
3		qusima.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
4		qusima.e	⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
5		qusima.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) )
6		qusima.n	⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
7		qusima.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
8		qusima.s	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
9	5	reseq1i	⊢ ( 𝐹 ↾ 𝐻 ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) ↾ 𝐻 )
10	8 7	sseldd	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
11	1	subgss	⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝐵 )
12	10 11	syl	⊢ ( 𝜑 → 𝐻 ⊆ 𝐵 )
13	12	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) ↾ 𝐻 ) = ( 𝑥 ∈ 𝐻 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) )
14		nsgsubg	⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
15	6 14	syl	⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
17	12	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝑥 ∈ 𝐵 )
18	1 3 16 17	quslsm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
19	18	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐻 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) = ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
20	13 19	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) ↾ 𝐻 ) = ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
21	9 20	syl5req	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝐹 ↾ 𝐻 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝐹 ↾ 𝐻 ) )
23	22	rneqd	⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ran ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝐹 ↾ 𝐻 ) )
24		mpteq1	⊢ ( ℎ = 𝐻 → ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
25	24	rneqd	⊢ ( ℎ = 𝐻 → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
26	25	adantl	⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
27		df-ima	⊢ ( 𝐹 “ 𝐻 ) = ran ( 𝐹 ↾ 𝐻 )
28	27	a1i	⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( 𝐹 “ 𝐻 ) = ran ( 𝐹 ↾ 𝐻 ) )
29	23 26 28	3eqtr4d	⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝐹 “ 𝐻 ) )
30	1	fvexi	⊢ 𝐵 ∈ V
31	30	mptex	⊢ ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) ∈ V
32	5 31	eqeltri	⊢ 𝐹 ∈ V
33		imaexg	⊢ ( 𝐹 ∈ V → ( 𝐹 “ 𝐻 ) ∈ V )
34	32 33	mp1i	⊢ ( 𝜑 → ( 𝐹 “ 𝐻 ) ∈ V )
35	4 29 7 34	fvmptd2	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐻 ) = ( 𝐹 “ 𝐻 ) )

Metamath Proof Explorer

Theorem qusima

Proof