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=BaseG
Assertion qusxpid ⊢G∈Grp→G~QGB=B×B

Proof

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