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

Metamath Proof Explorer

Theorem quselbas

Description: Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025)

Ref Expression
Hypotheses quselbas.e ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
quselbas.u ⊢ 𝑈 = ( 𝐺 /s ∼ )
quselbas.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion quselbas ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )

Proof

Step Hyp Ref Expression
1 quselbas.e ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
2 quselbas.u ⊢ 𝑈 = ( 𝐺 /s ∼ )
3 quselbas.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 2 a1i ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝑈 = ( 𝐺 /s ∼ ) )
5 3 a1i ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝐵 = ( Base ‘ 𝐺 ) )
6 1 ovexi ⊢ ∼ ∈ V
7 6 a1i ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ∼ ∈ V )
8 simpl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝐺 ∈ 𝑉 )
9 4 5 7 8 qusbas ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝐵 / ∼ ) = ( Base ‘ 𝑈 ) )
10 9 eqcomd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( Base ‘ 𝑈 ) = ( 𝐵 / ∼ ) )
11 10 eleq2d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ 𝑋 ∈ ( 𝐵 / ∼ ) ) )
12 elqsg ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑋 ∈ ( 𝐵 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )
13 12 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( 𝐵 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )
14 11 13 bitrd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )