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 e. Grp -> ( G ~QG B ) = ( B X. B ) )

Proof

Step Hyp Ref Expression
1 qustriv.1 
 |-  B = ( Base ` G )
2 1 subgid 
 |-  ( G e. Grp -> B e. ( SubGrp ` G ) )
3 eqid 
 |-  ( G ~QG B ) = ( G ~QG B )
4 1 3 eqger 
 |-  ( B e. ( SubGrp ` G ) -> ( G ~QG B ) Er B )
5 errel 
 |-  ( ( G ~QG B ) Er B -> Rel ( G ~QG B ) )
6 2 4 5 3syl 
 |-  ( G e. Grp -> Rel ( G ~QG B ) )
7 relxp 
 |-  Rel ( B X. B )
8 7 a1i 
 |-  ( G e. Grp -> Rel ( B X. B ) )
9 df-3an 
 |-  ( ( x e. B /\ y e. B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) <-> ( ( x e. B /\ y e. B ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) )
10 simpl 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> G e. Grp )
11 eqid 
 |-  ( invg ` G ) = ( invg ` G )
12 1 11 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
13 12 adantrr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( invg ` G ) ` x ) e. B )
14 simprr 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> y e. B )
15 eqid 
 |-  ( +g ` G ) = ( +g ` G )
16 1 15 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` x ) e. B /\ y e. B ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B )
17 10 13 14 16 syl3anc 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B )
18 17 ex 
 |-  ( G e. Grp -> ( ( x e. B /\ y e. B ) -> ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) )
19 18 pm4.71d 
 |-  ( G e. Grp -> ( ( x e. B /\ y e. B ) <-> ( ( x e. B /\ y e. B ) /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) ) )
20 9 19 bitr4id 
 |-  ( G e. Grp -> ( ( x e. B /\ y e. B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) <-> ( x e. B /\ y e. B ) ) )
21 ssid 
 |-  B C_ B
22 1 11 15 3 eqgval 
 |-  ( ( G e. Grp /\ B C_ B ) -> ( x ( G ~QG B ) y <-> ( x e. B /\ y e. B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) ) )
23 21 22 mpan2 
 |-  ( G e. Grp -> ( x ( G ~QG B ) y <-> ( x e. B /\ y e. B /\ ( ( ( invg ` G ) ` x ) ( +g ` G ) y ) e. B ) ) )
24 brxp 
 |-  ( x ( B X. B ) y <-> ( x e. B /\ y e. B ) )
25 24 a1i 
 |-  ( G e. Grp -> ( x ( B X. B ) y <-> ( x e. B /\ y e. B ) ) )
26 20 23 25 3bitr4d 
 |-  ( G e. Grp -> ( x ( G ~QG B ) y <-> x ( B X. B ) y ) )
27 6 8 26 eqbrrdv 
 |-  ( G e. Grp -> ( G ~QG B ) = ( B X. B ) )