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 ‘ 𝑈 ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )