Metamath Proof Explorer


Theorem eqg0subgecsn

Description: The equivalence classes modulo the coset equivalence relation for the trivial (zero) subgroup of a group are singletons. (Contributed by AV, 26-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 eqg0subgecsn G Grp X B X R = X

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 df-ec X R = R X
6 1 2 3 4 eqg0subg G Grp R = I B
7 6 adantr G Grp X B R = I B
8 7 imaeq1d G Grp X B R X = I B X
9 snssi X B X B
10 9 adantl G Grp X B X B
11 resima2 X B I B X = I X
12 10 11 syl G Grp X B I B X = I X
13 imai I X = X
14 12 13 eqtrdi G Grp X B I B X = X
15 8 14 eqtrd G Grp X B R X = X
16 5 15 eqtrid G Grp X B X R = X