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 ∈ B ⟼ x G ~ QG N
qusrn.n ⊢ φ → N ∈ NrmSGrp ⁡ G
Assertion qusrn ⊢ φ → 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 ∈ B ⟼ x G ~ QG N
4 qusrn.n ⊢ φ → N ∈ NrmSGrp ⁡ G
5 eqid ⊢ LSSum ⁡ G = LSSum ⁡ G
6 nsgsubg ⊢ N ∈ NrmSGrp ⁡ G → N ∈ SubGrp ⁡ G
7 4 6 syl ⊢ φ → N ∈ SubGrp ⁡ G
8 7 adantr ⊢ φ ∧ x ∈ B → N ∈ SubGrp ⁡ G
9 1 5 8 qusbas2 ⊢ φ → B / G ~ QG N = ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N
10 2 9 eqtrid ⊢ φ → U = ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N
11 ovex ⊢ G ~ QG N ∈ V
12 ecexg ⊢ G ~ QG N ∈ V → x G ~ QG N ∈ V
13 11 12 mp1i ⊢ φ ∧ x ∈ B → x G ~ QG N ∈ V
14 3 13 dmmptd ⊢ φ → dom ⁡ F = B
15 14 imaeq2d ⊢ φ → F dom ⁡ F = F B
16 eqid ⊢ G / 𝑠 G ~ QG N = G / 𝑠 G ~ QG N
17 eqid ⊢ h ∈ SubGrp ⁡ G ⟼ ran ⁡ x ∈ h ⟼ x LSSum ⁡ G N = h ∈ SubGrp ⁡ G ⟼ ran ⁡ x ∈ h ⟼ x LSSum ⁡ G N
18 subgrcl ⊢ N ∈ SubGrp ⁡ G → G ∈ Grp
19 1 subgid ⊢ G ∈ Grp → B ∈ SubGrp ⁡ G
20 4 6 18 19 4syl ⊢ φ → B ∈ SubGrp ⁡ G
21 ssidd ⊢ φ → SubGrp ⁡ G ⊆ SubGrp ⁡ G
22 1 16 5 17 3 4 20 21 qusima ⊢ φ → h ∈ SubGrp ⁡ G ⟼ ran ⁡ x ∈ h ⟼ x LSSum ⁡ G N ⁡ B = F B
23 mpteq1 ⊢ h = B → x ∈ h ⟼ x LSSum ⁡ G N = x ∈ B ⟼ x LSSum ⁡ G N
24 23 rneqd ⊢ h = B → ran ⁡ x ∈ h ⟼ x LSSum ⁡ G N = ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N
25 20 mptexd ⊢ φ → x ∈ B ⟼ x LSSum ⁡ G N ∈ V
26 25 rnexd ⊢ φ → ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N ∈ V
27 17 24 20 26 fvmptd3 ⊢ φ → h ∈ SubGrp ⁡ G ⟼ ran ⁡ x ∈ h ⟼ x LSSum ⁡ G N ⁡ B = ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N
28 15 22 27 3eqtr2rd ⊢ φ → ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N = F dom ⁡ F
29 imadmrn ⊢ F dom ⁡ F = ran ⁡ F
30 28 29 eqtrdi ⊢ φ → ran ⁡ x ∈ B ⟼ x LSSum ⁡ G N = ran ⁡ F
31 10 30 eqtr2d ⊢ φ → ran ⁡ F = U