Step |
Hyp |
Ref |
Expression |
1 |
|
ablfac1.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
ablfac1.o |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
3 |
|
ablfac1.s |
⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
4 |
|
ablfac1.g |
⊢ ( 𝜑 → 𝐺 ∈ Abel ) |
5 |
|
ablfac1.f |
⊢ ( 𝜑 → 𝐵 ∈ Fin ) |
6 |
|
ablfac1.1 |
⊢ ( 𝜑 → 𝐴 ⊆ ℙ ) |
7 |
|
ablfac1c.d |
⊢ 𝐷 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } |
8 |
|
ablfac1.2 |
⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 ) |
9 |
|
ablfac1eu.1 |
⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝐵 ) ) |
10 |
|
ablfac1eu.2 |
⊢ ( 𝜑 → dom 𝑇 = 𝐴 ) |
11 |
|
ablfac1eu.3 |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ∈ ℕ0 ) |
12 |
|
ablfac1eu.4 |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) ) |
13 |
9
|
simpld |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑇 ) |
14 |
13 10
|
dprdf2 |
⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) ) |
15 |
14
|
ffnd |
⊢ ( 𝜑 → 𝑇 Fn 𝐴 ) |
16 |
1 2 3 4 5 6
|
ablfac1b |
⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 ) |
17 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
18 |
17
|
rabex |
⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ V |
19 |
18 3
|
dmmpti |
⊢ dom 𝑆 = 𝐴 |
20 |
19
|
a1i |
⊢ ( 𝜑 → dom 𝑆 = 𝐴 ) |
21 |
16 20
|
dprdf2 |
⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) ) |
22 |
21
|
ffnd |
⊢ ( 𝜑 → 𝑆 Fn 𝐴 ) |
23 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐵 ∈ Fin ) |
24 |
21
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
25 |
1
|
subgss |
⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑞 ) ⊆ 𝐵 ) |
26 |
24 25
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ⊆ 𝐵 ) |
27 |
23 26
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ∈ Fin ) |
28 |
14
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
29 |
1
|
subgss |
⊢ ( ( 𝑇 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑇 ‘ 𝑞 ) ⊆ 𝐵 ) |
30 |
28 29
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ⊆ 𝐵 ) |
31 |
30
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → 𝑥 ∈ 𝐵 ) |
32 |
1 2
|
odcl |
⊢ ( 𝑥 ∈ 𝐵 → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 ) |
33 |
31 32
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 ) |
34 |
33
|
nn0zd |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℤ ) |
35 |
23 30
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ∈ Fin ) |
36 |
|
hashcl |
⊢ ( ( 𝑇 ‘ 𝑞 ) ∈ Fin → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∈ ℕ0 ) |
37 |
35 36
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∈ ℕ0 ) |
38 |
37
|
nn0zd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∈ ℤ ) |
39 |
38
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∈ ℤ ) |
40 |
6
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ ℙ ) |
41 |
|
prmnn |
⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℕ ) |
42 |
40 41
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ ℕ ) |
43 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
44 |
4 43
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
45 |
1
|
grpbn0 |
⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ ) |
46 |
44 45
|
syl |
⊢ ( 𝜑 → 𝐵 ≠ ∅ ) |
47 |
|
hashnncl |
⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) ) |
48 |
5 47
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) ) |
49 |
46 48
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ ) |
50 |
49
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ ) |
51 |
40 50
|
pccld |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) |
52 |
42 51
|
nnexpcld |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ ) |
53 |
52
|
nnzd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ) |
54 |
53
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ) |
55 |
28
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑇 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
56 |
35
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑇 ‘ 𝑞 ) ∈ Fin ) |
57 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) |
58 |
2
|
odsubdvds |
⊢ ( ( ( 𝑇 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑇 ‘ 𝑞 ) ∈ Fin ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) |
59 |
55 56 57 58
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) |
60 |
|
prmz |
⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ ) |
61 |
40 60
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ ℤ ) |
62 |
11
|
nn0zd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ∈ ℤ ) |
63 |
51
|
nn0zd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℤ ) |
64 |
1
|
lagsubg |
⊢ ( ( ( 𝑇 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
65 |
28 23 64
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
66 |
12 65
|
eqbrtrrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) |
67 |
50
|
nnzd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℤ ) |
68 |
|
pcdvdsb |
⊢ ( ( 𝑞 ∈ ℙ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 ≤ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ↔ ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) ) |
69 |
40 67 11 68
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐶 ≤ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ↔ ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) ) |
70 |
66 69
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ≤ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) |
71 |
|
eluz2 |
⊢ ( ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐶 ∈ ℤ ∧ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝐶 ≤ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
72 |
62 63 70 71
|
syl3anbrc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ 𝐶 ) ) |
73 |
|
dvdsexp |
⊢ ( ( 𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ∧ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( 𝑞 ↑ 𝐶 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
74 |
61 11 72 73
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ 𝐶 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
75 |
12 74
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
76 |
75
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
77 |
34 39 54 59 76
|
dvdstrd |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 𝑇 ‘ 𝑞 ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
78 |
30 77
|
ssrabdv |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
79 |
|
id |
⊢ ( 𝑝 = 𝑞 → 𝑝 = 𝑞 ) |
80 |
|
oveq1 |
⊢ ( 𝑝 = 𝑞 → ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) = ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) |
81 |
79 80
|
oveq12d |
⊢ ( 𝑝 = 𝑞 → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
82 |
81
|
breq2d |
⊢ ( 𝑝 = 𝑞 → ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) |
83 |
82
|
rabbidv |
⊢ ( 𝑝 = 𝑞 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
84 |
83 3 18
|
fvmpt3i |
⊢ ( 𝑞 ∈ 𝐴 → ( 𝑆 ‘ 𝑞 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
85 |
84
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
86 |
78 85
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ⊆ ( 𝑆 ‘ 𝑞 ) ) |
87 |
52
|
nnnn0d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ0 ) |
88 |
|
pcdvds |
⊢ ( ( 𝑞 ∈ ℙ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
89 |
40 50 88
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
90 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐺 dom DProd 𝑇 ) |
91 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → dom 𝑇 = 𝐴 ) |
92 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐷 ⊆ 𝐴 ) |
93 |
90 91 92
|
dprdres |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑇 ) ) ) |
94 |
93
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ) |
95 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑇 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) ) |
96 |
95 92
|
fssresd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ↾ 𝐷 ) : 𝐷 ⟶ ( SubGrp ‘ 𝐺 ) ) |
97 |
96
|
fdmd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → dom ( 𝑇 ↾ 𝐷 ) = 𝐷 ) |
98 |
|
difssd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐷 ∖ { 𝑞 } ) ⊆ 𝐷 ) |
99 |
94 97 98
|
dprdres |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 dom DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ∧ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) ) |
100 |
99
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐺 dom DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) |
101 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
102 |
100 101
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
103 |
1
|
lagsubg |
⊢ ( ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
104 |
102 23 103
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
105 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
106 |
105
|
subg0cl |
⊢ ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) |
107 |
102 106
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) |
108 |
107
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ≠ ∅ ) |
109 |
1
|
dprdssv |
⊢ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ⊆ 𝐵 |
110 |
|
ssfi |
⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ⊆ 𝐵 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ Fin ) |
111 |
23 109 110
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ Fin ) |
112 |
|
hashnncl |
⊢ ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ∈ Fin → ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℕ ↔ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ≠ ∅ ) ) |
113 |
111 112
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℕ ↔ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ≠ ∅ ) ) |
114 |
108 113
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℕ ) |
115 |
114
|
nnzd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℤ ) |
116 |
|
id |
⊢ ( 𝑥 = 𝑞 → 𝑥 = 𝑞 ) |
117 |
|
sneq |
⊢ ( 𝑥 = 𝑞 → { 𝑥 } = { 𝑞 } ) |
118 |
117
|
difeq2d |
⊢ ( 𝑥 = 𝑞 → ( 𝐷 ∖ { 𝑥 } ) = ( 𝐷 ∖ { 𝑞 } ) ) |
119 |
118
|
reseq2d |
⊢ ( 𝑥 = 𝑞 → ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) = ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) |
120 |
119
|
oveq2d |
⊢ ( 𝑥 = 𝑞 → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) = ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) |
121 |
120
|
fveq2d |
⊢ ( 𝑥 = 𝑞 → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) ) = ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) |
122 |
116 121
|
breq12d |
⊢ ( 𝑥 = 𝑞 → ( 𝑥 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) ) ↔ 𝑞 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ) |
123 |
122
|
notbid |
⊢ ( 𝑥 = 𝑞 → ( ¬ 𝑥 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) ) ↔ ¬ 𝑞 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ) |
124 |
|
eqid |
⊢ ( 𝑝 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑦 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) = ( 𝑝 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑦 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) |
125 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → 𝐺 ∈ Abel ) |
126 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → 𝐵 ∈ Fin ) |
127 |
7
|
ssrab3 |
⊢ 𝐷 ⊆ ℙ |
128 |
127
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → 𝐷 ⊆ ℙ ) |
129 |
|
ssidd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → 𝐷 ⊆ 𝐷 ) |
130 |
13 10 8
|
dprdres |
⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑇 ) ) ) |
131 |
130
|
simpld |
⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ) |
132 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) → ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
133 |
131 132
|
syl |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
134 |
|
difssd |
⊢ ( 𝜑 → ( 𝐴 ∖ 𝐷 ) ⊆ 𝐴 ) |
135 |
13 10 134
|
dprdres |
⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ⊆ ( 𝐺 DProd 𝑇 ) ) ) |
136 |
135
|
simpld |
⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) |
137 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) → ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
138 |
136 137
|
syl |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
139 |
|
difss |
⊢ ( 𝐴 ∖ 𝐷 ) ⊆ 𝐴 |
140 |
|
fssres |
⊢ ( ( 𝑇 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∖ 𝐷 ) ⊆ 𝐴 ) → ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) : ( 𝐴 ∖ 𝐷 ) ⟶ ( SubGrp ‘ 𝐺 ) ) |
141 |
14 139 140
|
sylancl |
⊢ ( 𝜑 → ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) : ( 𝐴 ∖ 𝐷 ) ⟶ ( SubGrp ‘ 𝐺 ) ) |
142 |
141
|
fdmd |
⊢ ( 𝜑 → dom ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) = ( 𝐴 ∖ 𝐷 ) ) |
143 |
|
fvres |
⊢ ( 𝑞 ∈ ( 𝐴 ∖ 𝐷 ) → ( ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ‘ 𝑞 ) = ( 𝑇 ‘ 𝑞 ) ) |
144 |
143
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 𝐴 ∖ 𝐷 ) ) → ( ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ‘ 𝑞 ) = ( 𝑇 ‘ 𝑞 ) ) |
145 |
|
eldif |
⊢ ( 𝑞 ∈ ( 𝐴 ∖ 𝐷 ) ↔ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) |
146 |
35
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝑇 ‘ 𝑞 ) ∈ Fin ) |
147 |
105
|
subg0cl |
⊢ ( ( 𝑇 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑇 ‘ 𝑞 ) ) |
148 |
28 147
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑇 ‘ 𝑞 ) ) |
149 |
148
|
snssd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { ( 0g ‘ 𝐺 ) } ⊆ ( 𝑇 ‘ 𝑞 ) ) |
150 |
149
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → { ( 0g ‘ 𝐺 ) } ⊆ ( 𝑇 ‘ 𝑞 ) ) |
151 |
|
fvex |
⊢ ( 0g ‘ 𝐺 ) ∈ V |
152 |
|
hashsng |
⊢ ( ( 0g ‘ 𝐺 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 ) |
153 |
151 152
|
ax-mp |
⊢ ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = 1 |
154 |
12
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) ) |
155 |
40
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝐶 ∈ ℕ ) → 𝑞 ∈ ℙ ) |
156 |
|
iddvdsexp |
⊢ ( ( 𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝑞 ∥ ( 𝑞 ↑ 𝐶 ) ) |
157 |
61 156
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝐶 ∈ ℕ ) → 𝑞 ∥ ( 𝑞 ↑ 𝐶 ) ) |
158 |
66
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝐶 ∈ ℕ ) → ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) |
159 |
12 38
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ 𝐶 ) ∈ ℤ ) |
160 |
|
dvdstr |
⊢ ( ( 𝑞 ∈ ℤ ∧ ( 𝑞 ↑ 𝐶 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) → ( ( 𝑞 ∥ ( 𝑞 ↑ 𝐶 ) ∧ ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) → 𝑞 ∥ ( ♯ ‘ 𝐵 ) ) ) |
161 |
61 159 67 160
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑞 ∥ ( 𝑞 ↑ 𝐶 ) ∧ ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) → 𝑞 ∥ ( ♯ ‘ 𝐵 ) ) ) |
162 |
161
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝐶 ∈ ℕ ) → ( ( 𝑞 ∥ ( 𝑞 ↑ 𝐶 ) ∧ ( 𝑞 ↑ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) → 𝑞 ∥ ( ♯ ‘ 𝐵 ) ) ) |
163 |
157 158 162
|
mp2and |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝐶 ∈ ℕ ) → 𝑞 ∥ ( ♯ ‘ 𝐵 ) ) |
164 |
|
breq1 |
⊢ ( 𝑤 = 𝑞 → ( 𝑤 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑞 ∥ ( ♯ ‘ 𝐵 ) ) ) |
165 |
164 7
|
elrab2 |
⊢ ( 𝑞 ∈ 𝐷 ↔ ( 𝑞 ∈ ℙ ∧ 𝑞 ∥ ( ♯ ‘ 𝐵 ) ) ) |
166 |
155 163 165
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝐶 ∈ ℕ ) → 𝑞 ∈ 𝐷 ) |
167 |
166
|
ex |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐶 ∈ ℕ → 𝑞 ∈ 𝐷 ) ) |
168 |
167
|
con3d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ ) ) |
169 |
168
|
impr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ¬ 𝐶 ∈ ℕ ) |
170 |
11
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → 𝐶 ∈ ℕ0 ) |
171 |
|
elnn0 |
⊢ ( 𝐶 ∈ ℕ0 ↔ ( 𝐶 ∈ ℕ ∨ 𝐶 = 0 ) ) |
172 |
170 171
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝐶 ∈ ℕ ∨ 𝐶 = 0 ) ) |
173 |
172
|
ord |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ¬ 𝐶 ∈ ℕ → 𝐶 = 0 ) ) |
174 |
169 173
|
mpd |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → 𝐶 = 0 ) |
175 |
174
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝑞 ↑ 𝐶 ) = ( 𝑞 ↑ 0 ) ) |
176 |
42
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → 𝑞 ∈ ℕ ) |
177 |
176
|
nncnd |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → 𝑞 ∈ ℂ ) |
178 |
177
|
exp0d |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝑞 ↑ 0 ) = 1 ) |
179 |
154 175 178
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = 1 ) |
180 |
153 179
|
eqtr4id |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) |
181 |
|
snfi |
⊢ { ( 0g ‘ 𝐺 ) } ∈ Fin |
182 |
|
hashen |
⊢ ( ( { ( 0g ‘ 𝐺 ) } ∈ Fin ∧ ( 𝑇 ‘ 𝑞 ) ∈ Fin ) → ( ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ↔ { ( 0g ‘ 𝐺 ) } ≈ ( 𝑇 ‘ 𝑞 ) ) ) |
183 |
181 146 182
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ( ♯ ‘ { ( 0g ‘ 𝐺 ) } ) = ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ↔ { ( 0g ‘ 𝐺 ) } ≈ ( 𝑇 ‘ 𝑞 ) ) ) |
184 |
180 183
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → { ( 0g ‘ 𝐺 ) } ≈ ( 𝑇 ‘ 𝑞 ) ) |
185 |
|
fisseneq |
⊢ ( ( ( 𝑇 ‘ 𝑞 ) ∈ Fin ∧ { ( 0g ‘ 𝐺 ) } ⊆ ( 𝑇 ‘ 𝑞 ) ∧ { ( 0g ‘ 𝐺 ) } ≈ ( 𝑇 ‘ 𝑞 ) ) → { ( 0g ‘ 𝐺 ) } = ( 𝑇 ‘ 𝑞 ) ) |
186 |
146 150 184 185
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → { ( 0g ‘ 𝐺 ) } = ( 𝑇 ‘ 𝑞 ) ) |
187 |
105
|
subg0cl |
⊢ ( ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
188 |
133 187
|
syl |
⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
189 |
188
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 0g ‘ 𝐺 ) ∈ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
190 |
189
|
snssd |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → { ( 0g ‘ 𝐺 ) } ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
191 |
186 190
|
eqsstrrd |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝑇 ‘ 𝑞 ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
192 |
145 191
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 𝐴 ∖ 𝐷 ) ) → ( 𝑇 ‘ 𝑞 ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
193 |
144 192
|
eqsstrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( 𝐴 ∖ 𝐷 ) ) → ( ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ‘ 𝑞 ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
194 |
136 142 133 193
|
dprdlub |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
195 |
|
eqid |
⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 ) |
196 |
195
|
lsmss2 |
⊢ ( ( ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) → ( ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
197 |
133 138 194 196
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ) = ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) |
198 |
|
disjdif |
⊢ ( 𝐷 ∩ ( 𝐴 ∖ 𝐷 ) ) = ∅ |
199 |
198
|
a1i |
⊢ ( 𝜑 → ( 𝐷 ∩ ( 𝐴 ∖ 𝐷 ) ) = ∅ ) |
200 |
|
undif2 |
⊢ ( 𝐷 ∪ ( 𝐴 ∖ 𝐷 ) ) = ( 𝐷 ∪ 𝐴 ) |
201 |
|
ssequn1 |
⊢ ( 𝐷 ⊆ 𝐴 ↔ ( 𝐷 ∪ 𝐴 ) = 𝐴 ) |
202 |
8 201
|
sylib |
⊢ ( 𝜑 → ( 𝐷 ∪ 𝐴 ) = 𝐴 ) |
203 |
200 202
|
eqtr2id |
⊢ ( 𝜑 → 𝐴 = ( 𝐷 ∪ ( 𝐴 ∖ 𝐷 ) ) ) |
204 |
14 199 203 195 13
|
dprdsplit |
⊢ ( 𝜑 → ( 𝐺 DProd 𝑇 ) = ( ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ) ) |
205 |
9
|
simprd |
⊢ ( 𝜑 → ( 𝐺 DProd 𝑇 ) = 𝐵 ) |
206 |
204 205
|
eqtr3d |
⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑇 ↾ ( 𝐴 ∖ 𝐷 ) ) ) ) = 𝐵 ) |
207 |
197 206
|
eqtr3d |
⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) = 𝐵 ) |
208 |
131 207
|
jca |
⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) = 𝐵 ) ) |
209 |
208
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → ( 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) = 𝐵 ) ) |
210 |
14 8
|
fssresd |
⊢ ( 𝜑 → ( 𝑇 ↾ 𝐷 ) : 𝐷 ⟶ ( SubGrp ‘ 𝐺 ) ) |
211 |
210
|
fdmd |
⊢ ( 𝜑 → dom ( 𝑇 ↾ 𝐷 ) = 𝐷 ) |
212 |
211
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → dom ( 𝑇 ↾ 𝐷 ) = 𝐷 ) |
213 |
8
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐷 ) → 𝑞 ∈ 𝐴 ) |
214 |
213 11
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐷 ) → 𝐶 ∈ ℕ0 ) |
215 |
214
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) ∧ 𝑞 ∈ 𝐷 ) → 𝐶 ∈ ℕ0 ) |
216 |
|
fvres |
⊢ ( 𝑞 ∈ 𝐷 → ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) = ( 𝑇 ‘ 𝑞 ) ) |
217 |
216
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐷 ) → ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) = ( 𝑇 ‘ 𝑞 ) ) |
218 |
217
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐷 ) → ( ♯ ‘ ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) ) = ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) |
219 |
213 12
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐷 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) ) |
220 |
218 219
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐷 ) → ( ♯ ‘ ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) ) |
221 |
220
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) ∧ 𝑞 ∈ 𝐷 ) → ( ♯ ‘ ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) ) |
222 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → 𝑥 ∈ ℙ ) |
223 |
|
fzfid |
⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐵 ) ) ∈ Fin ) |
224 |
|
prmnn |
⊢ ( 𝑤 ∈ ℙ → 𝑤 ∈ ℕ ) |
225 |
224
|
3ad2ant2 |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑤 ∈ ℕ ) |
226 |
|
prmz |
⊢ ( 𝑤 ∈ ℙ → 𝑤 ∈ ℤ ) |
227 |
|
dvdsle |
⊢ ( ( 𝑤 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑤 ∥ ( ♯ ‘ 𝐵 ) → 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) ) |
228 |
226 49 227
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ) → ( 𝑤 ∥ ( ♯ ‘ 𝐵 ) → 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) ) |
229 |
228
|
3impia |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) |
230 |
49
|
nnzd |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ ) |
231 |
230
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ ) |
232 |
|
fznn |
⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( 𝑤 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( 𝑤 ∈ ℕ ∧ 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) ) ) |
233 |
231 232
|
syl |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑤 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( 𝑤 ∈ ℕ ∧ 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) ) ) |
234 |
225 229 233
|
mpbir2and |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑤 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) |
235 |
234
|
rabssdv |
⊢ ( 𝜑 → { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) |
236 |
7 235
|
eqsstrid |
⊢ ( 𝜑 → 𝐷 ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) |
237 |
223 236
|
ssfid |
⊢ ( 𝜑 → 𝐷 ∈ Fin ) |
238 |
237
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → 𝐷 ∈ Fin ) |
239 |
1 2 124 125 126 128 7 129 209 212 215 221 222 238
|
ablfac1eulem |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℙ ) → ¬ 𝑥 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) ) ) |
240 |
239
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℙ ¬ 𝑥 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) ) ) |
241 |
240
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ∀ 𝑥 ∈ ℙ ¬ 𝑥 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑥 } ) ) ) ) ) |
242 |
123 241 40
|
rspcdva |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ¬ 𝑞 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) |
243 |
|
coprm |
⊢ ( ( 𝑞 ∈ ℙ ∧ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℤ ) → ( ¬ 𝑞 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ↔ ( 𝑞 gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) ) |
244 |
40 115 243
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ∥ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ↔ ( 𝑞 gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) ) |
245 |
242 244
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) |
246 |
|
rpexp1i |
⊢ ( ( 𝑞 ∈ ℤ ∧ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℤ ∧ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) → ( ( 𝑞 gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) ) |
247 |
61 115 51 246
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑞 gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) ) |
248 |
245 247
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) |
249 |
|
coprmdvds2 |
⊢ ( ( ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) ∧ ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = 1 ) → ( ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) ) |
250 |
53 115 67 248 249
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) ) |
251 |
89 104 250
|
mp2and |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) |
252 |
|
eqid |
⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 ) |
253 |
|
inss1 |
⊢ ( 𝐷 ∩ { 𝑞 } ) ⊆ 𝐷 |
254 |
253
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐷 ∩ { 𝑞 } ) ⊆ 𝐷 ) |
255 |
94 97 254
|
dprdres |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 dom DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ∧ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ⊆ ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) ) ) |
256 |
255
|
simpld |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐺 dom DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) |
257 |
|
dprdsubg |
⊢ ( 𝐺 dom DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
258 |
256 257
|
syl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
259 |
|
inass |
⊢ ( ( 𝐷 ∩ { 𝑞 } ) ∩ ( 𝐷 ∖ { 𝑞 } ) ) = ( 𝐷 ∩ ( { 𝑞 } ∩ ( 𝐷 ∖ { 𝑞 } ) ) ) |
260 |
|
disjdif |
⊢ ( { 𝑞 } ∩ ( 𝐷 ∖ { 𝑞 } ) ) = ∅ |
261 |
260
|
ineq2i |
⊢ ( 𝐷 ∩ ( { 𝑞 } ∩ ( 𝐷 ∖ { 𝑞 } ) ) ) = ( 𝐷 ∩ ∅ ) |
262 |
|
in0 |
⊢ ( 𝐷 ∩ ∅ ) = ∅ |
263 |
259 261 262
|
3eqtri |
⊢ ( ( 𝐷 ∩ { 𝑞 } ) ∩ ( 𝐷 ∖ { 𝑞 } ) ) = ∅ |
264 |
263
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝐷 ∩ { 𝑞 } ) ∩ ( 𝐷 ∖ { 𝑞 } ) ) = ∅ ) |
265 |
94 97 254 98 264 105
|
dprddisj2 |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ∩ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) |
266 |
94 97 254 98 264 252
|
dprdcntz2 |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) |
267 |
1
|
dprdssv |
⊢ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ⊆ 𝐵 |
268 |
|
ssfi |
⊢ ( ( 𝐵 ∈ Fin ∧ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ⊆ 𝐵 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ∈ Fin ) |
269 |
23 267 268
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ∈ Fin ) |
270 |
195 105 252 258 102 265 266 269 111
|
lsmhash |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ) |
271 |
|
inundif |
⊢ ( ( 𝐷 ∩ { 𝑞 } ) ∪ ( 𝐷 ∖ { 𝑞 } ) ) = 𝐷 |
272 |
271
|
eqcomi |
⊢ 𝐷 = ( ( 𝐷 ∩ { 𝑞 } ) ∪ ( 𝐷 ∖ { 𝑞 } ) ) |
273 |
272
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐷 = ( ( 𝐷 ∩ { 𝑞 } ) ∪ ( 𝐷 ∖ { 𝑞 } ) ) ) |
274 |
96 264 273 195 94
|
dprdsplit |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) = ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) |
275 |
207
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( 𝑇 ↾ 𝐷 ) ) = 𝐵 ) |
276 |
274 275
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) = 𝐵 ) |
277 |
276
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = ( ♯ ‘ 𝐵 ) ) |
278 |
|
snssi |
⊢ ( 𝑞 ∈ 𝐷 → { 𝑞 } ⊆ 𝐷 ) |
279 |
278
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → { 𝑞 } ⊆ 𝐷 ) |
280 |
|
sseqin2 |
⊢ ( { 𝑞 } ⊆ 𝐷 ↔ ( 𝐷 ∩ { 𝑞 } ) = { 𝑞 } ) |
281 |
279 280
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → ( 𝐷 ∩ { 𝑞 } ) = { 𝑞 } ) |
282 |
281
|
reseq2d |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) = ( ( 𝑇 ↾ 𝐷 ) ↾ { 𝑞 } ) ) |
283 |
282
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) = ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ { 𝑞 } ) ) ) |
284 |
94
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → 𝐺 dom DProd ( 𝑇 ↾ 𝐷 ) ) |
285 |
211
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → dom ( 𝑇 ↾ 𝐷 ) = 𝐷 ) |
286 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → 𝑞 ∈ 𝐷 ) |
287 |
284 285 286
|
dpjlem |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ { 𝑞 } ) ) = ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) ) |
288 |
216
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → ( ( 𝑇 ↾ 𝐷 ) ‘ 𝑞 ) = ( 𝑇 ‘ 𝑞 ) ) |
289 |
283 287 288
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐷 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) = ( 𝑇 ‘ 𝑞 ) ) |
290 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ¬ 𝑞 ∈ 𝐷 ) |
291 |
|
disjsn |
⊢ ( ( 𝐷 ∩ { 𝑞 } ) = ∅ ↔ ¬ 𝑞 ∈ 𝐷 ) |
292 |
290 291
|
sylibr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝐷 ∩ { 𝑞 } ) = ∅ ) |
293 |
292
|
reseq2d |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) = ( ( 𝑇 ↾ 𝐷 ) ↾ ∅ ) ) |
294 |
|
res0 |
⊢ ( ( 𝑇 ↾ 𝐷 ) ↾ ∅ ) = ∅ |
295 |
293 294
|
eqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) = ∅ ) |
296 |
295
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) = ( 𝐺 DProd ∅ ) ) |
297 |
105
|
dprd0 |
⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) ) |
298 |
44 297
|
syl |
⊢ ( 𝜑 → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) ) |
299 |
298
|
simprd |
⊢ ( 𝜑 → ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) |
300 |
299
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) |
301 |
296 300 186
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷 ) ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) = ( 𝑇 ‘ 𝑞 ) ) |
302 |
301
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ ¬ 𝑞 ∈ 𝐷 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) = ( 𝑇 ‘ 𝑞 ) ) |
303 |
289 302
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) = ( 𝑇 ‘ 𝑞 ) ) |
304 |
303
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ) = ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) |
305 |
304
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∩ { 𝑞 } ) ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) = ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ) |
306 |
270 277 305
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ) |
307 |
251 306
|
breqtrd |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ∥ ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ) |
308 |
114
|
nnne0d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ≠ 0 ) |
309 |
|
dvdsmulcr |
⊢ ( ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∈ ℤ ∧ ( ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ∈ ℤ ∧ ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ≠ 0 ) ) → ( ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ∥ ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ↔ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) ) |
310 |
53 38 115 308 309
|
syl112anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ∥ ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) · ( ♯ ‘ ( 𝐺 DProd ( ( 𝑇 ↾ 𝐷 ) ↾ ( 𝐷 ∖ { 𝑞 } ) ) ) ) ) ↔ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) ) |
311 |
307 310
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) |
312 |
|
dvdseq |
⊢ ( ( ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∈ ℕ0 ∧ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ0 ) ∧ ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ∥ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∧ ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) ) ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
313 |
37 87 75 311 312
|
syl22anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
314 |
1 2 3 4 5 6
|
ablfac1a |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑞 ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
315 |
313 314
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( ♯ ‘ ( 𝑆 ‘ 𝑞 ) ) ) |
316 |
|
hashen |
⊢ ( ( ( 𝑇 ‘ 𝑞 ) ∈ Fin ∧ ( 𝑆 ‘ 𝑞 ) ∈ Fin ) → ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( ♯ ‘ ( 𝑆 ‘ 𝑞 ) ) ↔ ( 𝑇 ‘ 𝑞 ) ≈ ( 𝑆 ‘ 𝑞 ) ) ) |
317 |
35 27 316
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( ♯ ‘ ( 𝑆 ‘ 𝑞 ) ) ↔ ( 𝑇 ‘ 𝑞 ) ≈ ( 𝑆 ‘ 𝑞 ) ) ) |
318 |
315 317
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ≈ ( 𝑆 ‘ 𝑞 ) ) |
319 |
|
fisseneq |
⊢ ( ( ( 𝑆 ‘ 𝑞 ) ∈ Fin ∧ ( 𝑇 ‘ 𝑞 ) ⊆ ( 𝑆 ‘ 𝑞 ) ∧ ( 𝑇 ‘ 𝑞 ) ≈ ( 𝑆 ‘ 𝑞 ) ) → ( 𝑇 ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) |
320 |
27 86 318 319
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 ) ) |
321 |
15 22 320
|
eqfnfvd |
⊢ ( 𝜑 → 𝑇 = 𝑆 ) |