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 ‘ 𝑈 ) ↔ ∃ 𝑥𝐵 𝑋 = [ 𝑥 ] ) )