Metamath Proof Explorer

Theorem qusrn

Description: The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses qusrn.b 
|- B = ( Base ` G )
qusrn.e 
|- U = ( B /. ( G ~QG N ) )
qusrn.f 
|- F = ( x e. B |-> [ x ] ( G ~QG N ) )
qusrn.n 
|- ( ph -> N e. ( NrmSGrp ` G ) )
Assertion qusrn 
|- ( ph -> ran F = U )

Proof

Step Hyp Ref Expression
1 qusrn.b 
 |-  B = ( Base ` G )
2 qusrn.e 
 |-  U = ( B /. ( G ~QG N ) )
3 qusrn.f 
 |-  F = ( x e. B |-> [ x ] ( G ~QG N ) )
4 qusrn.n 
 |-  ( ph -> N e. ( NrmSGrp ` G ) )
5 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
6 nsgsubg 
 |-  ( N e. ( NrmSGrp ` G ) -> N e. ( SubGrp ` G ) )
7 4 6 syl 
 |-  ( ph -> N e. ( SubGrp ` G ) )
8 7 adantr 
 |-  ( ( ph /\ x e. B ) -> N e. ( SubGrp ` G ) )
9 1 5 8 qusbas2 
 |-  ( ph -> ( B /. ( G ~QG N ) ) = ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) )
10 2 9 eqtrid 
 |-  ( ph -> U = ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) )
11 ovex 
 |-  ( G ~QG N ) e. _V
12 ecexg 
 |-  ( ( G ~QG N ) e. _V -> [ x ] ( G ~QG N ) e. _V )
13 11 12 mp1i 
 |-  ( ( ph /\ x e. B ) -> [ x ] ( G ~QG N ) e. _V )
14 3 13 dmmptd 
 |-  ( ph -> dom F = B )
15 14 imaeq2d 
 |-  ( ph -> ( F " dom F ) = ( F " B ) )
16 eqid 
 |-  ( G /s ( G ~QG N ) ) = ( G /s ( G ~QG N ) )
17 eqid 
 |-  ( h e. ( SubGrp ` G ) |-> ran ( x e. h |-> ( { x } ( LSSum ` G ) N ) ) ) = ( h e. ( SubGrp ` G ) |-> ran ( x e. h |-> ( { x } ( LSSum ` G ) N ) ) )
18 subgrcl 
 |-  ( N e. ( SubGrp ` G ) -> G e. Grp )
19 1 subgid 
 |-  ( G e. Grp -> B e. ( SubGrp ` G ) )
20 4 6 18 19 4syl 
 |-  ( ph -> B e. ( SubGrp ` G ) )
21 ssidd 
 |-  ( ph -> ( SubGrp ` G ) C_ ( SubGrp ` G ) )
22 1 16 5 17 3 4 20 21 qusima 
 |-  ( ph -> ( ( h e. ( SubGrp ` G ) |-> ran ( x e. h |-> ( { x } ( LSSum ` G ) N ) ) ) ` B ) = ( F " B ) )
23 mpteq1 
 |-  ( h = B -> ( x e. h |-> ( { x } ( LSSum ` G ) N ) ) = ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) )
24 23 rneqd 
 |-  ( h = B -> ran ( x e. h |-> ( { x } ( LSSum ` G ) N ) ) = ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) )
25 20 mptexd 
 |-  ( ph -> ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) e. _V )
26 25 rnexd 
 |-  ( ph -> ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) e. _V )
27 17 24 20 26 fvmptd3 
 |-  ( ph -> ( ( h e. ( SubGrp ` G ) |-> ran ( x e. h |-> ( { x } ( LSSum ` G ) N ) ) ) ` B ) = ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) )
28 15 22 27 3eqtr2rd 
 |-  ( ph -> ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) = ( F " dom F ) )
29 imadmrn 
 |-  ( F " dom F ) = ran F
30 28 29 eqtrdi 
 |-  ( ph -> ran ( x e. B |-> ( { x } ( LSSum ` G ) N ) ) = ran F )
31 10 30 eqtr2d 
 |-  ( ph -> ran F = U )