Metamath Proof Explorer

Theorem ablfac1eu

Description: The factorization of ablfac1b is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to S . (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses ablfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfac1.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
ablfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac1.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
ablfac1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
ablfac1c.d ⊢ 𝐷 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
ablfac1.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
ablfac1eu.1 ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝐵 ) )
ablfac1eu.2 ⊢ ( 𝜑 → dom 𝑇 = 𝐴 )
ablfac1eu.3 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐶 ∈ ℕ0 )
ablfac1eu.4 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑇 ‘ 𝑞 ) ) = ( 𝑞 ↑ 𝐶 ) )
Assertion ablfac1eu ( 𝜑 → 𝑇 = 𝑆 )

Proof

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) )
25 1 subgss ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑞 ) ⊆ 𝐵 )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ⊆ 𝐵 )
27 23 26 ssfid ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ∈ Fin )
28 14 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑞 ) ∈ ( 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 ⊢ ( 𝜑 → 𝑇 = 𝑆 )