MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gass Structured version   Visualization version   GIF version

Theorem gass 18091
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.)
Hypothesis
Ref Expression
gass.1 𝑋 = (Base‘𝐺)
Assertion
Ref Expression
gass (( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) → (( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍))
Distinct variable groups:   𝑥,𝑦,𝐺   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑥,𝑍,𝑦   𝑥, ,𝑦

Proof of Theorem gass
Dummy variables 𝑣 𝑢 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovres 7065 . . . . 5 ((𝑥𝑋𝑦𝑍) → (𝑥( ↾ (𝑋 × 𝑍))𝑦) = (𝑥 𝑦))
21adantl 475 . . . 4 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥𝑋𝑦𝑍)) → (𝑥( ↾ (𝑋 × 𝑍))𝑦) = (𝑥 𝑦))
3 gass.1 . . . . . . 7 𝑋 = (Base‘𝐺)
43gaf 18085 . . . . . 6 (( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) → ( ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍)
54adantl 475 . . . . 5 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) → ( ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍)
65fovrnda 7070 . . . 4 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥𝑋𝑦𝑍)) → (𝑥( ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍)
72, 6eqeltrrd 2907 . . 3 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥𝑋𝑦𝑍)) → (𝑥 𝑦) ∈ 𝑍)
87ralrimivva 3180 . 2 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) → ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍)
9 gagrp 18082 . . . . 5 ( ∈ (𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp)
109ad2antrr 717 . . . 4 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → 𝐺 ∈ Grp)
11 gaset 18083 . . . . . . 7 ( ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V)
1211adantr 474 . . . . . 6 (( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) → 𝑌 ∈ V)
13 simpr 479 . . . . . 6 (( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) → 𝑍𝑌)
1412, 13ssexd 5032 . . . . 5 (( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) → 𝑍 ∈ V)
1514adantr 474 . . . 4 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → 𝑍 ∈ V)
1610, 15jca 507 . . 3 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → (𝐺 ∈ Grp ∧ 𝑍 ∈ V))
173gaf 18085 . . . . . . . 8 ( ∈ (𝐺 GrpAct 𝑌) → :(𝑋 × 𝑌)⟶𝑌)
1817ad2antrr 717 . . . . . . 7 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → :(𝑋 × 𝑌)⟶𝑌)
1918ffnd 6283 . . . . . 6 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → Fn (𝑋 × 𝑌))
20 simplr 785 . . . . . . 7 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → 𝑍𝑌)
21 xpss2 5366 . . . . . . 7 (𝑍𝑌 → (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌))
2220, 21syl 17 . . . . . 6 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌))
23 fnssres 6241 . . . . . 6 (( Fn (𝑋 × 𝑌) ∧ (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌)) → ( ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍))
2419, 22, 23syl2anc 579 . . . . 5 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ( ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍))
25 simpr 479 . . . . . 6 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍)
261eleq1d 2891 . . . . . . . 8 ((𝑥𝑋𝑦𝑍) → ((𝑥( ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ (𝑥 𝑦) ∈ 𝑍))
2726ralbidva 3194 . . . . . . 7 (𝑥𝑋 → (∀𝑦𝑍 (𝑥( ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ ∀𝑦𝑍 (𝑥 𝑦) ∈ 𝑍))
2827ralbiia 3188 . . . . . 6 (∀𝑥𝑋𝑦𝑍 (𝑥( ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍)
2925, 28sylibr 226 . . . . 5 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ∀𝑥𝑋𝑦𝑍 (𝑥( ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍)
30 ffnov 7029 . . . . 5 (( ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ↔ (( ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥( ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍))
3124, 29, 30sylanbrc 578 . . . 4 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ( ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍)
32 eqid 2825 . . . . . . . . . 10 (0g𝐺) = (0g𝐺)
333, 32grpidcl 17811 . . . . . . . . 9 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
3410, 33syl 17 . . . . . . . 8 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → (0g𝐺) ∈ 𝑋)
35 ovres 7065 . . . . . . . 8 (((0g𝐺) ∈ 𝑋𝑧𝑍) → ((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = ((0g𝐺) 𝑧))
3634, 35sylan 575 . . . . . . 7 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) → ((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = ((0g𝐺) 𝑧))
3720sselda 3827 . . . . . . . 8 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) → 𝑧𝑌)
38 simpll 783 . . . . . . . . 9 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ∈ (𝐺 GrpAct 𝑌))
3932gagrpid 18084 . . . . . . . . 9 (( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑧𝑌) → ((0g𝐺) 𝑧) = 𝑧)
4038, 39sylan 575 . . . . . . . 8 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑌) → ((0g𝐺) 𝑧) = 𝑧)
4137, 40syldan 585 . . . . . . 7 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) → ((0g𝐺) 𝑧) = 𝑧)
4236, 41eqtrd 2861 . . . . . 6 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) → ((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = 𝑧)
4338ad2antrr 717 . . . . . . . . . 10 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → ∈ (𝐺 GrpAct 𝑌))
44 simprl 787 . . . . . . . . . 10 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → 𝑢𝑋)
45 simprr 789 . . . . . . . . . 10 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → 𝑣𝑋)
4637adantr 474 . . . . . . . . . 10 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → 𝑧𝑌)
47 eqid 2825 . . . . . . . . . . 11 (+g𝐺) = (+g𝐺)
483, 47gaass 18087 . . . . . . . . . 10 (( ∈ (𝐺 GrpAct 𝑌) ∧ (𝑢𝑋𝑣𝑋𝑧𝑌)) → ((𝑢(+g𝐺)𝑣) 𝑧) = (𝑢 (𝑣 𝑧)))
4943, 44, 45, 46, 48syl13anc 1495 . . . . . . . . 9 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → ((𝑢(+g𝐺)𝑣) 𝑧) = (𝑢 (𝑣 𝑧)))
50 simplr 785 . . . . . . . . . . 11 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → 𝑧𝑍)
51 simpllr 793 . . . . . . . . . . 11 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍)
52 ovrspc2v 6936 . . . . . . . . . . 11 (((𝑣𝑋𝑧𝑍) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → (𝑣 𝑧) ∈ 𝑍)
5345, 50, 51, 52syl21anc 871 . . . . . . . . . 10 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → (𝑣 𝑧) ∈ 𝑍)
54 ovres 7065 . . . . . . . . . 10 ((𝑢𝑋 ∧ (𝑣 𝑧) ∈ 𝑍) → (𝑢( ↾ (𝑋 × 𝑍))(𝑣 𝑧)) = (𝑢 (𝑣 𝑧)))
5544, 53, 54syl2anc 579 . . . . . . . . 9 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → (𝑢( ↾ (𝑋 × 𝑍))(𝑣 𝑧)) = (𝑢 (𝑣 𝑧)))
5649, 55eqtr4d 2864 . . . . . . . 8 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → ((𝑢(+g𝐺)𝑣) 𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣 𝑧)))
5710ad2antrr 717 . . . . . . . . . 10 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → 𝐺 ∈ Grp)
583, 47grpcl 17791 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑣𝑋) → (𝑢(+g𝐺)𝑣) ∈ 𝑋)
5957, 44, 45, 58syl3anc 1494 . . . . . . . . 9 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → (𝑢(+g𝐺)𝑣) ∈ 𝑋)
60 ovres 7065 . . . . . . . . 9 (((𝑢(+g𝐺)𝑣) ∈ 𝑋𝑧𝑍) → ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = ((𝑢(+g𝐺)𝑣) 𝑧))
6159, 50, 60syl2anc 579 . . . . . . . 8 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = ((𝑢(+g𝐺)𝑣) 𝑧))
62 ovres 7065 . . . . . . . . . 10 ((𝑣𝑋𝑧𝑍) → (𝑣( ↾ (𝑋 × 𝑍))𝑧) = (𝑣 𝑧))
6345, 50, 62syl2anc 579 . . . . . . . . 9 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → (𝑣( ↾ (𝑋 × 𝑍))𝑧) = (𝑣 𝑧))
6463oveq2d 6926 . . . . . . . 8 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧)) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣 𝑧)))
6556, 61, 643eqtr4d 2871 . . . . . . 7 ((((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) ∧ (𝑢𝑋𝑣𝑋)) → ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧)))
6665ralrimivva 3180 . . . . . 6 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) → ∀𝑢𝑋𝑣𝑋 ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧)))
6742, 66jca 507 . . . . 5 (((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) ∧ 𝑧𝑍) → (((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢𝑋𝑣𝑋 ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧))))
6867ralrimiva 3175 . . . 4 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ∀𝑧𝑍 (((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢𝑋𝑣𝑋 ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧))))
6931, 68jca 507 . . 3 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → (( ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ∧ ∀𝑧𝑍 (((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢𝑋𝑣𝑋 ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧)))))
703, 47, 32isga 18081 . . 3 (( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ((𝐺 ∈ Grp ∧ 𝑍 ∈ V) ∧ (( ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ∧ ∀𝑧𝑍 (((0g𝐺)( ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢𝑋𝑣𝑋 ((𝑢(+g𝐺)𝑣)( ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ↾ (𝑋 × 𝑍))(𝑣( ↾ (𝑋 × 𝑍))𝑧))))))
7116, 69, 70sylanbrc 578 . 2 ((( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) ∧ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍) → ( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍))
728, 71impbida 835 1 (( ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍𝑌) → (( ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥𝑋𝑦𝑍 (𝑥 𝑦) ∈ 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1656  wcel 2164  wral 3117  Vcvv 3414  wss 3798   × cxp 5344  cres 5348   Fn wfn 6122  wf 6123  cfv 6127  (class class class)co 6910  Basecbs 16229  +gcplusg 16312  0gc0g 16460  Grpcgrp 17783   GrpAct cga 18079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-fv 6135  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-map 8129  df-0g 16462  df-mgm 17602  df-sgrp 17644  df-mnd 17655  df-grp 17786  df-ga 18080
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator