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 
|- .~ = ( G ~QG S )
quselbas.u 
|- U = ( G /s .~ )
quselbas.b 
|- B = ( Base ` G )
Assertion quselbas 
|- ( ( G e. V /\ X e. W ) -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )

Proof

Step Hyp Ref Expression
1 quselbas.e 
 |-  .~ = ( G ~QG S )
2 quselbas.u 
 |-  U = ( G /s .~ )
3 quselbas.b 
 |-  B = ( Base ` G )
4 2 a1i 
 |-  ( ( G e. V /\ X e. W ) -> U = ( G /s .~ ) )
5 3 a1i 
 |-  ( ( G e. V /\ X e. W ) -> B = ( Base ` G ) )
6 1 ovexi 
 |-  .~ e. _V
7 6 a1i 
 |-  ( ( G e. V /\ X e. W ) -> .~ e. _V )
8 simpl 
 |-  ( ( G e. V /\ X e. W ) -> G e. V )
9 4 5 7 8 qusbas 
 |-  ( ( G e. V /\ X e. W ) -> ( B /. .~ ) = ( Base ` U ) )
10 9 eqcomd 
 |-  ( ( G e. V /\ X e. W ) -> ( Base ` U ) = ( B /. .~ ) )
11 10 eleq2d 
 |-  ( ( G e. V /\ X e. W ) -> ( X e. ( Base ` U ) <-> X e. ( B /. .~ ) ) )
12 elqsg 
 |-  ( X e. W -> ( X e. ( B /. .~ ) <-> E. x e. B X = [ x ] .~ ) )
13 12 adantl 
 |-  ( ( G e. V /\ X e. W ) -> ( X e. ( B /. .~ ) <-> E. x e. B X = [ x ] .~ ) )
14 11 13 bitrd 
 |-  ( ( G e. V /\ X e. W ) -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )