Step | Hyp | Ref
| Expression |
1 | | eqid 2760 |
. 2
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
2 | | eqid 2760 |
. 2
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | eqid 2760 |
. 2
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
4 | | ablfac1.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Abel) |
5 | | ablgrp 18398 |
. . 3
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | ablfac1.1 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℙ) |
8 | | nnex 11218 |
. . . . 5
⊢ ℕ
∈ V |
9 | | prmnn 15590 |
. . . . . 6
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
10 | 9 | ssriv 3748 |
. . . . 5
⊢ ℙ
⊆ ℕ |
11 | 8, 10 | ssexi 4955 |
. . . 4
⊢ ℙ
∈ V |
12 | 11 | ssex 4954 |
. . 3
⊢ (𝐴 ⊆ ℙ → 𝐴 ∈ V) |
13 | 7, 12 | syl 17 |
. 2
⊢ (𝜑 → 𝐴 ∈ V) |
14 | 4 | adantr 472 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐺 ∈ Abel) |
15 | 7 | sselda 3744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℙ) |
16 | 15, 9 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℕ) |
17 | | ablfac1.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐺) |
18 | 17 | grpbn0 17652 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
19 | 6, 18 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ≠ ∅) |
20 | | ablfac1.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ Fin) |
21 | | hashnncl 13349 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin →
((♯‘𝐵) ∈
ℕ ↔ 𝐵 ≠
∅)) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
23 | 19, 22 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) |
24 | 23 | adantr 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ) |
25 | 15, 24 | pccld 15757 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝 pCnt (♯‘𝐵)) ∈
ℕ0) |
26 | 16, 25 | nnexpcld 13224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ) |
27 | 26 | nnzd 11673 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) |
28 | | ablfac1.o |
. . . . 5
⊢ 𝑂 = (od‘𝐺) |
29 | 28, 17 | oddvdssubg 18458 |
. . . 4
⊢ ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺)) |
30 | 14, 27, 29 | syl2anc 696 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺)) |
31 | | ablfac1.s |
. . 3
⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
32 | 30, 31 | fmptd 6548 |
. 2
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
33 | 4 | adantr 472 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝐺 ∈ Abel) |
34 | 32 | adantr 472 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
35 | | simpr1 1234 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝐴) |
36 | 34, 35 | ffvelrnd 6523 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ∈ (SubGrp‘𝐺)) |
37 | | simpr2 1236 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝐴) |
38 | 34, 37 | ffvelrnd 6523 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑏) ∈ (SubGrp‘𝐺)) |
39 | 1, 33, 36, 38 | ablcntzd 18460 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑏))) |
40 | | id 22 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑎 → 𝑝 = 𝑎) |
41 | | oveq1 6820 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑎 → (𝑝 pCnt (♯‘𝐵)) = (𝑎 pCnt (♯‘𝐵))) |
42 | 40, 41 | oveq12d 6831 |
. . . . . . . . 9
⊢ (𝑝 = 𝑎 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵)))) |
43 | 42 | breq2d 4816 |
. . . . . . . 8
⊢ (𝑝 = 𝑎 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵))))) |
44 | 43 | rabbidv 3329 |
. . . . . . 7
⊢ (𝑝 = 𝑎 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}) |
45 | | fvex 6362 |
. . . . . . . . 9
⊢
(Base‘𝐺)
∈ V |
46 | 17, 45 | eqeltri 2835 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
47 | 46 | rabex 4964 |
. . . . . . 7
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V |
48 | 44, 31, 47 | fvmpt3i 6449 |
. . . . . 6
⊢ (𝑎 ∈ 𝐴 → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}) |
49 | 48 | adantl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}) |
50 | | eqimss 3798 |
. . . . 5
⊢ ((𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}) |
51 | 49, 50 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}) |
52 | 4 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐺 ∈ Abel) |
53 | | eqid 2760 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
54 | 53 | subgacs 17830 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
55 | | acsmre 16514 |
. . . . . 6
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
56 | 52, 5, 54, 55 | 4syl 19 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
57 | | df-ima 5279 |
. . . . . . 7
⊢ (𝑆 “ (𝐴 ∖ {𝑎})) = ran (𝑆 ↾ (𝐴 ∖ {𝑎})) |
58 | 7 | sselda 3744 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℙ) |
59 | 58 | ad2antrr 764 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℙ) |
60 | 23 | ad3antrrr 768 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ) |
61 | | pcdvds 15770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℙ ∧
(♯‘𝐵) ∈
ℕ) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
62 | 59, 60, 61 | syl2anc 696 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
63 | 7 | ad3antrrr 768 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℙ) |
64 | | eldifi 3875 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ∈ 𝐴) |
65 | 64 | ad2antlr 765 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ 𝐴) |
66 | 63, 65 | sseldd 3745 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℙ) |
67 | | pcdvds 15770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℙ ∧
(♯‘𝐵) ∈
ℕ) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
68 | 66, 60, 67 | syl2anc 696 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
69 | | eqid 2760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎↑(𝑎 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵))) |
70 | | eqid 2760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝐵) /
(𝑎↑(𝑎 pCnt (♯‘𝐵)))) = ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) |
71 | 17, 28, 31, 4, 20, 7, 69, 70 | ablfac1lem 18667 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧
((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1 ∧ (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))) |
72 | 71 | simp1d 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧
((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)) |
73 | 72 | simpld 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ) |
74 | 73 | ad2antrr 764 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ) |
75 | 74 | nnzd 11673 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ) |
76 | 66, 9 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℕ) |
77 | 66, 60 | pccld 15757 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝 pCnt (♯‘𝐵)) ∈
ℕ0) |
78 | 76, 77 | nnexpcld 13224 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ) |
79 | 78 | nnzd 11673 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) |
80 | 60 | nnzd 11673 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ) |
81 | | eldifsni 4466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ≠ 𝑎) |
82 | 81 | ad2antlr 765 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ≠ 𝑎) |
83 | 82 | necomd 2987 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ≠ 𝑝) |
84 | | prmrp 15626 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝)) |
85 | 59, 66, 84 | syl2anc 696 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝)) |
86 | 83, 85 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 gcd 𝑝) = 1) |
87 | | prmz 15591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ ℙ → 𝑎 ∈
ℤ) |
88 | 59, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℤ) |
89 | | prmz 15591 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
90 | 66, 89 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℤ) |
91 | 59, 60 | pccld 15757 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 pCnt (♯‘𝐵)) ∈
ℕ0) |
92 | | rpexp12i 15636 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ((𝑎 pCnt (♯‘𝐵)) ∈ ℕ0
∧ (𝑝 pCnt
(♯‘𝐵)) ∈
ℕ0)) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1)) |
93 | 88, 90, 91, 77, 92 | syl112anc 1481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1)) |
94 | 86, 93 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1) |
95 | | coprmdvds2 15570 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘𝐵) ∈
ℤ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵))) |
96 | 75, 79, 80, 94, 95 | syl31anc 1480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵))) |
97 | 62, 68, 96 | mp2and 717 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)) |
98 | 71 | simp3d 1139 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
99 | 98 | ad2antrr 764 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
100 | 97, 99 | breqtrd 4830 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
101 | 72 | simprd 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) |
102 | 101 | ad2antrr 764 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) |
103 | 102 | nnzd 11673 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) |
104 | 74 | nnne0d 11257 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0) |
105 | | dvdscmulr 15212 |
. . . . . . . . . . . . . 14
⊢ (((𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧
((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
106 | 79, 103, 75, 104, 105 | syl112anc 1481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
107 | 100, 106 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) |
108 | 17, 28 | odcl 18155 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈
ℕ0) |
109 | 108 | adantl 473 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈
ℕ0) |
110 | 109 | nn0zd 11672 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ) |
111 | | dvdstr 15220 |
. . . . . . . . . . . . 13
⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧
((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
112 | 110, 79, 103, 111 | syl3anc 1477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
113 | 107, 112 | mpan2d 712 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))) |
114 | 113 | ss2rabdv 3824 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
115 | 47 | elpw 4308 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
116 | 114, 115 | sylibr 224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
117 | 31 | reseq1i 5547 |
. . . . . . . . . 10
⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) |
118 | | difss 3880 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝑎}) ⊆ 𝐴 |
119 | | resmpt 5607 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ {𝑎}) ⊆ 𝐴 → ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})) |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
121 | 117, 120 | eqtri 2782 |
. . . . . . . . 9
⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
122 | 116, 121 | fmptd 6548 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
123 | | frn 6214 |
. . . . . . . 8
⊢ ((𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
124 | 122, 123 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
125 | 57, 124 | syl5eqss 3790 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
126 | | sspwuni 4763 |
. . . . . 6
⊢ ((𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ ∪
(𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
127 | 125, 126 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
128 | 101 | nnzd 11673 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) |
129 | 28, 17 | oddvdssubg 18458 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧
((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) |
130 | 52, 128, 129 | syl2anc 696 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) |
131 | 3 | mrcsscl 16482 |
. . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∧ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
132 | 56, 127, 130, 131 | syl3anc 1477 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) |
133 | | ss2in 3983 |
. . . 4
⊢ (((𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})) |
134 | 51, 132, 133 | syl2anc 696 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})) |
135 | | eqid 2760 |
. . . . 5
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} |
136 | | eqid 2760 |
. . . . 5
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} |
137 | 71 | simp2d 1138 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1) |
138 | | eqid 2760 |
. . . . 5
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
139 | 17, 28, 135, 136, 52, 73, 101, 137, 98, 2, 138 | ablfacrp 18665 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0g‘𝐺)} ∧ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} (LSSum‘𝐺){𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = 𝐵)) |
140 | 139 | simpld 477 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0g‘𝐺)}) |
141 | 134, 140 | sseqtrd 3782 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐴 ∖ {𝑎})))) ⊆
{(0g‘𝐺)}) |
142 | 1, 2, 3, 6, 13, 32, 39, 141 | dmdprdd 18598 |
1
⊢ (𝜑 → 𝐺dom DProd 𝑆) |