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 
|- X = ( Base ` G )
subgga.2 
|- .+ = ( +g ` G )
subgga.3 
|- H = ( G |`s Y )
subgga.4 
|- F = ( x e. Y , y e. X |-> ( x .+ y ) )
Assertion subgga 
|- ( Y e. ( SubGrp ` G ) -> F e. ( H GrpAct X ) )

Proof

Step Hyp Ref Expression
1 subgga.1 
 |-  X = ( Base ` G )
2 subgga.2 
 |-  .+ = ( +g ` G )
3 subgga.3 
 |-  H = ( G |`s Y )
4 subgga.4 
 |-  F = ( x e. Y , y e. X |-> ( x .+ y ) )
5 3 subggrp 
 |-  ( Y e. ( SubGrp ` G ) -> H e. Grp )
6 1 fvexi 
 |-  X e. _V
7 5 6 jctir 
 |-  ( Y e. ( SubGrp ` G ) -> ( H e. Grp /\ X e. _V ) )
8 subgrcl 
 |-  ( Y e. ( SubGrp ` G ) -> G e. Grp )
9 8 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x e. Y /\ y e. X ) ) -> G e. Grp )
10 1 subgss 
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
11 10 sselda 
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. Y ) -> x e. X )
12 11 adantrr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x e. Y /\ y e. X ) ) -> x e. X )
13 simprr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x e. Y /\ y e. X ) ) -> y e. X )
14 1 2 grpcl 
 |-  ( ( G e. Grp /\ x e. X /\ y e. X ) -> ( x .+ y ) e. X )
15 9 12 13 14 syl3anc 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( x e. Y /\ y e. X ) ) -> ( x .+ y ) e. X )
16 15 ralrimivva 
 |-  ( Y e. ( SubGrp ` G ) -> A. x e. Y A. y e. X ( x .+ y ) e. X )
17 4 fmpo 
 |-  ( A. x e. Y A. y e. X ( x .+ y ) e. X <-> F : ( Y X. X ) --> X )
18 16 17 sylib 
 |-  ( Y e. ( SubGrp ` G ) -> F : ( Y X. X ) --> X )
19 3 subgbas 
 |-  ( Y e. ( SubGrp ` G ) -> Y = ( Base ` H ) )
20 19 xpeq1d 
 |-  ( Y e. ( SubGrp ` G ) -> ( Y X. X ) = ( ( Base ` H ) X. X ) )
21 20 feq2d 
 |-  ( Y e. ( SubGrp ` G ) -> ( F : ( Y X. X ) --> X <-> F : ( ( Base ` H ) X. X ) --> X ) )
22 18 21 mpbid 
 |-  ( Y e. ( SubGrp ` G ) -> F : ( ( Base ` H ) X. X ) --> X )
23 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
24 23 subg0cl 
 |-  ( Y e. ( SubGrp ` G ) -> ( 0g ` G ) e. Y )
25 oveq12 
 |-  ( ( x = ( 0g ` G ) /\ y = u ) -> ( x .+ y ) = ( ( 0g ` G ) .+ u ) )
26 ovex 
 |-  ( ( 0g ` G ) .+ u ) e. _V
27 25 4 26 ovmpoa 
 |-  ( ( ( 0g ` G ) e. Y /\ u e. X ) -> ( ( 0g ` G ) F u ) = ( ( 0g ` G ) .+ u ) )
28 24 27 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> ( ( 0g ` G ) F u ) = ( ( 0g ` G ) .+ u ) )
29 3 23 subg0 
 |-  ( Y e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
30 29 oveq1d 
 |-  ( Y e. ( SubGrp ` G ) -> ( ( 0g ` G ) F u ) = ( ( 0g ` H ) F u ) )
31 30 adantr 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> ( ( 0g ` G ) F u ) = ( ( 0g ` H ) F u ) )
32 1 2 23 grplid 
 |-  ( ( G e. Grp /\ u e. X ) -> ( ( 0g ` G ) .+ u ) = u )
33 8 32 sylan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> ( ( 0g ` G ) .+ u ) = u )
34 28 31 33 3eqtr3d 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> ( ( 0g ` H ) F u ) = u )
35 8 ad2antrr 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> G e. Grp )
36 10 ad2antrr 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> Y C_ X )
37 simprl 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> v e. Y )
38 36 37 sseldd 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> v e. X )
39 simprr 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> w e. Y )
40 36 39 sseldd 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> w e. X )
41 simplr 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> u e. X )
42 1 2 grpass 
 |-  ( ( G e. Grp /\ ( v e. X /\ w e. X /\ u e. X ) ) -> ( ( v .+ w ) .+ u ) = ( v .+ ( w .+ u ) ) )
43 35 38 40 41 42 syl13anc 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( ( v .+ w ) .+ u ) = ( v .+ ( w .+ u ) ) )
44 1 2 grpcl 
 |-  ( ( G e. Grp /\ w e. X /\ u e. X ) -> ( w .+ u ) e. X )
45 35 40 41 44 syl3anc 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( w .+ u ) e. X )
46 oveq12 
 |-  ( ( x = v /\ y = ( w .+ u ) ) -> ( x .+ y ) = ( v .+ ( w .+ u ) ) )
47 ovex 
 |-  ( v .+ ( w .+ u ) ) e. _V
48 46 4 47 ovmpoa 
 |-  ( ( v e. Y /\ ( w .+ u ) e. X ) -> ( v F ( w .+ u ) ) = ( v .+ ( w .+ u ) ) )
49 37 45 48 syl2anc 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( v F ( w .+ u ) ) = ( v .+ ( w .+ u ) ) )
50 43 49 eqtr4d 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( ( v .+ w ) .+ u ) = ( v F ( w .+ u ) ) )
51 2 subgcl 
 |-  ( ( Y e. ( SubGrp ` G ) /\ v e. Y /\ w e. Y ) -> ( v .+ w ) e. Y )
52 51 3expb 
 |-  ( ( Y e. ( SubGrp ` G ) /\ ( v e. Y /\ w e. Y ) ) -> ( v .+ w ) e. Y )
53 52 adantlr 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( v .+ w ) e. Y )
54 oveq12 
 |-  ( ( x = ( v .+ w ) /\ y = u ) -> ( x .+ y ) = ( ( v .+ w ) .+ u ) )
55 ovex 
 |-  ( ( v .+ w ) .+ u ) e. _V
56 54 4 55 ovmpoa 
 |-  ( ( ( v .+ w ) e. Y /\ u e. X ) -> ( ( v .+ w ) F u ) = ( ( v .+ w ) .+ u ) )
57 53 41 56 syl2anc 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( ( v .+ w ) F u ) = ( ( v .+ w ) .+ u ) )
58 oveq12 
 |-  ( ( x = w /\ y = u ) -> ( x .+ y ) = ( w .+ u ) )
59 ovex 
 |-  ( w .+ u ) e. _V
60 58 4 59 ovmpoa 
 |-  ( ( w e. Y /\ u e. X ) -> ( w F u ) = ( w .+ u ) )
61 39 41 60 syl2anc 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( w F u ) = ( w .+ u ) )
62 61 oveq2d 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( v F ( w F u ) ) = ( v F ( w .+ u ) ) )
63 50 57 62 3eqtr4d 
 |-  ( ( ( Y e. ( SubGrp ` G ) /\ u e. X ) /\ ( v e. Y /\ w e. Y ) ) -> ( ( v .+ w ) F u ) = ( v F ( w F u ) ) )
64 63 ralrimivva 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> A. v e. Y A. w e. Y ( ( v .+ w ) F u ) = ( v F ( w F u ) ) )
65 3 2 ressplusg 
 |-  ( Y e. ( SubGrp ` G ) -> .+ = ( +g ` H ) )
66 65 oveqd 
 |-  ( Y e. ( SubGrp ` G ) -> ( v .+ w ) = ( v ( +g ` H ) w ) )
67 66 oveq1d 
 |-  ( Y e. ( SubGrp ` G ) -> ( ( v .+ w ) F u ) = ( ( v ( +g ` H ) w ) F u ) )
68 67 eqeq1d 
 |-  ( Y e. ( SubGrp ` G ) -> ( ( ( v .+ w ) F u ) = ( v F ( w F u ) ) <-> ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) )
69 19 68 raleqbidv 
 |-  ( Y e. ( SubGrp ` G ) -> ( A. w e. Y ( ( v .+ w ) F u ) = ( v F ( w F u ) ) <-> A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) )
70 19 69 raleqbidv 
 |-  ( Y e. ( SubGrp ` G ) -> ( A. v e. Y A. w e. Y ( ( v .+ w ) F u ) = ( v F ( w F u ) ) <-> A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) )
71 70 biimpa 
 |-  ( ( Y e. ( SubGrp ` G ) /\ A. v e. Y A. w e. Y ( ( v .+ w ) F u ) = ( v F ( w F u ) ) ) -> A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) )
72 64 71 syldan 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) )
73 34 72 jca 
 |-  ( ( Y e. ( SubGrp ` G ) /\ u e. X ) -> ( ( ( 0g ` H ) F u ) = u /\ A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) )
74 73 ralrimiva 
 |-  ( Y e. ( SubGrp ` G ) -> A. u e. X ( ( ( 0g ` H ) F u ) = u /\ A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) )
75 22 74 jca 
 |-  ( Y e. ( SubGrp ` G ) -> ( F : ( ( Base ` H ) X. X ) --> X /\ A. u e. X ( ( ( 0g ` H ) F u ) = u /\ A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) ) )
76 eqid 
 |-  ( Base ` H ) = ( Base ` H )
77 eqid 
 |-  ( +g ` H ) = ( +g ` H )
78 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
79 76 77 78 isga 
 |-  ( F e. ( H GrpAct X ) <-> ( ( H e. Grp /\ X e. _V ) /\ ( F : ( ( Base ` H ) X. X ) --> X /\ A. u e. X ( ( ( 0g ` H ) F u ) = u /\ A. v e. ( Base ` H ) A. w e. ( Base ` H ) ( ( v ( +g ` H ) w ) F u ) = ( v F ( w F u ) ) ) ) ) )
80 7 75 79 sylanbrc 
 |-  ( Y e. ( SubGrp ` G ) -> F e. ( H GrpAct X ) )