This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusbas2

Description: Alternate definition of the group quotient set, as the set of all cosets of the form ( { x } .(+) N ) . (Contributed by Thierry Arnoux, 22-Mar-2025)

		Ref	Expression
	Hypotheses	qusbas2.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
		qusbas2.2	⊢ ⊕ = ( LSSum ‘ 𝐺 )
		qusbas2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
	Assertion	qusbas2	⊢ ( 𝜑 → ( 𝐵 / ( 𝐺 ~_QG 𝑁 ) ) = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qusbas2.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		qusbas2.2	⊢ ⊕ = ( LSSum ‘ 𝐺 )
3		qusbas2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
4		df-qs	⊢ ( 𝐵 / ( 𝐺 ~_QG 𝑁 ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) }
5		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) )
6	5	rnmpt	⊢ ran ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 = [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) }
7	4 6	eqtr4i	⊢ ( 𝐵 / ( 𝐺 ~_QG 𝑁 ) ) = ran ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
9	1 2 3 8	quslsm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
10	9	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
11	10	rneqd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~_QG 𝑁 ) ) = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
12	7 11	eqtrid	⊢ ( 𝜑 → ( 𝐵 / ( 𝐺 ~_QG 𝑁 ) ) = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )