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 𝐵 = ( Base ‘ 𝐺 )
Assertion qusxpid ( 𝐺 ∈ Grp → ( 𝐺 ~QG 𝐵 ) = ( 𝐵 × 𝐵 ) )

Proof

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