Step | Hyp | Ref
| Expression |
1 | | odcau.x |
. . 3
⊢ 𝑋 = (Base‘𝐺) |
2 | | simpl1 1064 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 𝐺 ∈ Grp) |
3 | | simpl2 1065 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 𝑋 ∈ Fin) |
4 | | simpl3 1066 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 𝑃 ∈ ℙ) |
5 | | 1nn0 11308 |
. . . 4
⊢ 1 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 1 ∈
ℕ0) |
7 | | prmnn 15388 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
8 | 4, 7 | syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 𝑃 ∈ ℕ) |
9 | 8 | nncnd 11036 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 𝑃 ∈ ℂ) |
10 | 9 | exp1d 13003 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → (𝑃↑1) = 𝑃) |
11 | | simpr 477 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → 𝑃 ∥ (#‘𝑋)) |
12 | 10, 11 | eqbrtrd 4675 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → (𝑃↑1) ∥ (#‘𝑋)) |
13 | 1, 2, 3, 4, 6, 12 | sylow1 18018 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → ∃𝑠 ∈ (SubGrp‘𝐺)(#‘𝑠) = (𝑃↑1)) |
14 | 10 | eqeq2d 2632 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → ((#‘𝑠) = (𝑃↑1) ↔ (#‘𝑠) = 𝑃)) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ 𝑠 ∈ (SubGrp‘𝐺)) → ((#‘𝑠) = (𝑃↑1) ↔ (#‘𝑠) = 𝑃)) |
16 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(0g‘𝐺) ∈ V |
17 | | hashsng 13159 |
. . . . . . . . . . . 12
⊢
((0g‘𝐺) ∈ V →
(#‘{(0g‘𝐺)}) = 1) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(#‘{(0g‘𝐺)}) = 1 |
19 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → (#‘𝑠) = 𝑃) |
20 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → 𝑃 ∈ ℙ) |
21 | | prmuz2 15408 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → 𝑃 ∈
(ℤ≥‘2)) |
23 | 19, 22 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → (#‘𝑠) ∈
(ℤ≥‘2)) |
24 | | eluz2b2 11761 |
. . . . . . . . . . . . 13
⊢
((#‘𝑠) ∈
(ℤ≥‘2) ↔ ((#‘𝑠) ∈ ℕ ∧ 1 < (#‘𝑠))) |
25 | 24 | simprbi 480 |
. . . . . . . . . . . 12
⊢
((#‘𝑠) ∈
(ℤ≥‘2) → 1 < (#‘𝑠)) |
26 | 23, 25 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → 1 < (#‘𝑠)) |
27 | 18, 26 | syl5eqbr 4688 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) →
(#‘{(0g‘𝐺)}) < (#‘𝑠)) |
28 | | snfi 8038 |
. . . . . . . . . . 11
⊢
{(0g‘𝐺)} ∈ Fin |
29 | 3 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → 𝑋 ∈ Fin) |
30 | 1 | subgss 17595 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (SubGrp‘𝐺) → 𝑠 ⊆ 𝑋) |
31 | 30 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → 𝑠 ⊆ 𝑋) |
32 | | ssfi 8180 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Fin ∧ 𝑠 ⊆ 𝑋) → 𝑠 ∈ Fin) |
33 | 29, 31, 32 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → 𝑠 ∈ Fin) |
34 | | hashsdom 13170 |
. . . . . . . . . . 11
⊢
(({(0g‘𝐺)} ∈ Fin ∧ 𝑠 ∈ Fin) →
((#‘{(0g‘𝐺)}) < (#‘𝑠) ↔ {(0g‘𝐺)} ≺ 𝑠)) |
35 | 28, 33, 34 | sylancr 695 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) →
((#‘{(0g‘𝐺)}) < (#‘𝑠) ↔ {(0g‘𝐺)} ≺ 𝑠)) |
36 | 27, 35 | mpbid 222 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → {(0g‘𝐺)} ≺ 𝑠) |
37 | | sdomdif 8108 |
. . . . . . . . 9
⊢
({(0g‘𝐺)} ≺ 𝑠 → (𝑠 ∖ {(0g‘𝐺)}) ≠
∅) |
38 | 36, 37 | syl 17 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → (𝑠 ∖ {(0g‘𝐺)}) ≠
∅) |
39 | | n0 3931 |
. . . . . . . 8
⊢ ((𝑠 ∖
{(0g‘𝐺)})
≠ ∅ ↔ ∃𝑔 𝑔 ∈ (𝑠 ∖ {(0g‘𝐺)})) |
40 | 38, 39 | sylib 208 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → ∃𝑔 𝑔 ∈ (𝑠 ∖ {(0g‘𝐺)})) |
41 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝑠 ∖ {(0g‘𝐺)}) ↔ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺))) |
42 | 31 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑠 ⊆ 𝑋) |
43 | | simprrl 804 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑔 ∈ 𝑠) |
44 | 42, 43 | sseldd 3604 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑔 ∈ 𝑋) |
45 | | simprrr 805 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑔 ≠ (0g‘𝐺)) |
46 | | simprll 802 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑠 ∈ (SubGrp‘𝐺)) |
47 | 33 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑠 ∈ Fin) |
48 | | odcau.o |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑂 = (od‘𝐺) |
49 | 48 | odsubdvds 17986 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ (SubGrp‘𝐺) ∧ 𝑠 ∈ Fin ∧ 𝑔 ∈ 𝑠) → (𝑂‘𝑔) ∥ (#‘𝑠)) |
50 | 46, 47, 43, 49 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (𝑂‘𝑔) ∥ (#‘𝑠)) |
51 | | simprlr 803 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (#‘𝑠) = 𝑃) |
52 | 50, 51 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (𝑂‘𝑔) ∥ 𝑃) |
53 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑃 ∈ ℙ) |
54 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝐺 ∈ Grp) |
55 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → 𝑋 ∈ Fin) |
56 | 1, 48 | odcl2 17982 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑔 ∈ 𝑋) → (𝑂‘𝑔) ∈ ℕ) |
57 | 54, 55, 44, 56 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (𝑂‘𝑔) ∈ ℕ) |
58 | | dvdsprime 15400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧ (𝑂‘𝑔) ∈ ℕ) → ((𝑂‘𝑔) ∥ 𝑃 ↔ ((𝑂‘𝑔) = 𝑃 ∨ (𝑂‘𝑔) = 1))) |
59 | 53, 57, 58 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → ((𝑂‘𝑔) ∥ 𝑃 ↔ ((𝑂‘𝑔) = 𝑃 ∨ (𝑂‘𝑔) = 1))) |
60 | 52, 59 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → ((𝑂‘𝑔) = 𝑃 ∨ (𝑂‘𝑔) = 1)) |
61 | 60 | ord 392 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (¬ (𝑂‘𝑔) = 𝑃 → (𝑂‘𝑔) = 1)) |
62 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐺) = (0g‘𝐺) |
63 | 48, 62, 1 | odeq1 17977 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → ((𝑂‘𝑔) = 1 ↔ 𝑔 = (0g‘𝐺))) |
64 | 54, 44, 63 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → ((𝑂‘𝑔) = 1 ↔ 𝑔 = (0g‘𝐺))) |
65 | 61, 64 | sylibd 229 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (¬ (𝑂‘𝑔) = 𝑃 → 𝑔 = (0g‘𝐺))) |
66 | 65 | necon1ad 2811 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (𝑔 ≠ (0g‘𝐺) → (𝑂‘𝑔) = 𝑃)) |
67 | 45, 66 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (𝑂‘𝑔) = 𝑃) |
68 | 44, 67 | jca 554 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ ((𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃) ∧ (𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)))) → (𝑔 ∈ 𝑋 ∧ (𝑂‘𝑔) = 𝑃)) |
69 | 68 | expr 643 |
. . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → ((𝑔 ∈ 𝑠 ∧ 𝑔 ≠ (0g‘𝐺)) → (𝑔 ∈ 𝑋 ∧ (𝑂‘𝑔) = 𝑃))) |
70 | 41, 69 | syl5bi 232 |
. . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → (𝑔 ∈ (𝑠 ∖ {(0g‘𝐺)}) → (𝑔 ∈ 𝑋 ∧ (𝑂‘𝑔) = 𝑃))) |
71 | 70 | eximdv 1846 |
. . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → (∃𝑔 𝑔 ∈ (𝑠 ∖ {(0g‘𝐺)}) → ∃𝑔(𝑔 ∈ 𝑋 ∧ (𝑂‘𝑔) = 𝑃))) |
72 | 40, 71 | mpd 15 |
. . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → ∃𝑔(𝑔 ∈ 𝑋 ∧ (𝑂‘𝑔) = 𝑃)) |
73 | | df-rex 2918 |
. . . . . 6
⊢
(∃𝑔 ∈
𝑋 (𝑂‘𝑔) = 𝑃 ↔ ∃𝑔(𝑔 ∈ 𝑋 ∧ (𝑂‘𝑔) = 𝑃)) |
74 | 72, 73 | sylibr 224 |
. . . . 5
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (#‘𝑠) = 𝑃)) → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃) |
75 | 74 | expr 643 |
. . . 4
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ 𝑠 ∈ (SubGrp‘𝐺)) → ((#‘𝑠) = 𝑃 → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃)) |
76 | 15, 75 | sylbid 230 |
. . 3
⊢ ((((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) ∧ 𝑠 ∈ (SubGrp‘𝐺)) → ((#‘𝑠) = (𝑃↑1) → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃)) |
77 | 76 | rexlimdva 3031 |
. 2
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → (∃𝑠 ∈ (SubGrp‘𝐺)(#‘𝑠) = (𝑃↑1) → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃)) |
78 | 13, 77 | mpd 15 |
1
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃) |