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

Metamath Proof Explorer

Theorem qusecsub

Description: Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025)

Ref Expression
Hypotheses qusecsub.x 
|- B = ( Base ` G )
qusecsub.n 
|- .- = ( -g ` G )
qusecsub.r 
|- .~ = ( G ~QG S )
Assertion qusecsub 
|- ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ = [ Y ] .~ <-> ( Y .- X ) e. S ) )

Proof

Step Hyp Ref Expression
1 qusecsub.x 
 |-  B = ( Base ` G )
2 qusecsub.n 
 |-  .- = ( -g ` G )
3 qusecsub.r 
 |-  .~ = ( G ~QG S )
4 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
5 4 anim2i 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) -> ( G e. Abel /\ S C_ B ) )
6 5 adantr 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( G e. Abel /\ S C_ B ) )
7 1 2 3 eqgabl 
 |-  ( ( G e. Abel /\ S C_ B ) -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) ) )
8 6 7 syl 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) ) )
9 1 3 eqger 
 |-  ( S e. ( SubGrp ` G ) -> .~ Er B )
10 9 ad2antlr 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> .~ Er B )
11 simprl 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> X e. B )
12 10 11 erth 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> [ X ] .~ = [ Y ] .~ ) )
13 df-3an 
 |-  ( ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) <-> ( ( X e. B /\ Y e. B ) /\ ( Y .- X ) e. S ) )
14 ibar 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( Y .- X ) e. S <-> ( ( X e. B /\ Y e. B ) /\ ( Y .- X ) e. S ) ) )
15 14 adantl 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( ( Y .- X ) e. S <-> ( ( X e. B /\ Y e. B ) /\ ( Y .- X ) e. S ) ) )
16 13 15 bitr4id 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( ( X e. B /\ Y e. B /\ ( Y .- X ) e. S ) <-> ( Y .- X ) e. S ) )
17 8 12 16 3bitr3d 
 |-  ( ( ( G e. Abel /\ S e. ( SubGrp ` G ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ = [ Y ] .~ <-> ( Y .- X ) e. S ) )