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	|- B = ( Base ` G )
	qusbas2.2	|- .(+) = ( LSSum ` G )
	qusbas2.3	|- ( ( ph /\ x e. B ) -> N e. ( SubGrp ` G ) )
Assertion	qusbas2	|- ( ph -> ( B /. ( G ~QG N ) ) = ran ( x e. B |-> ( { x } .(+) N ) ) )

Proof

Step	Hyp	Ref	Expression
1		qusbas2.1	|- B = ( Base ` G )
2		qusbas2.2	|- .(+) = ( LSSum ` G )
3		qusbas2.3	|- ( ( ph /\ x e. B ) -> N e. ( SubGrp ` G ) )
4		df-qs	|- ( B /. ( G ~QG N ) ) = { y | E. x e. B y = [ x ] ( G ~QG N ) }
5		eqid	|- ( x e. B |-> [ x ] ( G ~QG N ) ) = ( x e. B |-> [ x ] ( G ~QG N ) )
6	5	rnmpt	|- ran ( x e. B |-> [ x ] ( G ~QG N ) ) = { y | E. x e. B y = [ x ] ( G ~QG N ) }
7	4 6	eqtr4i	|- ( B /. ( G ~QG N ) ) = ran ( x e. B |-> [ x ] ( G ~QG N ) )
8		simpr	|- ( ( ph /\ x e. B ) -> x e. B )
9	1 2 3 8	quslsm	|- ( ( ph /\ x e. B ) -> [ x ] ( G ~QG N ) = ( { x } .(+) N ) )
10	9	mpteq2dva	|- ( ph -> ( x e. B |-> [ x ] ( G ~QG N ) ) = ( x e. B |-> ( { x } .(+) N ) ) )
11	10	rneqd	|- ( ph -> ran ( x e. B |-> [ x ] ( G ~QG N ) ) = ran ( x e. B |-> ( { x } .(+) N ) ) )
12	7 11	eqtrid	|- ( ph -> ( B /. ( G ~QG N ) ) = ran ( x e. B |-> ( { x } .(+) N ) ) )