Metamath Proof Explorer

Theorem qusxpid

Description: The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024)

Ref Expression
Hypothesis qustriv.1 ⊢ B = Base G
Assertion qusxpid ⊢ G ∈ Grp → G ~ QG B = B × B

Proof

Step Hyp Ref Expression
1 qustriv.1 ⊢ B = Base G
2 1 subgid ⊢ G ∈ Grp → B ∈ SubGrp ⁡ G
3 eqid ⊢ G ~ QG B = G ~ QG B
4 1 3 eqger ⊢ B ∈ SubGrp ⁡ G → G ~ QG B Er B
5 errel ⊢ G ~ QG B Er B → Rel ⁡ G ~ QG B
6 2 4 5 3syl ⊢ G ∈ Grp → Rel ⁡ G ~ QG B
7 relxp ⊢ Rel ⁡ B × B
8 7 a1i ⊢ G ∈ Grp → Rel ⁡ B × B
9 simpl ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → G ∈ Grp
10 eqid ⊢ inv g ⁡ G = inv g ⁡ G
11 1 10 grpinvcl ⊢ G ∈ Grp ∧ x ∈ B → inv g ⁡ G ⁡ x ∈ B
12 11 adantrr ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x ∈ B
13 simprr ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → y ∈ B
14 eqid ⊢ + G = + G
15 1 14 grpcl ⊢ G ∈ Grp ∧ inv g ⁡ G ⁡ x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x + G y ∈ B
16 9 12 13 15 syl3anc ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x + G y ∈ B
17 16 ex ⊢ G ∈ Grp → x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x + G y ∈ B
18 17 pm4.71d ⊢ G ∈ Grp → x ∈ B ∧ y ∈ B ↔ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B
19 df-3an ⊢ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B ↔ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B
20 18 19 syl6rbbr ⊢ G ∈ Grp → x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B ↔ x ∈ B ∧ y ∈ B
21 ssid ⊢ B ⊆ B
22 1 10 14 3 eqgval ⊢ G ∈ Grp ∧ B ⊆ B → x G ~ QG B y ↔ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B
23 21 22 mpan2 ⊢ G ∈ Grp → x G ~ QG B y ↔ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B
24 brxp ⊢ x B × B y ↔ x ∈ B ∧ y ∈ B
25 24 a1i ⊢ G ∈ Grp → x B × B y ↔ x ∈ B ∧ y ∈ B
26 20 23 25 3bitr4d ⊢ G ∈ Grp → x G ~ QG B y ↔ x B × B y
27 6 8 26 eqbrrdv ⊢ G ∈ Grp → G ~ QG B = B × B