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