Metamath Proof Explorer


Theorem sylow3lem2

Description: Lemma for sylow3 , first part. The stabilizer of a given Sylow subgroup K in the group action .(+) acting on all of G is the normalizer N_G(K). (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x X = Base G
sylow3.g φ G Grp
sylow3.xf φ X Fin
sylow3.p φ P
sylow3lem1.a + ˙ = + G
sylow3lem1.d - ˙ = - G
sylow3lem1.m ˙ = x X , y P pSyl G ran z y x + ˙ z - ˙ x
sylow3lem2.k φ K P pSyl G
sylow3lem2.h H = u X | u ˙ K = K
sylow3lem2.n N = x X | y X x + ˙ y K y + ˙ x K
Assertion sylow3lem2 φ H = N

Proof

Step Hyp Ref Expression
1 sylow3.x X = Base G
2 sylow3.g φ G Grp
3 sylow3.xf φ X Fin
4 sylow3.p φ P
5 sylow3lem1.a + ˙ = + G
6 sylow3lem1.d - ˙ = - G
7 sylow3lem1.m ˙ = x X , y P pSyl G ran z y x + ˙ z - ˙ x
8 sylow3lem2.k φ K P pSyl G
9 sylow3lem2.h H = u X | u ˙ K = K
10 sylow3lem2.n N = x X | y X x + ˙ y K y + ˙ x K
11 10 ssrab3 N X
12 sseqin2 N X X N = N
13 11 12 mpbi X N = N
14 simpr φ u X u X
15 8 adantr φ u X K P pSyl G
16 mptexg K P pSyl G z K u + ˙ z - ˙ u V
17 rnexg z K u + ˙ z - ˙ u V ran z K u + ˙ z - ˙ u V
18 15 16 17 3syl φ u X ran z K u + ˙ z - ˙ u V
19 simpr x = u y = K y = K
20 simpl x = u y = K x = u
21 20 oveq1d x = u y = K x + ˙ z = u + ˙ z
22 21 20 oveq12d x = u y = K x + ˙ z - ˙ x = u + ˙ z - ˙ u
23 19 22 mpteq12dv x = u y = K z y x + ˙ z - ˙ x = z K u + ˙ z - ˙ u
24 23 rneqd x = u y = K ran z y x + ˙ z - ˙ x = ran z K u + ˙ z - ˙ u
25 24 7 ovmpoga u X K P pSyl G ran z K u + ˙ z - ˙ u V u ˙ K = ran z K u + ˙ z - ˙ u
26 14 15 18 25 syl3anc φ u X u ˙ K = ran z K u + ˙ z - ˙ u
27 26 adantr φ u X u N u ˙ K = ran z K u + ˙ z - ˙ u
28 slwsubg K P pSyl G K SubGrp G
29 8 28 syl φ K SubGrp G
30 29 adantr φ u X K SubGrp G
31 eqid z K u + ˙ z - ˙ u = z K u + ˙ z - ˙ u
32 1 5 6 31 10 conjnmz K SubGrp G u N K = ran z K u + ˙ z - ˙ u
33 30 32 sylan φ u X u N K = ran z K u + ˙ z - ˙ u
34 27 33 eqtr4d φ u X u N u ˙ K = K
35 simplr φ u X u ˙ K = K u X
36 simprl φ u X u ˙ K = K w X u ˙ K = K
37 26 adantr φ u X u ˙ K = K w X u ˙ K = ran z K u + ˙ z - ˙ u
38 36 37 eqtr3d φ u X u ˙ K = K w X K = ran z K u + ˙ z - ˙ u
39 38 eleq2d φ u X u ˙ K = K w X u + ˙ w K u + ˙ w ran z K u + ˙ z - ˙ u
40 ovex u + ˙ w V
41 eqeq1 v = u + ˙ w v = u + ˙ z - ˙ u u + ˙ w = u + ˙ z - ˙ u
42 41 rexbidv v = u + ˙ w z K v = u + ˙ z - ˙ u z K u + ˙ w = u + ˙ z - ˙ u
43 31 rnmpt ran z K u + ˙ z - ˙ u = v | z K v = u + ˙ z - ˙ u
44 40 42 43 elab2 u + ˙ w ran z K u + ˙ z - ˙ u z K u + ˙ w = u + ˙ z - ˙ u
45 simprr φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u u + ˙ w = u + ˙ z - ˙ u
46 2 ad3antrrr φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u G Grp
47 simpllr φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u u X
48 1 subgss K SubGrp G K X
49 29 48 syl φ K X
50 49 ad3antrrr φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u K X
51 simprl φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u z K
52 50 51 sseldd φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u z X
53 1 5 6 grpaddsubass G Grp u X z X u X u + ˙ z - ˙ u = u + ˙ z - ˙ u
54 46 47 52 47 53 syl13anc φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u u + ˙ z - ˙ u = u + ˙ z - ˙ u
55 45 54 eqtr2d φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u u + ˙ z - ˙ u = u + ˙ w
56 1 6 grpsubcl G Grp z X u X z - ˙ u X
57 46 52 47 56 syl3anc φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u z - ˙ u X
58 simplrr φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u w X
59 1 5 grplcan G Grp z - ˙ u X w X u X u + ˙ z - ˙ u = u + ˙ w z - ˙ u = w
60 46 57 58 47 59 syl13anc φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u u + ˙ z - ˙ u = u + ˙ w z - ˙ u = w
61 55 60 mpbid φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u z - ˙ u = w
62 1 5 6 grpsubadd G Grp z X u X w X z - ˙ u = w w + ˙ u = z
63 46 52 47 58 62 syl13anc φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u z - ˙ u = w w + ˙ u = z
64 61 63 mpbid φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u w + ˙ u = z
65 64 51 eqeltrd φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u w + ˙ u K
66 65 rexlimdvaa φ u X u ˙ K = K w X z K u + ˙ w = u + ˙ z - ˙ u w + ˙ u K
67 44 66 syl5bi φ u X u ˙ K = K w X u + ˙ w ran z K u + ˙ z - ˙ u w + ˙ u K
68 simpr φ u X u ˙ K = K w X w + ˙ u K w + ˙ u K
69 oveq2 z = w + ˙ u u + ˙ z = u + ˙ w + ˙ u
70 69 oveq1d z = w + ˙ u u + ˙ z - ˙ u = u + ˙ w + ˙ u - ˙ u
71 ovex u + ˙ w + ˙ u - ˙ u V
72 70 31 71 fvmpt w + ˙ u K z K u + ˙ z - ˙ u w + ˙ u = u + ˙ w + ˙ u - ˙ u
73 68 72 syl φ u X u ˙ K = K w X w + ˙ u K z K u + ˙ z - ˙ u w + ˙ u = u + ˙ w + ˙ u - ˙ u
74 2 ad3antrrr φ u X u ˙ K = K w X w + ˙ u K G Grp
75 simpllr φ u X u ˙ K = K w X w + ˙ u K u X
76 simplrr φ u X u ˙ K = K w X w + ˙ u K w X
77 1 5 grpass G Grp u X w X u X u + ˙ w + ˙ u = u + ˙ w + ˙ u
78 74 75 76 75 77 syl13anc φ u X u ˙ K = K w X w + ˙ u K u + ˙ w + ˙ u = u + ˙ w + ˙ u
79 78 oveq1d φ u X u ˙ K = K w X w + ˙ u K u + ˙ w + ˙ u - ˙ u = u + ˙ w + ˙ u - ˙ u
80 1 5 grpcl G Grp u X w X u + ˙ w X
81 74 75 76 80 syl3anc φ u X u ˙ K = K w X w + ˙ u K u + ˙ w X
82 1 5 6 grppncan G Grp u + ˙ w X u X u + ˙ w + ˙ u - ˙ u = u + ˙ w
83 74 81 75 82 syl3anc φ u X u ˙ K = K w X w + ˙ u K u + ˙ w + ˙ u - ˙ u = u + ˙ w
84 73 79 83 3eqtr2d φ u X u ˙ K = K w X w + ˙ u K z K u + ˙ z - ˙ u w + ˙ u = u + ˙ w
85 ovex u + ˙ z - ˙ u V
86 85 31 fnmpti z K u + ˙ z - ˙ u Fn K
87 fnfvelrn z K u + ˙ z - ˙ u Fn K w + ˙ u K z K u + ˙ z - ˙ u w + ˙ u ran z K u + ˙ z - ˙ u
88 86 68 87 sylancr φ u X u ˙ K = K w X w + ˙ u K z K u + ˙ z - ˙ u w + ˙ u ran z K u + ˙ z - ˙ u
89 84 88 eqeltrrd φ u X u ˙ K = K w X w + ˙ u K u + ˙ w ran z K u + ˙ z - ˙ u
90 89 ex φ u X u ˙ K = K w X w + ˙ u K u + ˙ w ran z K u + ˙ z - ˙ u
91 67 90 impbid φ u X u ˙ K = K w X u + ˙ w ran z K u + ˙ z - ˙ u w + ˙ u K
92 39 91 bitrd φ u X u ˙ K = K w X u + ˙ w K w + ˙ u K
93 92 anassrs φ u X u ˙ K = K w X u + ˙ w K w + ˙ u K
94 93 ralrimiva φ u X u ˙ K = K w X u + ˙ w K w + ˙ u K
95 10 elnmz u N u X w X u + ˙ w K w + ˙ u K
96 35 94 95 sylanbrc φ u X u ˙ K = K u N
97 34 96 impbida φ u X u N u ˙ K = K
98 97 rabbi2dva φ X N = u X | u ˙ K = K
99 13 98 eqtr3id φ N = u X | u ˙ K = K
100 9 99 eqtr4id φ H = N