Metamath Proof Explorer


Theorem eqg0subg

Description: The coset equivalence relation for the trivial (zero) subgroup of a group is the identity relation restricted to the base set of the group. (Contributed by AV, 25-Feb-2025)

Ref Expression
Hypotheses eqg0subg.0 0 ˙ = 0 G
eqg0subg.s S = 0 ˙
eqg0subg.b B = Base G
eqg0subg.r R = G ~ QG S
Assertion eqg0subg G Grp R = I B

Proof

Step Hyp Ref Expression
1 eqg0subg.0 0 ˙ = 0 G
2 eqg0subg.s S = 0 ˙
3 eqg0subg.b B = Base G
4 eqg0subg.r R = G ~ QG S
5 1 0subg G Grp 0 ˙ SubGrp G
6 3 subgss 0 ˙ SubGrp G 0 ˙ B
7 5 6 syl G Grp 0 ˙ B
8 2 7 eqsstrid G Grp S B
9 eqid inv g G = inv g G
10 eqid + G = + G
11 3 9 10 4 eqgfval G Grp S B R = x y | x y B inv g G x + G y S
12 8 11 mpdan G Grp R = x y | x y B inv g G x + G y S
13 opabresid I B = x y | x B y = x
14 simpl x B y = x x B
15 eleq1w x = y x B y B
16 15 equcoms y = x x B y B
17 16 biimpac x B y = x y B
18 simpr x B y = x y = x
19 14 17 18 jca31 x B y = x x B y B y = x
20 simpl x B y B x B
21 20 anim1i x B y B y = x x B y = x
22 21 a1i G Grp x B y B y = x x B y = x
23 19 22 impbid2 G Grp x B y = x x B y B y = x
24 simpl G Grp x B y B G Grp
25 simpr x B y B y B
26 25 adantl G Grp x B y B y B
27 20 adantl G Grp x B y B x B
28 3 9 24 26 27 grpinv11 G Grp x B y B inv g G y = inv g G x y = x
29 3 9 grpinvcl G Grp x B inv g G x B
30 29 adantrr G Grp x B y B inv g G x B
31 3 10 1 9 grpinvid2 G Grp y B inv g G x B inv g G y = inv g G x inv g G x + G y = 0 ˙
32 24 26 30 31 syl3anc G Grp x B y B inv g G y = inv g G x inv g G x + G y = 0 ˙
33 28 32 bitr3d G Grp x B y B y = x inv g G x + G y = 0 ˙
34 33 pm5.32da G Grp x B y B y = x x B y B inv g G x + G y = 0 ˙
35 vex x V
36 vex y V
37 35 36 prss x B y B x y B
38 37 a1i G Grp x B y B x y B
39 2 eleq2i inv g G x + G y S inv g G x + G y 0 ˙
40 ovex inv g G x + G y V
41 40 elsn inv g G x + G y 0 ˙ inv g G x + G y = 0 ˙
42 39 41 bitr2i inv g G x + G y = 0 ˙ inv g G x + G y S
43 42 a1i G Grp inv g G x + G y = 0 ˙ inv g G x + G y S
44 38 43 anbi12d G Grp x B y B inv g G x + G y = 0 ˙ x y B inv g G x + G y S
45 23 34 44 3bitrd G Grp x B y = x x y B inv g G x + G y S
46 45 opabbidv G Grp x y | x B y = x = x y | x y B inv g G x + G y S
47 13 46 eqtr2id G Grp x y | x y B inv g G x + G y S = I B
48 12 47 eqtrd G Grp R = I B