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

Proof

Step Hyp Ref Expression
1 qusima.b ⊢ B = Base G
2 qusima.q ⊢ Q = G / 𝑠 G ~ QG N
3 qusima.p ⊢ ⊕ ˙ = LSSum ⁡ G
4 qusima.e ⊢ E = h ∈ S ⟼ ran ⁡ x ∈ h ⟼ x ⊕ ˙ N
5 qusima.f ⊢ F = x ∈ B ⟼ x G ~ QG N
6 qusima.n ⊢ φ → N ∈ NrmSGrp ⁡ G
7 qusima.h ⊢ φ → H ∈ S
8 qusima.s ⊢ φ → S ⊆ SubGrp ⁡ G
9 5 reseq1i ⊢ F ↾ H = x ∈ B ⟼ x G ~ QG N ↾ 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 ⟼ x G ~ QG N ↾ H = x ∈ H ⟼ x G ~ QG N
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 → x G ~ QG N = x ⊕ ˙ N
19 18 mpteq2dva ⊢ φ → x ∈ H ⟼ x G ~ QG N = x ∈ H ⟼ x ⊕ ˙ N
20 13 19 eqtrd ⊢ φ → x ∈ B ⟼ x G ~ QG N ↾ 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 ⊢ F H = ran ⁡ F ↾ H
28 27 a1i ⊢ φ ∧ h = H → F H = ran ⁡ F ↾ H
29 23 26 28 3eqtr4d ⊢ φ ∧ h = H → ran ⁡ x ∈ h ⟼ x ⊕ ˙ N = F H
30 1 fvexi ⊢ B ∈ V
31 30 mptex ⊢ x ∈ B ⟼ x G ~ QG N ∈ V
32 5 31 eqeltri ⊢ F ∈ V
33 imaexg ⊢ F ∈ V → F H ∈ V
34 32 33 mp1i ⊢ φ → F H ∈ V
35 4 29 7 34 fvmptd2 ⊢ φ → E ⁡ H = F H