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 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 ( 𝜑𝑇 = 𝑆 )