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 Grp S V 2 nd X × S G GrpAct S

Proof

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