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 fovrnda 
 |-  ( ( ( ( .(+) 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 simpr 
 |-  ( ( ( .(+) 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 .(+) y ) e. Z )
26 2 eleq1d 
 |-  ( ( x e. X /\ y e. Z ) -> ( ( x ( .(+) |` ( X X. Z ) ) y ) e. Z <-> ( x .(+) y ) e. Z ) )
27 26 ralbidva 
 |-  ( x e. X -> ( A. y e. Z ( x ( .(+) |` ( X X. Z ) ) y ) e. Z <-> A. y e. Z ( x .(+) y ) e. Z ) )
28 27 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 )
29 25 28 sylibr 
 |-  ( ( ( .(+) 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 )
30 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 ) )
31 24 29 30 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 )
32 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
33 1 32 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
34 10 33 syl 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( 0g ` G ) e. X )
35 ovres 
 |-  ( ( ( 0g ` G ) e. X /\ z e. Z ) -> ( ( 0g ` G ) ( .(+) |` ( X X. Z ) ) z ) = ( ( 0g ` G ) .(+) z ) )
36 34 35 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 ) )
37 simpll 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ Z C_ Y ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> .(+) e. ( G GrpAct Y ) )
38 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 )
39 32 gagrpid 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ z e. Y ) -> ( ( 0g ` G ) .(+) z ) = z )
40 37 38 39 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 )
41 36 40 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 )
42 37 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 ) )
43 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 )
44 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 )
45 38 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 )
46 eqid 
 |-  ( +g ` G ) = ( +g ` G )
47 1 46 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( u e. X /\ v e. X /\ z e. Y ) ) -> ( ( u ( +g ` G ) v ) .(+) z ) = ( u .(+) ( v .(+) z ) ) )
48 42 43 44 45 47 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 ) ) )
49 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 )
50 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 )
51 ovrspc2v 
 |-  ( ( ( v e. X /\ z e. Z ) /\ A. x e. X A. y e. Z ( x .(+) y ) e. Z ) -> ( v .(+) z ) e. Z )
52 44 49 50 51 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 )
53 ovres 
 |-  ( ( u e. X /\ ( v .(+) z ) e. Z ) -> ( u ( .(+) |` ( X X. Z ) ) ( v .(+) z ) ) = ( u .(+) ( v .(+) z ) ) )
54 43 52 53 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 ) ) )
55 48 54 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 ) ) )
56 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 )
57 1 46 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ v e. X ) -> ( u ( +g ` G ) v ) e. X )
58 56 43 44 57 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 )
59 ovres 
 |-  ( ( ( u ( +g ` G ) v ) e. X /\ z e. Z ) -> ( ( u ( +g ` G ) v ) ( .(+) |` ( X X. Z ) ) z ) = ( ( u ( +g ` G ) v ) .(+) z ) )
60 58 49 59 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 ) )
61 ovres 
 |-  ( ( v e. X /\ z e. Z ) -> ( v ( .(+) |` ( X X. Z ) ) z ) = ( v .(+) z ) )
62 44 49 61 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 ) )
63 62 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 ) ) )
64 55 60 63 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 ) ) )
65 64 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 ) ) )
66 41 65 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 ) ) ) )
67 66 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 ) ) ) )
68 31 67 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 ) ) ) ) )
69 1 46 32 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 ) ) ) ) ) )
70 16 68 69 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 ) )
71 8 70 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 ) )