This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusima

Description: The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses qusima.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
qusima.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
qusima.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
qusima.e ⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
qusima.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
qusima.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
qusima.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
qusima.s ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
Assertion qusima ( 𝜑 → ( 𝐸 ‘ 𝐻 ) = ( 𝐹 “ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 qusima.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 qusima.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
3 qusima.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
4 qusima.e ⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
5 qusima.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
6 qusima.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
7 qusima.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑆 )
8 qusima.s ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
9 5 reseq1i ⊢ ( 𝐹 ↾ 𝐻 ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ↾ 𝐻 )
10 8 7 sseldd ⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
11 1 subgss ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝐵 )
12 10 11 syl ⊢ ( 𝜑 → 𝐻 ⊆ 𝐵 )
13 12 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ↾ 𝐻 ) = ( 𝑥 ∈ 𝐻 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) )
14 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
15 6 14 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
17 12 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → 𝑥 ∈ 𝐵 )
18 1 3 16 17 quslsm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐻 ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
19 18 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐻 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
20 13 19 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ↾ 𝐻 ) = ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
21 9 20 eqtr2id ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝐹 ↾ 𝐻 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝐹 ↾ 𝐻 ) )
23 22 rneqd ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ran ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝐹 ↾ 𝐻 ) )
24 mpteq1 ⊢ ( ℎ = 𝐻 → ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
25 24 rneqd ⊢ ( ℎ = 𝐻 → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝑥 ∈ 𝐻 ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
27 df-ima ⊢ ( 𝐹 “ 𝐻 ) = ran ( 𝐹 ↾ 𝐻 )
28 27 a1i ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( 𝐹 “ 𝐻 ) = ran ( 𝐹 ↾ 𝐻 ) )
29 23 26 28 3eqtr4d ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝐹 “ 𝐻 ) )
30 1 fvexi ⊢ 𝐵 ∈ V
31 30 mptex ⊢ ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) ∈ V
32 5 31 eqeltri ⊢ 𝐹 ∈ V
33 imaexg ⊢ ( 𝐹 ∈ V → ( 𝐹 “ 𝐻 ) ∈ V )
34 32 33 mp1i ⊢ ( 𝜑 → ( 𝐹 “ 𝐻 ) ∈ V )
35 4 29 7 34 fvmptd2 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐻 ) = ( 𝐹 “ 𝐻 ) )