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

Metamath Proof Explorer

Theorem qus0subgbas

Description: The base set of a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025)

Ref Expression
Hypotheses qus0subg.0 ⊢ 0 = ( 0g ‘ 𝐺 )
qus0subg.s ⊢ 𝑆 = { 0 }
qus0subg.e ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
qus0subg.u ⊢ 𝑈 = ( 𝐺 /s ∼ )
qus0subg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion qus0subgbas ( 𝐺 ∈ Grp → ( Base ‘ 𝑈 ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )

Proof

Step Hyp Ref Expression
1 qus0subg.0 ⊢ 0 = ( 0g ‘ 𝐺 )
2 qus0subg.s ⊢ 𝑆 = { 0 }
3 qus0subg.e ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
4 qus0subg.u ⊢ 𝑈 = ( 𝐺 /s ∼ )
5 qus0subg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
6 df-qs ⊢ ( 𝐵 / ∼ ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = [ 𝑥 ] ∼ }
7 4 a1i ⊢ ( 𝐺 ∈ Grp → 𝑈 = ( 𝐺 /s ∼ ) )
8 5 a1i ⊢ ( 𝐺 ∈ Grp → 𝐵 = ( Base ‘ 𝐺 ) )
9 3 ovexi ⊢ ∼ ∈ V
10 9 a1i ⊢ ( 𝐺 ∈ Grp → ∼ ∈ V )
11 id ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
12 7 8 10 11 qusbas ⊢ ( 𝐺 ∈ Grp → ( 𝐵 / ∼ ) = ( Base ‘ 𝑈 ) )
13 1 2 5 3 eqg0subgecsn ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ∼ = { 𝑥 } )
14 13 eqeq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑢 = [ 𝑥 ] ∼ ↔ 𝑢 = { 𝑥 } ) )
15 14 rexbidva ⊢ ( 𝐺 ∈ Grp → ( ∃ 𝑥 ∈ 𝐵 𝑢 = [ 𝑥 ] ∼ ↔ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) )
16 15 abbidv ⊢ ( 𝐺 ∈ Grp → { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = [ 𝑥 ] ∼ } = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
17 6 12 16 3eqtr3a ⊢ ( 𝐺 ∈ Grp → ( Base ‘ 𝑈 ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )