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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y → ⊕ ˙ ↾ X × Z ∈ G GrpAct Z ↔ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z

Proof

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