Metamath Proof Explorer

Theorem gastacos

Description: Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses gasta.1 
|- X = ( Base ` G )
gasta.2 
|- H = { u e. X | ( u .(+) A ) = A }
orbsta.r 
|- .~ = ( G ~QG H )
Assertion gastacos 
|- ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( B .~ C <-> ( B .(+) A ) = ( C .(+) A ) ) )

Proof

Step Hyp Ref Expression
1 gasta.1 
 |-  X = ( Base ` G )
2 gasta.2 
 |-  H = { u e. X | ( u .(+) A ) = A }
3 orbsta.r 
 |-  .~ = ( G ~QG H )
4 1 2 gastacl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> H e. ( SubGrp ` G ) )
5 4 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> H e. ( SubGrp ` G ) )
6 subgrcl 
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
7 5 6 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> G e. Grp )
8 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
9 5 8 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> H C_ X )
10 eqid 
 |-  ( invg ` G ) = ( invg ` G )
11 eqid 
 |-  ( +g ` G ) = ( +g ` G )
12 1 10 11 3 eqgval 
 |-  ( ( G e. Grp /\ H C_ X ) -> ( B .~ C <-> ( B e. X /\ C e. X /\ ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H ) ) )
13 7 9 12 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( B .~ C <-> ( B e. X /\ C e. X /\ ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H ) ) )
14 df-3an 
 |-  ( ( B e. X /\ C e. X /\ ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H ) <-> ( ( B e. X /\ C e. X ) /\ ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H ) )
15 13 14 bitrdi 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( B .~ C <-> ( ( B e. X /\ C e. X ) /\ ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H ) ) )
16 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( B e. X /\ C e. X ) )
17 16 biantrurd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H <-> ( ( B e. X /\ C e. X ) /\ ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H ) ) )
18 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> .(+) e. ( G GrpAct Y ) )
19 simprl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> B e. X )
20 1 10 grpinvcl 
 |-  ( ( G e. Grp /\ B e. X ) -> ( ( invg ` G ) ` B ) e. X )
21 7 19 20 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( invg ` G ) ` B ) e. X )
22 simprr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> C e. X )
23 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> A e. Y )
24 1 11 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( ( ( invg ` G ) ` B ) e. X /\ C e. X /\ A e. Y ) ) -> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = ( ( ( invg ` G ) ` B ) .(+) ( C .(+) A ) ) )
25 18 21 22 23 24 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = ( ( ( invg ` G ) ` B ) .(+) ( C .(+) A ) ) )
26 25 eqeq1d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = A <-> ( ( ( invg ` G ) ` B ) .(+) ( C .(+) A ) ) = A ) )
27 1 11 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` B ) e. X /\ C e. X ) -> ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. X )
28 7 21 22 27 syl3anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. X )
29 oveq1 
 |-  ( u = ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) -> ( u .(+) A ) = ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) )
30 29 eqeq1d 
 |-  ( u = ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) -> ( ( u .(+) A ) = A <-> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = A ) )
31 30 2 elrab2 
 |-  ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H <-> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. X /\ ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = A ) )
32 31 baib 
 |-  ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. X -> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H <-> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = A ) )
33 28 32 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H <-> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) .(+) A ) = A ) )
34 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
35 18 34 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> .(+) : ( X X. Y ) --> Y )
36 35 22 23 fovrnd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( C .(+) A ) e. Y )
37 1 10 gacan 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( B e. X /\ A e. Y /\ ( C .(+) A ) e. Y ) ) -> ( ( B .(+) A ) = ( C .(+) A ) <-> ( ( ( invg ` G ) ` B ) .(+) ( C .(+) A ) ) = A ) )
38 18 19 23 36 37 syl13anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( B .(+) A ) = ( C .(+) A ) <-> ( ( ( invg ` G ) ` B ) .(+) ( C .(+) A ) ) = A ) )
39 26 33 38 3bitr4d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( ( ( ( invg ` G ) ` B ) ( +g ` G ) C ) e. H <-> ( B .(+) A ) = ( C .(+) A ) ) )
40 15 17 39 3bitr2d 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) /\ ( B e. X /\ C e. X ) ) -> ( B .~ C <-> ( B .(+) A ) = ( C .(+) A ) ) )