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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
qusrn.e ⊢ 𝑈 = ( 𝐵 / ( 𝐺 ~QG 𝑁 ) )
qusrn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
qusrn.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
Assertion qusrn ( 𝜑 → ran 𝐹 = 𝑈 )

Proof

Step Hyp Ref Expression
1 qusrn.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 qusrn.e ⊢ 𝑈 = ( 𝐵 / ( 𝐺 ~QG 𝑁 ) )
3 qusrn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
4 qusrn.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
5 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
6 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
7 4 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
9 1 5 8 qusbas2 ⊢ ( 𝜑 → ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) )
10 2 9 eqtrid ⊢ ( 𝜑 → 𝑈 = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) )
11 ovex ⊢ ( 𝐺 ~QG 𝑁 ) ∈ V
12 ecexg ⊢ ( ( 𝐺 ~QG 𝑁 ) ∈ V → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ∈ V )
13 11 12 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ∈ V )
14 3 13 dmmptd ⊢ ( 𝜑 → dom 𝐹 = 𝐵 )
15 14 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐵 ) )
16 eqid ⊢ ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
17 eqid ⊢ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) ) = ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) )
18 subgrcl ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
19 1 subgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
20 4 6 18 19 4syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
21 ssidd ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ⊆ ( SubGrp ‘ 𝐺 ) )
22 1 16 5 17 3 4 20 21 qusima ⊢ ( 𝜑 → ( ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) ) ‘ 𝐵 ) = ( 𝐹 “ 𝐵 ) )
23 mpteq1 ⊢ ( ℎ = 𝐵 → ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) )
24 23 rneqd ⊢ ( ℎ = 𝐵 → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) )
25 20 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) ∈ V )
26 25 rnexd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) ∈ V )
27 17 24 20 26 fvmptd3 ⊢ ( 𝜑 → ( ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) ) ‘ 𝐵 ) = ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) )
28 15 22 27 3eqtr2rd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) = ( 𝐹 “ dom 𝐹 ) )
29 imadmrn ⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
30 28 29 eqtrdi ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ ( { 𝑥 } ( LSSum ‘ 𝐺 ) 𝑁 ) ) = ran 𝐹 )
31 10 30 eqtr2d ⊢ ( 𝜑 → ran 𝐹 = 𝑈 )