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 𝑌 ) )