Metamath Proof Explorer

Theorem gaid

Description: The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypothesis gaid.1 
|- X = ( Base ` G )
Assertion gaid 
|- ( ( G e. Grp /\ S e. V ) -> ( 2nd |` ( X X. S ) ) e. ( G GrpAct S ) )

Proof

Step Hyp Ref Expression
1 gaid.1 
 |-  X = ( Base ` G )
2 elex 
 |-  ( S e. V -> S e. _V )
3 2 anim2i 
 |-  ( ( G e. Grp /\ S e. V ) -> ( G e. Grp /\ S e. _V ) )
4 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
5 1 4 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
6 5 adantr 
 |-  ( ( G e. Grp /\ S e. V ) -> ( 0g ` G ) e. X )
7 ovres 
 |-  ( ( ( 0g ` G ) e. X /\ x e. S ) -> ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = ( ( 0g ` G ) 2nd x ) )
8 df-ov 
 |-  ( ( 0g ` G ) 2nd x ) = ( 2nd ` <. ( 0g ` G ) , x >. )
9 fvex 
 |-  ( 0g ` G ) e. _V
10 vex 
 |-  x e. _V
11 9 10 op2nd 
 |-  ( 2nd ` <. ( 0g ` G ) , x >. ) = x
12 8 11 eqtri 
 |-  ( ( 0g ` G ) 2nd x ) = x
13 7 12 eqtrdi 
 |-  ( ( ( 0g ` G ) e. X /\ x e. S ) -> ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = x )
14 6 13 sylan 
 |-  ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) -> ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = x )
15 simprl 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> y e. X )
16 simplr 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> x e. S )
17 ovres 
 |-  ( ( y e. X /\ x e. S ) -> ( y ( 2nd |` ( X X. S ) ) x ) = ( y 2nd x ) )
18 df-ov 
 |-  ( y 2nd x ) = ( 2nd ` <. y , x >. )
19 vex 
 |-  y e. _V
20 19 10 op2nd 
 |-  ( 2nd ` <. y , x >. ) = x
21 18 20 eqtri 
 |-  ( y 2nd x ) = x
22 17 21 eqtrdi 
 |-  ( ( y e. X /\ x e. S ) -> ( y ( 2nd |` ( X X. S ) ) x ) = x )
23 15 16 22 syl2anc 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> ( y ( 2nd |` ( X X. S ) ) x ) = x )
24 simprr 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> z e. X )
25 ovres 
 |-  ( ( z e. X /\ x e. S ) -> ( z ( 2nd |` ( X X. S ) ) x ) = ( z 2nd x ) )
26 df-ov 
 |-  ( z 2nd x ) = ( 2nd ` <. z , x >. )
27 vex 
 |-  z e. _V
28 27 10 op2nd 
 |-  ( 2nd ` <. z , x >. ) = x
29 26 28 eqtri 
 |-  ( z 2nd x ) = x
30 25 29 eqtrdi 
 |-  ( ( z e. X /\ x e. S ) -> ( z ( 2nd |` ( X X. S ) ) x ) = x )
31 24 16 30 syl2anc 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> ( z ( 2nd |` ( X X. S ) ) x ) = x )
32 31 oveq2d 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) = ( y ( 2nd |` ( X X. S ) ) x ) )
33 eqid 
 |-  ( +g ` G ) = ( +g ` G )
34 1 33 grpcl 
 |-  ( ( G e. Grp /\ y e. X /\ z e. X ) -> ( y ( +g ` G ) z ) e. X )
35 34 3expb 
 |-  ( ( G e. Grp /\ ( y e. X /\ z e. X ) ) -> ( y ( +g ` G ) z ) e. X )
36 35 ad4ant14 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> ( y ( +g ` G ) z ) e. X )
37 ovres 
 |-  ( ( ( y ( +g ` G ) z ) e. X /\ x e. S ) -> ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( ( y ( +g ` G ) z ) 2nd x ) )
38 df-ov 
 |-  ( ( y ( +g ` G ) z ) 2nd x ) = ( 2nd ` <. ( y ( +g ` G ) z ) , x >. )
39 ovex 
 |-  ( y ( +g ` G ) z ) e. _V
40 39 10 op2nd 
 |-  ( 2nd ` <. ( y ( +g ` G ) z ) , x >. ) = x
41 38 40 eqtri 
 |-  ( ( y ( +g ` G ) z ) 2nd x ) = x
42 37 41 eqtrdi 
 |-  ( ( ( y ( +g ` G ) z ) e. X /\ x e. S ) -> ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = x )
43 36 16 42 syl2anc 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = x )
44 23 32 43 3eqtr4rd 
 |-  ( ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) /\ ( y e. X /\ z e. X ) ) -> ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) )
45 44 ralrimivva 
 |-  ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) -> A. y e. X A. z e. X ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) )
46 14 45 jca 
 |-  ( ( ( G e. Grp /\ S e. V ) /\ x e. S ) -> ( ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = x /\ A. y e. X A. z e. X ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) ) )
47 46 ralrimiva 
 |-  ( ( G e. Grp /\ S e. V ) -> A. x e. S ( ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = x /\ A. y e. X A. z e. X ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) ) )
48 f2ndres 
 |-  ( 2nd |` ( X X. S ) ) : ( X X. S ) --> S
49 47 48 jctil 
 |-  ( ( G e. Grp /\ S e. V ) -> ( ( 2nd |` ( X X. S ) ) : ( X X. S ) --> S /\ A. x e. S ( ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = x /\ A. y e. X A. z e. X ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) ) ) )
50 1 33 4 isga 
 |-  ( ( 2nd |` ( X X. S ) ) e. ( G GrpAct S ) <-> ( ( G e. Grp /\ S e. _V ) /\ ( ( 2nd |` ( X X. S ) ) : ( X X. S ) --> S /\ A. x e. S ( ( ( 0g ` G ) ( 2nd |` ( X X. S ) ) x ) = x /\ A. y e. X A. z e. X ( ( y ( +g ` G ) z ) ( 2nd |` ( X X. S ) ) x ) = ( y ( 2nd |` ( X X. S ) ) ( z ( 2nd |` ( X X. S ) ) x ) ) ) ) ) )
51 3 49 50 sylanbrc 
 |-  ( ( G e. Grp /\ S e. V ) -> ( 2nd |` ( X X. S ) ) e. ( G GrpAct S ) )