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

Metamath Proof Explorer

Theorem qusbas2

Description: Alternate definition of the group quotient set, as the set of all cosets of the form ( { x } .(+) N ) . (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses qusbas2.1 ⊢ B = Base G
qusbas2.2 ⊢ ⊕ ˙ = LSSum ⁡ G
qusbas2.3 ⊢ φ ∧ x ∈ B → N ∈ SubGrp ⁡ G
Assertion qusbas2 ⊢ φ → B / G ~ QG N = ran ⁡ x ∈ B ⟼ x ⊕ ˙ N

Proof

Step Hyp Ref Expression
1 qusbas2.1 ⊢ B = Base G
2 qusbas2.2 ⊢ ⊕ ˙ = LSSum ⁡ G
3 qusbas2.3 ⊢ φ ∧ x ∈ B → N ∈ SubGrp ⁡ G
4 df-qs ⊢ B / G ~ QG N = y | ∃ x ∈ B y = x G ~ QG N
5 eqid ⊢ x ∈ B ⟼ x G ~ QG N = x ∈ B ⟼ x G ~ QG N
6 5 rnmpt ⊢ ran ⁡ x ∈ B ⟼ x G ~ QG N = y | ∃ x ∈ B y = x G ~ QG N
7 4 6 eqtr4i ⊢ B / G ~ QG N = ran ⁡ x ∈ B ⟼ x G ~ QG N
8 simpr ⊢ φ ∧ x ∈ B → x ∈ B
9 1 2 3 8 quslsm ⊢ φ ∧ x ∈ B → x G ~ QG N = x ⊕ ˙ N
10 9 mpteq2dva ⊢ φ → x ∈ B ⟼ x G ~ QG N = x ∈ B ⟼ x ⊕ ˙ N
11 10 rneqd ⊢ φ → ran ⁡ x ∈ B ⟼ x G ~ QG N = ran ⁡ x ∈ B ⟼ x ⊕ ˙ N
12 7 11 eqtrid ⊢ φ → B / G ~ QG N = ran ⁡ x ∈ B ⟼ x ⊕ ˙ N