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 df-3an ⊢ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B ↔ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B
10 simpl ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → G ∈ Grp
11 eqid ⊢ inv g ⁡ G = inv g ⁡ G
12 1 11 grpinvcl ⊢ G ∈ Grp ∧ x ∈ B → inv g ⁡ G ⁡ x ∈ B
13 12 adantrr ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x ∈ B
14 simprr ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → y ∈ B
15 eqid ⊢ + G = + G
16 1 15 grpcl ⊢ G ∈ Grp ∧ inv g ⁡ G ⁡ x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x + G y ∈ B
17 10 13 14 16 syl3anc ⊢ G ∈ Grp ∧ x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x + G y ∈ B
18 17 ex ⊢ G ∈ Grp → x ∈ B ∧ y ∈ B → inv g ⁡ G ⁡ x + G y ∈ B
19 18 pm4.71d ⊢ G ∈ Grp → x ∈ B ∧ y ∈ B ↔ x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B
20 9 19 bitr4id ⊢ G ∈ Grp → x ∈ B ∧ y ∈ B ∧ inv g ⁡ G ⁡ x + G y ∈ B ↔ x ∈ B ∧ y ∈ B
21 ssid ⊢ B ⊆ B
22 1 11 15 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