This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑋 ∈ 𝐵 ) → [ 𝑋 ] 𝑅 = { 𝑋 } )