Metamath Proof Explorer


Theorem gasubg

Description: The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypothesis gasubg.1 𝐻 = ( 𝐺s 𝑆 )
Assertion gasubg ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ↾ ( 𝑆 × 𝑌 ) ) ∈ ( 𝐻 GrpAct 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gasubg.1 𝐻 = ( 𝐺s 𝑆 )
2 gaset ( ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V )
3 1 subggrp ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
4 2 3 anim12ci ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐻 ∈ Grp ∧ 𝑌 ∈ V ) )
5 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6 5 gaf ( ∈ ( 𝐺 GrpAct 𝑌 ) → : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 )
7 6 adantr ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 )
8 simpr ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
9 5 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
10 8 9 syl ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
11 xpss1 ( 𝑆 ⊆ ( Base ‘ 𝐺 ) → ( 𝑆 × 𝑌 ) ⊆ ( ( Base ‘ 𝐺 ) × 𝑌 ) )
12 10 11 syl ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑌 ) ⊆ ( ( Base ‘ 𝐺 ) × 𝑌 ) )
13 7 12 fssresd ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ↾ ( 𝑆 × 𝑌 ) ) : ( 𝑆 × 𝑌 ) ⟶ 𝑌 )
14 1 subgbas ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
15 8 14 syl ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 = ( Base ‘ 𝐻 ) )
16 15 xpeq1d ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑌 ) = ( ( Base ‘ 𝐻 ) × 𝑌 ) )
17 16 feq2d ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ↾ ( 𝑆 × 𝑌 ) ) : ( 𝑆 × 𝑌 ) ⟶ 𝑌 ↔ ( ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ) )
18 13 17 mpbid ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 )
19 8 adantr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
20 eqid ( 0g𝐺 ) = ( 0g𝐺 )
21 20 subg0cl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g𝐺 ) ∈ 𝑆 )
22 19 21 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( 0g𝐺 ) ∈ 𝑆 )
23 simpr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → 𝑥𝑌 )
24 ovres ( ( ( 0g𝐺 ) ∈ 𝑆𝑥𝑌 ) → ( ( 0g𝐺 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 0g𝐺 ) 𝑥 ) )
25 22 23 24 syl2anc ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( ( 0g𝐺 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 0g𝐺 ) 𝑥 ) )
26 1 20 subg0 ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g𝐺 ) = ( 0g𝐻 ) )
27 19 26 syl ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( 0g𝐺 ) = ( 0g𝐻 ) )
28 27 oveq1d ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( ( 0g𝐺 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 0g𝐻 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) )
29 20 gagrpid ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥𝑌 ) → ( ( 0g𝐺 ) 𝑥 ) = 𝑥 )
30 29 adantlr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( ( 0g𝐺 ) 𝑥 ) = 𝑥 )
31 25 28 30 3eqtr3d ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( ( 0g𝐻 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 )
32 eqimss2 ( 𝑆 = ( Base ‘ 𝐻 ) → ( Base ‘ 𝐻 ) ⊆ 𝑆 )
33 15 32 syl ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( Base ‘ 𝐻 ) ⊆ 𝑆 )
34 33 adantr ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( Base ‘ 𝐻 ) ⊆ 𝑆 )
35 34 sselda ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → 𝑦𝑆 )
36 34 sselda ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝐻 ) ) → 𝑧𝑆 )
37 35 36 anim12dan ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑦𝑆𝑧𝑆 ) )
38 simprl ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → 𝑦𝑆 )
39 7 ad2antrr ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 )
40 9 ad3antlr ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
41 simprr ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → 𝑧𝑆 )
42 40 41 sseldd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
43 23 adantr ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → 𝑥𝑌 )
44 39 42 43 fovrnd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑧 𝑥 ) ∈ 𝑌 )
45 ovres ( ( 𝑦𝑆 ∧ ( 𝑧 𝑥 ) ∈ 𝑌 ) → ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 𝑥 ) ) = ( 𝑦 ( 𝑧 𝑥 ) ) )
46 38 44 45 syl2anc ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 𝑥 ) ) = ( 𝑦 ( 𝑧 𝑥 ) ) )
47 ovres ( ( 𝑧𝑆𝑥𝑌 ) → ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑧 𝑥 ) )
48 41 43 47 syl2anc ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑧 𝑥 ) )
49 48 oveq2d ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 𝑥 ) ) )
50 simplll ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ∈ ( 𝐺 GrpAct 𝑌 ) )
51 40 38 sseldd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
52 eqid ( +g𝐺 ) = ( +g𝐺 )
53 5 52 gaass ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥𝑌 ) ) → ( ( 𝑦 ( +g𝐺 ) 𝑧 ) 𝑥 ) = ( 𝑦 ( 𝑧 𝑥 ) ) )
54 50 51 42 43 53 syl13anc ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑦 ( +g𝐺 ) 𝑧 ) 𝑥 ) = ( 𝑦 ( 𝑧 𝑥 ) ) )
55 46 49 54 3eqtr4d ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) = ( ( 𝑦 ( +g𝐺 ) 𝑧 ) 𝑥 ) )
56 52 subgcl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦𝑆𝑧𝑆 ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ 𝑆 )
57 56 3expb ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ 𝑆 )
58 19 57 sylan ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ 𝑆 )
59 ovres ( ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ∈ 𝑆𝑥𝑌 ) → ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 𝑦 ( +g𝐺 ) 𝑧 ) 𝑥 ) )
60 58 43 59 syl2anc ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 𝑦 ( +g𝐺 ) 𝑧 ) 𝑥 ) )
61 1 52 ressplusg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g𝐺 ) = ( +g𝐻 ) )
62 61 ad3antlr ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( +g𝐺 ) = ( +g𝐻 ) )
63 62 oveqd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( 𝑦 ( +g𝐺 ) 𝑧 ) = ( 𝑦 ( +g𝐻 ) 𝑧 ) )
64 63 oveq1d ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑦 ( +g𝐺 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) )
65 55 60 64 3eqtr2rd ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) )
66 37 65 syldan ( ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝐻 ) ) ) → ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) )
67 66 ralrimivva ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) )
68 31 67 jca ( ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥𝑌 ) → ( ( ( 0g𝐻 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) )
69 68 ralrimiva ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥𝑌 ( ( ( 0g𝐻 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) )
70 18 69 jca ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥𝑌 ( ( ( 0g𝐻 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) ) )
71 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
72 eqid ( +g𝐻 ) = ( +g𝐻 )
73 eqid ( 0g𝐻 ) = ( 0g𝐻 )
74 71 72 73 isga ( ( ↾ ( 𝑆 × 𝑌 ) ) ∈ ( 𝐻 GrpAct 𝑌 ) ↔ ( ( 𝐻 ∈ Grp ∧ 𝑌 ∈ V ) ∧ ( ( ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥𝑌 ( ( ( 0g𝐻 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g𝐻 ) 𝑧 ) ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) ) ) )
75 4 70 74 sylanbrc ( ( ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ↾ ( 𝑆 × 𝑌 ) ) ∈ ( 𝐻 GrpAct 𝑌 ) )