This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subgga

Description: A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009) (Proof shortened by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses subgga.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
subgga.2 ⊢ + = ( +g ‘ 𝐺 )
subgga.3 ⊢ 𝐻 = ( 𝐺 ↾s 𝑌 )
subgga.4 ⊢ 𝐹 = ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) )
Assertion subgga ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐹 ∈ ( 𝐻 GrpAct 𝑋 ) )

Proof

Step Hyp Ref Expression
1 subgga.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 subgga.2 ⊢ + = ( +g ‘ 𝐺 )
3 subgga.3 ⊢ 𝐻 = ( 𝐺 ↾s 𝑌 )
4 subgga.4 ⊢ 𝐹 = ( 𝑥 ∈ 𝑌 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) )
5 3 subggrp ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
6 1 fvexi ⊢ 𝑋 ∈ V
7 5 6 jctir ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐻 ∈ Grp ∧ 𝑋 ∈ V ) )
8 subgrcl ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
9 8 adantr ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
10 1 subgss ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 )
11 10 sselda ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
12 11 adantrr ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
13 simprr ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
14 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 + 𝑦 ) ∈ 𝑋 )
15 9 12 13 14 syl3anc ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑋 )
16 15 ralrimivva ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑋 ( 𝑥 + 𝑦 ) ∈ 𝑋 )
17 4 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑋 ( 𝑥 + 𝑦 ) ∈ 𝑋 ↔ 𝐹 : ( 𝑌 × 𝑋 ) ⟶ 𝑋 )
18 16 17 sylib ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐹 : ( 𝑌 × 𝑋 ) ⟶ 𝑋 )
19 3 subgbas ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 = ( Base ‘ 𝐻 ) )
20 19 xpeq1d ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑌 × 𝑋 ) = ( ( Base ‘ 𝐻 ) × 𝑋 ) )
21 20 feq2d ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐹 : ( 𝑌 × 𝑋 ) ⟶ 𝑋 ↔ 𝐹 : ( ( Base ‘ 𝐻 ) × 𝑋 ) ⟶ 𝑋 ) )
22 18 21 mpbid ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐹 : ( ( Base ‘ 𝐻 ) × 𝑋 ) ⟶ 𝑋 )
23 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
24 23 subg0cl ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑌 )
25 oveq12 ⊢ ( ( 𝑥 = ( 0g ‘ 𝐺 ) ∧ 𝑦 = 𝑢 ) → ( 𝑥 + 𝑦 ) = ( ( 0g ‘ 𝐺 ) + 𝑢 ) )
26 ovex ⊢ ( ( 0g ‘ 𝐺 ) + 𝑢 ) ∈ V
27 25 4 26 ovmpoa ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑌 ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) 𝐹 𝑢 ) = ( ( 0g ‘ 𝐺 ) + 𝑢 ) )
28 24 27 sylan ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) 𝐹 𝑢 ) = ( ( 0g ‘ 𝐺 ) + 𝑢 ) )
29 3 23 subg0 ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
30 29 oveq1d ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 0g ‘ 𝐺 ) 𝐹 𝑢 ) = ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) )
31 30 adantr ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) 𝐹 𝑢 ) = ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) )
32 1 2 23 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
33 8 32 sylan ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑢 ) = 𝑢 )
34 28 31 33 3eqtr3d ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) = 𝑢 )
35 8 ad2antrr ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝐺 ∈ Grp )
36 10 ad2antrr ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
37 simprl ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑣 ∈ 𝑌 )
38 36 37 sseldd ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑣 ∈ 𝑋 )
39 simprr ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑌 )
40 36 39 sseldd ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑋 )
41 simplr ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑢 ∈ 𝑋 )
42 1 2 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) ) → ( ( 𝑣 + 𝑤 ) + 𝑢 ) = ( 𝑣 + ( 𝑤 + 𝑢 ) ) )
43 35 38 40 41 42 syl13anc ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑣 + 𝑤 ) + 𝑢 ) = ( 𝑣 + ( 𝑤 + 𝑢 ) ) )
44 1 2 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑤 + 𝑢 ) ∈ 𝑋 )
45 35 40 41 44 syl3anc ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑤 + 𝑢 ) ∈ 𝑋 )
46 oveq12 ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = ( 𝑤 + 𝑢 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑣 + ( 𝑤 + 𝑢 ) ) )
47 ovex ⊢ ( 𝑣 + ( 𝑤 + 𝑢 ) ) ∈ V
48 46 4 47 ovmpoa ⊢ ( ( 𝑣 ∈ 𝑌 ∧ ( 𝑤 + 𝑢 ) ∈ 𝑋 ) → ( 𝑣 𝐹 ( 𝑤 + 𝑢 ) ) = ( 𝑣 + ( 𝑤 + 𝑢 ) ) )
49 37 45 48 syl2anc ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑣 𝐹 ( 𝑤 + 𝑢 ) ) = ( 𝑣 + ( 𝑤 + 𝑢 ) ) )
50 43 49 eqtr4d ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑣 + 𝑤 ) + 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 + 𝑢 ) ) )
51 2 subgcl ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑣 + 𝑤 ) ∈ 𝑌 )
52 51 3expb ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑣 + 𝑤 ) ∈ 𝑌 )
53 52 adantlr ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑣 + 𝑤 ) ∈ 𝑌 )
54 oveq12 ⊢ ( ( 𝑥 = ( 𝑣 + 𝑤 ) ∧ 𝑦 = 𝑢 ) → ( 𝑥 + 𝑦 ) = ( ( 𝑣 + 𝑤 ) + 𝑢 ) )
55 ovex ⊢ ( ( 𝑣 + 𝑤 ) + 𝑢 ) ∈ V
56 54 4 55 ovmpoa ⊢ ( ( ( 𝑣 + 𝑤 ) ∈ 𝑌 ∧ 𝑢 ∈ 𝑋 ) → ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( ( 𝑣 + 𝑤 ) + 𝑢 ) )
57 53 41 56 syl2anc ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( ( 𝑣 + 𝑤 ) + 𝑢 ) )
58 oveq12 ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑢 ) → ( 𝑥 + 𝑦 ) = ( 𝑤 + 𝑢 ) )
59 ovex ⊢ ( 𝑤 + 𝑢 ) ∈ V
60 58 4 59 ovmpoa ⊢ ( ( 𝑤 ∈ 𝑌 ∧ 𝑢 ∈ 𝑋 ) → ( 𝑤 𝐹 𝑢 ) = ( 𝑤 + 𝑢 ) )
61 39 41 60 syl2anc ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑤 𝐹 𝑢 ) = ( 𝑤 + 𝑢 ) )
62 61 oveq2d ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) = ( 𝑣 𝐹 ( 𝑤 + 𝑢 ) ) )
63 50 57 62 3eqtr4d ⊢ ( ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) )
64 63 ralrimivva ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ∀ 𝑣 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) )
65 3 2 ressplusg ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → + = ( +g ‘ 𝐻 ) )
66 65 oveqd ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑣 + 𝑤 ) = ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) )
67 66 oveq1d ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) )
68 67 eqeq1d ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ↔ ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) )
69 19 68 raleqbidv ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑤 ∈ 𝑌 ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) )
70 19 69 raleqbidv ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑣 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) )
71 70 biimpa ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( 𝑣 + 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) → ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) )
72 64 71 syldan ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) )
73 34 72 jca ⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑢 ∈ 𝑋 ) → ( ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) = 𝑢 ∧ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) )
74 73 ralrimiva ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑢 ∈ 𝑋 ( ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) = 𝑢 ∧ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) )
75 22 74 jca ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐹 : ( ( Base ‘ 𝐻 ) × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑢 ∈ 𝑋 ( ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) = 𝑢 ∧ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) ) )
76 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
77 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
78 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
79 76 77 78 isga ⊢ ( 𝐹 ∈ ( 𝐻 GrpAct 𝑋 ) ↔ ( ( 𝐻 ∈ Grp ∧ 𝑋 ∈ V ) ∧ ( 𝐹 : ( ( Base ‘ 𝐻 ) × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑢 ∈ 𝑋 ( ( ( 0g ‘ 𝐻 ) 𝐹 𝑢 ) = 𝑢 ∧ ∀ 𝑣 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑣 ( +g ‘ 𝐻 ) 𝑤 ) 𝐹 𝑢 ) = ( 𝑣 𝐹 ( 𝑤 𝐹 𝑢 ) ) ) ) ) )
80 7 75 79 sylanbrc ⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐹 ∈ ( 𝐻 GrpAct 𝑋 ) )