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 = ( 0g𝐺 )
eqg0subg.s 𝑆 = { 0 }
eqg0subg.b 𝐵 = ( Base ‘ 𝐺 )
eqg0subg.r 𝑅 = ( 𝐺 ~QG 𝑆 )
Assertion eqg0subgecsn ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → [ 𝑋 ] 𝑅 = { 𝑋 } )

Proof

Step Hyp Ref Expression
1 eqg0subg.0 0 = ( 0g𝐺 )
2 eqg0subg.s 𝑆 = { 0 }
3 eqg0subg.b 𝐵 = ( Base ‘ 𝐺 )
4 eqg0subg.r 𝑅 = ( 𝐺 ~QG 𝑆 )
5 df-ec [ 𝑋 ] 𝑅 = ( 𝑅 “ { 𝑋 } )
6 1 2 3 4 eqg0subg ( 𝐺 ∈ Grp → 𝑅 = ( I ↾ 𝐵 ) )
7 6 adantr ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → 𝑅 = ( I ↾ 𝐵 ) )
8 7 imaeq1d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑅 “ { 𝑋 } ) = ( ( I ↾ 𝐵 ) “ { 𝑋 } ) )
9 snssi ( 𝑋𝐵 → { 𝑋 } ⊆ 𝐵 )
10 9 adantl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → { 𝑋 } ⊆ 𝐵 )
11 resima2 ( { 𝑋 } ⊆ 𝐵 → ( ( I ↾ 𝐵 ) “ { 𝑋 } ) = ( I “ { 𝑋 } ) )
12 10 11 syl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( I ↾ 𝐵 ) “ { 𝑋 } ) = ( I “ { 𝑋 } ) )
13 imai ( I “ { 𝑋 } ) = { 𝑋 }
14 12 13 eqtrdi ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( ( I ↾ 𝐵 ) “ { 𝑋 } ) = { 𝑋 } )
15 8 14 eqtrd ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑅 “ { 𝑋 } ) = { 𝑋 } )
16 5 15 eqtrid ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → [ 𝑋 ] 𝑅 = { 𝑋 } )