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
subgga.3 H = G 𝑠 Y
subgga.4 F = x Y , y X x + ˙ y
Assertion subgga Y SubGrp G F H GrpAct X

Proof

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