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