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 fovcdmda ⊢ ⊕ ˙ ∈ 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 2 eleq1d ⊢ x ∈ X ∧ y ∈ Z → x ⊕ ˙ ↾ X × Z y ∈ Z ↔ x ⊕ ˙ y ∈ Z
26 25 ralbidva ⊢ x ∈ X → ∀ y ∈ Z x ⊕ ˙ ↾ X × Z y ∈ Z ↔ ∀ y ∈ Z x ⊕ ˙ y ∈ Z
27 26 ralbiia ⊢ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ ↾ X × Z y ∈ Z ↔ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z
28 27 bilanri ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z → ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ ↾ X × Z y ∈ Z
29 ffnov ⊢ ⊕ ˙ ↾ X × Z : X × Z ⟶ Z ↔ ⊕ ˙ ↾ X × Z Fn X × Z ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ ↾ X × Z y ∈ Z
30 24 28 29 sylanbrc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z → ⊕ ˙ ↾ X × Z : X × Z ⟶ Z
31 eqid ⊢ 0 G = 0 G
32 1 31 grpidcl ⊢ G ∈ Grp → 0 G ∈ X
33 10 32 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z → 0 G ∈ X
34 ovres ⊢ 0 G ∈ X ∧ z ∈ Z → 0 G ⊕ ˙ ↾ X × Z z = 0 G ⊕ ˙ z
35 33 34 sylan ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z → 0 G ⊕ ˙ ↾ X × Z z = 0 G ⊕ ˙ z
36 simpll ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z → ⊕ ˙ ∈ G GrpAct Y
37 20 sselda ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z → z ∈ Y
38 31 gagrpid ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ Y → 0 G ⊕ ˙ z = z
39 36 37 38 syl2an2r ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z → 0 G ⊕ ˙ z = z
40 35 39 eqtrd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z → 0 G ⊕ ˙ ↾ X × Z z = z
41 36 ad2antrr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → ⊕ ˙ ∈ G GrpAct Y
42 simprl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → u ∈ X
43 simprr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → v ∈ X
44 37 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → z ∈ Y
45 eqid ⊢ + G = + G
46 1 45 gaass ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ u ∈ X ∧ v ∈ X ∧ z ∈ Y → u + G v ⊕ ˙ z = u ⊕ ˙ v ⊕ ˙ z
47 41 42 43 44 46 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
48 simplr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → z ∈ Z
49 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
50 ovrspc2v ⊢ v ∈ X ∧ z ∈ Z ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z → v ⊕ ˙ z ∈ Z
51 43 48 49 50 syl21anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → v ⊕ ˙ z ∈ Z
52 ovres ⊢ u ∈ X ∧ v ⊕ ˙ z ∈ Z → u ⊕ ˙ ↾ X × Z v ⊕ ˙ z = u ⊕ ˙ v ⊕ ˙ z
53 42 51 52 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
54 47 53 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
55 10 ad2antrr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → G ∈ Grp
56 1 45 grpcl ⊢ G ∈ Grp ∧ u ∈ X ∧ v ∈ X → u + G v ∈ X
57 55 42 43 56 syl3anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z ∧ z ∈ Z ∧ u ∈ X ∧ v ∈ X → u + G v ∈ X
58 ovres ⊢ u + G v ∈ X ∧ z ∈ Z → u + G v ⊕ ˙ ↾ X × Z z = u + G v ⊕ ˙ z
59 57 48 58 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
60 ovres ⊢ v ∈ X ∧ z ∈ Z → v ⊕ ˙ ↾ X × Z z = v ⊕ ˙ z
61 43 48 60 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
62 61 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
63 54 59 62 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
64 63 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
65 40 64 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
66 65 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
67 30 66 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
68 1 45 31 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
69 16 67 68 sylanbrc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y ∧ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z → ⊕ ˙ ↾ X × Z ∈ G GrpAct Z
70 8 69 impbida ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ Z ⊆ Y → ⊕ ˙ ↾ X × Z ∈ G GrpAct Z ↔ ∀ x ∈ X ∀ y ∈ Z x ⊕ ˙ y ∈ Z