Metamath Proof Explorer

Theorem gass

Description: A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypothesis gass.1 
|- X = ( Base ` G )
Assertion gass 
|- ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) -> ( ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) <-> A. x e. X A. y e. Z ( x .(+) y ) e. Z ) )

Proof

Step Hyp Ref Expression
1 gass.1 
 |-  X = ( Base ` G )
2 ovres 
 |-  ( ( x e. X /\ y e. Z ) -> ( x ( .(+) |` ( X X. Z ) ) y ) = ( x .(+) y ) )
3 2 adantl 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) ) /\ ( x e. X /\ y e. Z ) ) -> ( x ( .(+) |` ( X X. Z ) ) y ) = ( x .(+) y ) )
4 1 gaf 
 |-  ( ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) -> ( .(+) |` ( X X. Z ) ) : ( X X. Z ) --> Z )
5 4 adantl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) ) -> ( .(+) |` ( X X. Z ) ) : ( X X. Z ) --> Z )
6 5 fovcdmda 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) ) /\ ( x e. X /\ y e. Z ) ) -> ( x ( .(+) |` ( X X. Z ) ) y ) e. Z )
7 3 6 eqeltrrd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) ) /\ ( x e. X /\ y e. Z ) ) -> ( x .(+) y ) e. Z )
8 7 ralrimivva 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) ) -> A. x e. X A. y e. Z ( x .(+) y ) e. Z )
9 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
10 9 ad2antrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> G e. Grp )
11 gaset 
 |-  ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
12 11 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) -> Y e. _V )
13 simpr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) -> Z C_ Y )
14 12 13 ssexd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) -> Z e. _V )
15 14 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> Z e. _V )
16 10 15 jca 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( G e. Grp /\ Z e. _V ) )
17 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
18 17 ad2antrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> .(+) : ( X X. Y ) --> Y )
19 18 ffnd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> .(+) Fn ( X X. Y ) )
20 simplr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> Z C_ Y )
21 xpss2 
 |-  ( Z C_ Y -> ( X X. Z ) C_ ( X X. Y ) )
22 20 21 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( X X. Z ) C_ ( X X. Y ) )
23 fnssres 
 |-  ( ( .(+) Fn ( X X. Y ) /\ ( X X. Z ) C_ ( X X. Y ) ) -> ( .(+) |` ( X X. Z ) ) Fn ( X X. Z ) )
24 19 22 23 syl2anc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( .(+) |` ( X X. Z ) ) Fn ( X X. Z ) )
25 2 eleq1d 
 |-  ( ( x e. X /\ y e. Z ) -> ( ( x ( .(+) |` ( X X. Z ) ) y ) e. Z <-> ( x .(+) y ) e. Z ) )
26 25 ralbidva 
 |-  ( x e. X -> ( A. y e. Z ( x ( .(+) |` ( X X. Z ) ) y ) e. Z <-> A. y e. Z ( x .(+) y ) e. Z ) )
27 26 ralbiia 
 |-  ( A. x e. X A. y e. Z ( x ( .(+) |` ( X X. Z ) ) y ) e. Z <-> A. x e. X A. y e. Z ( x .(+) y ) e. Z )
28 27 bilanri 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> A. x e. X A. y e. Z ( x ( .(+) |` ( X X. Z ) ) y ) e. Z )
29 ffnov 
 |-  ( ( .(+) |` ( X X. Z ) ) : ( X X. Z ) --> Z <-> ( ( .(+) |` ( X X. Z ) ) Fn ( X X. Z ) /\ A. x e. X A. y e. Z ( x ( .(+) |` ( X X. Z ) ) y ) e. Z ) )
30 24 28 29 sylanbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( .(+) |` ( X X. Z ) ) : ( X X. Z ) --> Z )
31 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
32 1 31 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
33 10 32 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( 0g ` G ) e. X )
34 ovres 
 |-  ( ( ( 0g ` G ) e. X /\ z e. Z ) -> ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = ( ( 0g ` G ) .(+) z ) )
35 33 34 sylan 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) -> ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = ( ( 0g ` G ) .(+) z ) )
36 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> .(+) e. ( G GrpAct Y ) )
37 20 sselda 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) -> z e. Y )
38 31 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ z e. Y ) -> ( ( 0g ` G ) .(+) z ) = z )
39 36 37 38 syl2an2r 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) -> ( ( 0g ` G ) .(+) z ) = z )
40 35 39 eqtrd 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) -> ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = z )
41 36 ad2antrr 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> .(+) e. ( G GrpAct Y ) )
42 simprl 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> u e. X )
43 simprr 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> v e. X )
44 37 adantr 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> z e. Y )
45 eqid 
 |-  ( +g ` G ) = ( +g ` G )
46 1 45 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( u e. X /\ v e. X /\ z e. Y ) ) -> ( ( u ( +g ` G ) v ) .(+) z ) = ( u .(+) ( v .(+) z ) ) )
47 41 42 43 44 46 syl13anc 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( ( u ( +g ` G ) v ) .(+) z ) = ( u .(+) ( v .(+) z ) ) )
48 simplr 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> z e. Z )
49 simpllr 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> A. x e. X A. y e. Z ( x .(+) y ) e. Z )
50 ovrspc2v 
 |-  ( ( ( v e. X /\ z e. Z ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( v .(+) z ) e. Z )
51 43 48 49 50 syl21anc 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( v .(+) z ) e. Z )
52 ovres 
 |-  ( ( u e. X /\ ( v .(+) z ) e. Z ) -> ( u ( .(+) |` ( X X. Z ) ) ( v .(+) z ) ) = ( u .(+) ( v .(+) z ) ) )
53 42 51 52 syl2anc 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( u ( .(+) |` ( X X. Z ) ) ( v .(+) z ) ) = ( u .(+) ( v .(+) z ) ) )
54 47 53 eqtr4d 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( ( u ( +g ` G ) v ) .(+) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v .(+) z ) ) )
55 10 ad2antrr 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> G e. Grp )
56 1 45 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ v e. X ) -> ( u ( +g ` G ) v ) e. X )
57 55 42 43 56 syl3anc 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( u ( +g ` G ) v ) e. X )
58 ovres 
 |-  ( ( ( u ( +g ` G ) v ) e. X /\ z e. Z ) -> ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( ( u ( +g ` G ) v ) .(+) z ) )
59 57 48 58 syl2anc 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( ( u ( +g ` G ) v ) .(+) z ) )
60 ovres 
 |-  ( ( v e. X /\ z e. Z ) -> ( v ( .(+) |` ( X X. Z ) ) z ) = ( v .(+) z ) )
61 43 48 60 syl2anc 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( v ( .(+) |` ( X X. Z ) ) z ) = ( v .(+) z ) )
62 61 oveq2d 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) = ( u ( .(+) |` ( X X. Z ) ) ( v .(+) z ) ) )
63 54 59 62 3eqtr4d 
 |-  ( ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) /\ ( u e. X /\ v e. X ) ) -> ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) )
64 63 ralrimivva 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) -> A. u e. X A. v e. X ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) )
65 40 64 jca 
 |-  ( ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) /\ z e. Z ) -> ( ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = z /\ A. u e. X A. v e. X ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) ) )
66 65 ralrimiva 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> A. z e. Z ( ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = z /\ A. u e. X A. v e. X ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) ) )
67 30 66 jca 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( ( .(+) |` ( X X. Z ) ) : ( X X. Z ) --> Z /\ A. z e. Z ( ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = z /\ A. u e. X A. v e. X ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) ) ) )
68 1 45 31 isga 
 |-  ( ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) <-> ( ( G e. Grp /\ Z e. _V ) /\ ( ( .(+) |` ( X X. Z ) ) : ( X X. Z ) --> Z /\ A. z e. Z ( ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = z /\ A. u e. X A. v e. X ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( u ( .(+) |` ( X X. Z ) ) ( v ( .(+) |` ( X X. Z ) ) z ) ) ) ) ) )
69 16 67 68 sylanbrc 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) )
70 8 69 impbida 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) -> ( ( .(+) |` ( X X. Z ) ) e. ( G GrpAct Z ) <-> A. x e. X A. y e. Z ( x .(+) y ) e. Z ) )