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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion gaid ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) → ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ∈ ( 𝐺 GrpAct 𝑆 ) )

Proof

Step Hyp Ref Expression
1 gaid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 elex ⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
3 2 anim2i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) → ( 𝐺 ∈ Grp ∧ 𝑆 ∈ V ) )
4 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
5 1 4 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
6 5 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
7 ovres ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( ( 0g ‘ 𝐺 ) 2nd 𝑥 ) )
8 df-ov ⊢ ( ( 0g ‘ 𝐺 ) 2nd 𝑥 ) = ( 2nd ‘ ⟨ ( 0g ‘ 𝐺 ) , 𝑥 ⟩ )
9 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
10 vex ⊢ 𝑥 ∈ V
11 9 10 op2nd ⊢ ( 2nd ‘ ⟨ ( 0g ‘ 𝐺 ) , 𝑥 ⟩ ) = 𝑥
12 8 11 eqtri ⊢ ( ( 0g ‘ 𝐺 ) 2nd 𝑥 ) = 𝑥
13 7 12 eqtrdi ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
14 6 13 sylan ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
15 simprl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
16 simplr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑆 )
17 ovres ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 2nd 𝑥 ) )
18 df-ov ⊢ ( 𝑦 2nd 𝑥 ) = ( 2nd ‘ ⟨ 𝑦 , 𝑥 ⟩ )
19 vex ⊢ 𝑦 ∈ V
20 19 10 op2nd ⊢ ( 2nd ‘ ⟨ 𝑦 , 𝑥 ⟩ ) = 𝑥
21 18 20 eqtri ⊢ ( 𝑦 2nd 𝑥 ) = 𝑥
22 17 21 eqtrdi ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
23 15 16 22 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
24 simprr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
25 ovres ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑧 2nd 𝑥 ) )
26 df-ov ⊢ ( 𝑧 2nd 𝑥 ) = ( 2nd ‘ ⟨ 𝑧 , 𝑥 ⟩ )
27 vex ⊢ 𝑧 ∈ V
28 27 10 op2nd ⊢ ( 2nd ‘ ⟨ 𝑧 , 𝑥 ⟩ ) = 𝑥
29 26 28 eqtri ⊢ ( 𝑧 2nd 𝑥 ) = 𝑥
30 25 29 eqtrdi ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
31 24 16 30 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
32 31 oveq2d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) )
33 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
34 1 33 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
35 34 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
36 35 ad4ant14 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
37 ovres ⊢ ( ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) 2nd 𝑥 ) )
38 df-ov ⊢ ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) 2nd 𝑥 ) = ( 2nd ‘ ⟨ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) , 𝑥 ⟩ )
39 ovex ⊢ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ V
40 39 10 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) , 𝑥 ⟩ ) = 𝑥
41 38 40 eqtri ⊢ ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) 2nd 𝑥 ) = 𝑥
42 37 41 eqtrdi ⊢ ( ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
43 36 16 42 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 )
44 23 32 43 3eqtr4rd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) )
45 44 ralrimivva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) )
46 14 45 jca ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) ) )
47 46 ralrimiva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) → ∀ 𝑥 ∈ 𝑆 ( ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) ) )
48 f2ndres ⊢ ( 2nd ↾ ( 𝑋 × 𝑆 ) ) : ( 𝑋 × 𝑆 ) ⟶ 𝑆
49 47 48 jctil ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) → ( ( 2nd ↾ ( 𝑋 × 𝑆 ) ) : ( 𝑋 × 𝑆 ) ⟶ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) ) ) )
50 1 33 4 isga ⊢ ( ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ∈ ( 𝐺 GrpAct 𝑆 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ V ) ∧ ( ( 2nd ↾ ( 𝑋 × 𝑆 ) ) : ( 𝑋 × 𝑆 ) ⟶ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( 0g ‘ 𝐺 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) = ( 𝑦 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ( 𝑧 ( 2nd ↾ ( 𝑋 × 𝑆 ) ) 𝑥 ) ) ) ) ) )
51 3 49 50 sylanbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉 ) → ( 2nd ↾ ( 𝑋 × 𝑆 ) ) ∈ ( 𝐺 GrpAct 𝑆 ) )