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 ⊢B=BaseG
qusima.q ⊢Q=G/𝑠G~QGN
qusima.p ⊢⊕˙=LSSum⁡G
qusima.e ⊢E=h∈S⟼ran⁡x∈h⟼x⊕˙N
qusima.f ⊢F=x∈B⟼xG~QGN
qusima.n ⊢φ→N∈NrmSGrp⁡G
qusima.h ⊢φ→H∈S
qusima.s ⊢φ→S⊆SubGrp⁡G
Assertion qusima ⊢φ→E⁡H=FH

Proof

Step Hyp Ref Expression
1 qusima.b ⊢B=BaseG
2 qusima.q ⊢Q=G/𝑠G~QGN
3 qusima.p ⊢⊕˙=LSSum⁡G
4 qusima.e ⊢E=h∈S⟼ran⁡x∈h⟼x⊕˙N
5 qusima.f ⊢F=x∈B⟼xG~QGN
6 qusima.n ⊢φ→N∈NrmSGrp⁡G
7 qusima.h ⊢φ→H∈S
8 qusima.s ⊢φ→S⊆SubGrp⁡G
9 5 reseq1i ⊢F↾H=x∈B⟼xG~QGN↾H
10 8 7 sseldd ⊢φ→H∈SubGrp⁡G
11 1 subgss ⊢H∈SubGrp⁡G→H⊆B
12 10 11 syl ⊢φ→H⊆B
13 12 resmptd ⊢φ→x∈B⟼xG~QGN↾H=x∈H⟼xG~QGN
14 nsgsubg ⊢N∈NrmSGrp⁡G→N∈SubGrp⁡G
15 6 14 syl ⊢φ→N∈SubGrp⁡G
16 15 adantr ⊢φ∧x∈H→N∈SubGrp⁡G
17 12 sselda ⊢φ∧x∈H→x∈B
18 1 3 16 17 quslsm ⊢φ∧x∈H→xG~QGN=x⊕˙N
19 18 mpteq2dva ⊢φ→x∈H⟼xG~QGN=x∈H⟼x⊕˙N
20 13 19 eqtrd ⊢φ→x∈B⟼xG~QGN↾H=x∈H⟼x⊕˙N
21 9 20 eqtr2id ⊢φ→x∈H⟼x⊕˙N=F↾H
22 21 adantr ⊢φ∧h=H→x∈H⟼x⊕˙N=F↾H
23 22 rneqd ⊢φ∧h=H→ran⁡x∈H⟼x⊕˙N=ran⁡F↾H
24 mpteq1 ⊢h=H→x∈h⟼x⊕˙N=x∈H⟼x⊕˙N
25 24 rneqd ⊢h=H→ran⁡x∈h⟼x⊕˙N=ran⁡x∈H⟼x⊕˙N
26 25 adantl ⊢φ∧h=H→ran⁡x∈h⟼x⊕˙N=ran⁡x∈H⟼x⊕˙N
27 df-ima ⊢FH=ran⁡F↾H
28 27 a1i ⊢φ∧h=H→FH=ran⁡F↾H
29 23 26 28 3eqtr4d ⊢φ∧h=H→ran⁡x∈h⟼x⊕˙N=FH
30 1 fvexi ⊢B∈V
31 30 mptex ⊢x∈B⟼xG~QGN∈V
32 5 31 eqeltri ⊢F∈V
33 imaexg ⊢F∈V→FH∈V
34 32 33 mp1i ⊢φ→FH∈V
35 4 29 7 34 fvmptd2 ⊢φ→E⁡H=FH