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