MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablfac1eu Structured version   Visualization version   GIF version

Theorem ablfac1eu 19685
Description: The factorization of ablfac1b 19682 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to 𝑆. (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
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
Ref Expression
ablfac1eu (𝜑𝑇 = 𝑆)
Distinct variable groups:   𝑞,𝑝,𝑤,𝑥,𝐵   𝐷,𝑝,𝑞,𝑥   𝜑,𝑝,𝑞,𝑤,𝑥   𝑆,𝑞   𝐴,𝑝,𝑞,𝑥   𝑂,𝑝,𝑞,𝑥   𝑇,𝑞,𝑥   𝐺,𝑝,𝑞,𝑥
Allowed substitution hints:   𝐴(𝑤)   𝐶(𝑥,𝑤,𝑞,𝑝)   𝐷(𝑤)   𝑆(𝑥,𝑤,𝑝)   𝑇(𝑤,𝑝)   𝐺(𝑤)   𝑂(𝑤)

Proof of Theorem ablfac1eu
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ablfac1eu.1 . . . . 5 (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵))
21simpld 495 . . . 4 (𝜑𝐺dom DProd 𝑇)
3 ablfac1eu.2 . . . 4 (𝜑 → dom 𝑇 = 𝐴)
42, 3dprdf2 19619 . . 3 (𝜑𝑇:𝐴⟶(SubGrp‘𝐺))
54ffnd 6610 . 2 (𝜑𝑇 Fn 𝐴)
6 ablfac1.b . . . . 5 𝐵 = (Base‘𝐺)
7 ablfac1.o . . . . 5 𝑂 = (od‘𝐺)
8 ablfac1.s . . . . 5 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
9 ablfac1.g . . . . 5 (𝜑𝐺 ∈ Abel)
10 ablfac1.f . . . . 5 (𝜑𝐵 ∈ Fin)
11 ablfac1.1 . . . . 5 (𝜑𝐴 ⊆ ℙ)
126, 7, 8, 9, 10, 11ablfac1b 19682 . . . 4 (𝜑𝐺dom DProd 𝑆)
136fvexi 6797 . . . . . . 7 𝐵 ∈ V
1413rabex 5257 . . . . . 6 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
1514, 8dmmpti 6586 . . . . 5 dom 𝑆 = 𝐴
1615a1i 11 . . . 4 (𝜑 → dom 𝑆 = 𝐴)
1712, 16dprdf2 19619 . . 3 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
1817ffnd 6610 . 2 (𝜑𝑆 Fn 𝐴)
1910adantr 481 . . . 4 ((𝜑𝑞𝐴) → 𝐵 ∈ Fin)
2017ffvelrnda 6970 . . . . 5 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ (SubGrp‘𝐺))
216subgss 18765 . . . . 5 ((𝑆𝑞) ∈ (SubGrp‘𝐺) → (𝑆𝑞) ⊆ 𝐵)
2220, 21syl 17 . . . 4 ((𝜑𝑞𝐴) → (𝑆𝑞) ⊆ 𝐵)
2319, 22ssfid 9051 . . 3 ((𝜑𝑞𝐴) → (𝑆𝑞) ∈ Fin)
244ffvelrnda 6970 . . . . . 6 ((𝜑𝑞𝐴) → (𝑇𝑞) ∈ (SubGrp‘𝐺))
256subgss 18765 . . . . . 6 ((𝑇𝑞) ∈ (SubGrp‘𝐺) → (𝑇𝑞) ⊆ 𝐵)
2624, 25syl 17 . . . . 5 ((𝜑𝑞𝐴) → (𝑇𝑞) ⊆ 𝐵)
2726sselda 3922 . . . . . . . 8 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → 𝑥𝐵)
286, 7odcl 19153 . . . . . . . 8 (𝑥𝐵 → (𝑂𝑥) ∈ ℕ0)
2927, 28syl 17 . . . . . . 7 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑂𝑥) ∈ ℕ0)
3029nn0zd 12433 . . . . . 6 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑂𝑥) ∈ ℤ)
3119, 26ssfid 9051 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑇𝑞) ∈ Fin)
32 hashcl 14080 . . . . . . . . 9 ((𝑇𝑞) ∈ Fin → (♯‘(𝑇𝑞)) ∈ ℕ0)
3331, 32syl 17 . . . . . . . 8 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) ∈ ℕ0)
3433nn0zd 12433 . . . . . . 7 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) ∈ ℤ)
3534adantr 481 . . . . . 6 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (♯‘(𝑇𝑞)) ∈ ℤ)
3611sselda 3922 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝑞 ∈ ℙ)
37 prmnn 16388 . . . . . . . . . 10 (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
3836, 37syl 17 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝑞 ∈ ℕ)
39 ablgrp 19400 . . . . . . . . . . . . . 14 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
409, 39syl 17 . . . . . . . . . . . . 13 (𝜑𝐺 ∈ Grp)
416grpbn0 18617 . . . . . . . . . . . . 13 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
4240, 41syl 17 . . . . . . . . . . . 12 (𝜑𝐵 ≠ ∅)
43 hashnncl 14090 . . . . . . . . . . . . 13 (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
4410, 43syl 17 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
4542, 44mpbird 256 . . . . . . . . . . 11 (𝜑 → (♯‘𝐵) ∈ ℕ)
4645adantr 481 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘𝐵) ∈ ℕ)
4736, 46pccld 16560 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
4838, 47nnexpcld 13969 . . . . . . . 8 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ)
4948nnzd 12434 . . . . . . 7 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ)
5049adantr 481 . . . . . 6 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ)
5124adantr 481 . . . . . . 7 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑇𝑞) ∈ (SubGrp‘𝐺))
5231adantr 481 . . . . . . 7 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑇𝑞) ∈ Fin)
53 simpr 485 . . . . . . 7 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → 𝑥 ∈ (𝑇𝑞))
547odsubdvds 19185 . . . . . . 7 (((𝑇𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑂𝑥) ∥ (♯‘(𝑇𝑞)))
5551, 52, 53, 54syl3anc 1370 . . . . . 6 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑂𝑥) ∥ (♯‘(𝑇𝑞)))
56 ablfac1eu.4 . . . . . . . 8 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) = (𝑞𝐶))
57 prmz 16389 . . . . . . . . . 10 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
5836, 57syl 17 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝑞 ∈ ℤ)
59 ablfac1eu.3 . . . . . . . . 9 ((𝜑𝑞𝐴) → 𝐶 ∈ ℕ0)
6059nn0zd 12433 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝐶 ∈ ℤ)
6147nn0zd 12433 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ)
626lagsubg 18827 . . . . . . . . . . . . 13 (((𝑇𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇𝑞)) ∥ (♯‘𝐵))
6324, 19, 62syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) ∥ (♯‘𝐵))
6456, 63eqbrtrrd 5099 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑞𝐶) ∥ (♯‘𝐵))
6546nnzd 12434 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (♯‘𝐵) ∈ ℤ)
66 pcdvdsb 16579 . . . . . . . . . . . 12 ((𝑞 ∈ ℙ ∧ (♯‘𝐵) ∈ ℤ ∧ 𝐶 ∈ ℕ0) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞𝐶) ∥ (♯‘𝐵)))
6736, 65, 59, 66syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞𝐶) ∥ (♯‘𝐵)))
6864, 67mpbird 256 . . . . . . . . . 10 ((𝜑𝑞𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))
69 eluz2 12597 . . . . . . . . . 10 ((𝑞 pCnt (♯‘𝐵)) ∈ (ℤ𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))))
7060, 61, 68, 69syl3anbrc 1342 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ (ℤ𝐶))
71 dvdsexp 16046 . . . . . . . . 9 ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ∧ (𝑞 pCnt (♯‘𝐵)) ∈ (ℤ𝐶)) → (𝑞𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
7258, 59, 70, 71syl3anc 1370 . . . . . . . 8 ((𝜑𝑞𝐴) → (𝑞𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
7356, 72eqbrtrd 5097 . . . . . . 7 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
7473adantr 481 . . . . . 6 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (♯‘(𝑇𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
7530, 35, 50, 55, 74dvdstrd 16013 . . . . 5 (((𝜑𝑞𝐴) ∧ 𝑥 ∈ (𝑇𝑞)) → (𝑂𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))
7626, 75ssrabdv 4008 . . . 4 ((𝜑𝑞𝐴) → (𝑇𝑞) ⊆ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
77 id 22 . . . . . . . . 9 (𝑝 = 𝑞𝑝 = 𝑞)
78 oveq1 7291 . . . . . . . . 9 (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵)))
7977, 78oveq12d 7302 . . . . . . . 8 (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
8079breq2d 5087 . . . . . . 7 (𝑝 = 𝑞 → ((𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))))
8180rabbidv 3415 . . . . . 6 (𝑝 = 𝑞 → {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
8281, 8, 14fvmpt3i 6889 . . . . 5 (𝑞𝐴 → (𝑆𝑞) = {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
8382adantl 482 . . . 4 ((𝜑𝑞𝐴) → (𝑆𝑞) = {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))})
8476, 83sseqtrrd 3963 . . 3 ((𝜑𝑞𝐴) → (𝑇𝑞) ⊆ (𝑆𝑞))
8548nnnn0d 12302 . . . . . 6 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0)
86 pcdvds 16574 . . . . . . . . . 10 ((𝑞 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
8736, 46, 86syl2anc 584 . . . . . . . . 9 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
882adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → 𝐺dom DProd 𝑇)
893adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → dom 𝑇 = 𝐴)
90 ablfac1.2 . . . . . . . . . . . . . . . 16 (𝜑𝐷𝐴)
9190adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → 𝐷𝐴)
9288, 89, 91dprdres 19640 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → (𝐺dom DProd (𝑇𝐷) ∧ (𝐺 DProd (𝑇𝐷)) ⊆ (𝐺 DProd 𝑇)))
9392simpld 495 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → 𝐺dom DProd (𝑇𝐷))
944adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑞𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺))
9594, 91fssresd 6650 . . . . . . . . . . . . . 14 ((𝜑𝑞𝐴) → (𝑇𝐷):𝐷⟶(SubGrp‘𝐺))
9695fdmd 6620 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → dom (𝑇𝐷) = 𝐷)
97 difssd 4068 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷)
9893, 96, 97dprdres 19640 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝐺dom DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇𝐷))))
9998simpld 495 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → 𝐺dom DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))
100 dprdsubg 19636 . . . . . . . . . . 11 (𝐺dom DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺))
10199, 100syl 17 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺))
1026lagsubg 18827 . . . . . . . . . 10 (((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵))
103101, 19, 102syl2anc 584 . . . . . . . . 9 ((𝜑𝑞𝐴) → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵))
104 eqid 2739 . . . . . . . . . . . . . . 15 (0g𝐺) = (0g𝐺)
105104subg0cl 18772 . . . . . . . . . . . . . 14 ((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))
106101, 105syl 17 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (0g𝐺) ∈ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))
107106ne0d 4270 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)
1086dprdssv 19628 . . . . . . . . . . . . . 14 (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵
109 ssfi 8965 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin)
11019, 108, 109sylancl 586 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin)
111 hashnncl 14090 . . . . . . . . . . . . 13 ((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅))
112110, 111syl 17 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → ((♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅))
113107, 112mpbird 256 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ)
114113nnzd 12434 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ)
115 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑞𝑥 = 𝑞)
116 sneq 4572 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑞 → {𝑥} = {𝑞})
117116difeq2d 4058 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞}))
118117reseq2d 5894 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑞 → ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))
119118oveq2d 7300 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))
120119fveq2d 6787 . . . . . . . . . . . . . . 15 (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))))
121115, 120breq12d 5088 . . . . . . . . . . . . . 14 (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))))
122121notbid 318 . . . . . . . . . . . . 13 (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))))
123 eqid 2739 . . . . . . . . . . . . . . . 16 (𝑝𝐷 ↦ {𝑦𝐵 ∣ (𝑂𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝𝐷 ↦ {𝑦𝐵 ∣ (𝑂𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
1249adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → 𝐺 ∈ Abel)
12510adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → 𝐵 ∈ Fin)
126 ablfac1c.d . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
127126ssrab3 4016 . . . . . . . . . . . . . . . . 17 𝐷 ⊆ ℙ
128127a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ)
129 ssidd 3945 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → 𝐷𝐷)
1302, 3, 90dprdres 19640 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺dom DProd (𝑇𝐷) ∧ (𝐺 DProd (𝑇𝐷)) ⊆ (𝐺 DProd 𝑇)))
131130simpld 495 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺dom DProd (𝑇𝐷))
132 dprdsubg 19636 . . . . . . . . . . . . . . . . . . . . 21 (𝐺dom DProd (𝑇𝐷) → (𝐺 DProd (𝑇𝐷)) ∈ (SubGrp‘𝐺))
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺 DProd (𝑇𝐷)) ∈ (SubGrp‘𝐺))
134 difssd 4068 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐴𝐷) ⊆ 𝐴)
1352, 3, 134dprdres 19640 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴𝐷))) ⊆ (𝐺 DProd 𝑇)))
136135simpld 495 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺dom DProd (𝑇 ↾ (𝐴𝐷)))
137 dprdsubg 19636 . . . . . . . . . . . . . . . . . . . . 21 (𝐺dom DProd (𝑇 ↾ (𝐴𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴𝐷))) ∈ (SubGrp‘𝐺))
138136, 137syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴𝐷))) ∈ (SubGrp‘𝐺))
139 difss 4067 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴𝐷) ⊆ 𝐴
140 fssres 6649 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴𝐷)):(𝐴𝐷)⟶(SubGrp‘𝐺))
1414, 139, 140sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑇 ↾ (𝐴𝐷)):(𝐴𝐷)⟶(SubGrp‘𝐺))
142141fdmd 6620 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom (𝑇 ↾ (𝐴𝐷)) = (𝐴𝐷))
143 fvres 6802 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 ∈ (𝐴𝐷) → ((𝑇 ↾ (𝐴𝐷))‘𝑞) = (𝑇𝑞))
144143adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑞 ∈ (𝐴𝐷)) → ((𝑇 ↾ (𝐴𝐷))‘𝑞) = (𝑇𝑞))
145 eldif 3898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 ∈ (𝐴𝐷) ↔ (𝑞𝐴 ∧ ¬ 𝑞𝐷))
14631adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝑇𝑞) ∈ Fin)
147104subg0cl 18772 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑇𝑞) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝑇𝑞))
14824, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑞𝐴) → (0g𝐺) ∈ (𝑇𝑞))
149148snssd 4743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑞𝐴) → {(0g𝐺)} ⊆ (𝑇𝑞))
150149adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → {(0g𝐺)} ⊆ (𝑇𝑞))
151 fvex 6796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0g𝐺) ∈ V
152 hashsng 14093 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0g𝐺) ∈ V → (♯‘{(0g𝐺)}) = 1)
153151, 152ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (♯‘{(0g𝐺)}) = 1
15456adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (♯‘(𝑇𝑞)) = (𝑞𝐶))
15536adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑞𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ)
156 iddvdsexp 15998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞𝐶))
15758, 156sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑞𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞𝐶))
15864adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑞𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞𝐶) ∥ (♯‘𝐵))
15956, 34eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑞𝐴) → (𝑞𝐶) ∈ ℤ)
160 dvdstr 16012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑞 ∈ ℤ ∧ (𝑞𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞𝐶) ∧ (𝑞𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
16158, 159, 65, 160syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑞𝐴) → ((𝑞 ∥ (𝑞𝐶) ∧ (𝑞𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
162161adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝜑𝑞𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞𝐶) ∧ (𝑞𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵)))
163157, 158, 162mp2and 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝜑𝑞𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵))
164 breq1 5078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵)))
165164, 126elrab2 3628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑞𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵)))
166155, 163, 165sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑞𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞𝐷)
167166ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑞𝐴) → (𝐶 ∈ ℕ → 𝑞𝐷))
168167con3d 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑𝑞𝐴) → (¬ 𝑞𝐷 → ¬ 𝐶 ∈ ℕ))
169168impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → ¬ 𝐶 ∈ ℕ)
17059adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → 𝐶 ∈ ℕ0)
171 elnn0 12244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐶 ∈ ℕ0 ↔ (𝐶 ∈ ℕ ∨ 𝐶 = 0))
172170, 171sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0))
173172ord 861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0))
174169, 173mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → 𝐶 = 0)
175174oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝑞𝐶) = (𝑞↑0))
17638adantrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → 𝑞 ∈ ℕ)
177176nncnd 11998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → 𝑞 ∈ ℂ)
178177exp0d 13867 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝑞↑0) = 1)
179154, 175, 1783eqtrd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (♯‘(𝑇𝑞)) = 1)
180153, 179eqtr4id 2798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (♯‘{(0g𝐺)}) = (♯‘(𝑇𝑞)))
181 snfi 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 {(0g𝐺)} ∈ Fin
182 hashen 14070 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (({(0g𝐺)} ∈ Fin ∧ (𝑇𝑞) ∈ Fin) → ((♯‘{(0g𝐺)}) = (♯‘(𝑇𝑞)) ↔ {(0g𝐺)} ≈ (𝑇𝑞)))
183181, 146, 182sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → ((♯‘{(0g𝐺)}) = (♯‘(𝑇𝑞)) ↔ {(0g𝐺)} ≈ (𝑇𝑞)))
184180, 183mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → {(0g𝐺)} ≈ (𝑇𝑞))
185 fisseneq 9043 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑇𝑞) ∈ Fin ∧ {(0g𝐺)} ⊆ (𝑇𝑞) ∧ {(0g𝐺)} ≈ (𝑇𝑞)) → {(0g𝐺)} = (𝑇𝑞))
186146, 150, 184, 185syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → {(0g𝐺)} = (𝑇𝑞))
187104subg0cl 18772 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 DProd (𝑇𝐷)) ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ (𝐺 DProd (𝑇𝐷)))
188133, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (0g𝐺) ∈ (𝐺 DProd (𝑇𝐷)))
189188adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (0g𝐺) ∈ (𝐺 DProd (𝑇𝐷)))
190189snssd 4743 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → {(0g𝐺)} ⊆ (𝐺 DProd (𝑇𝐷)))
191186, 190eqsstrrd 3961 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝑇𝑞) ⊆ (𝐺 DProd (𝑇𝐷)))
192145, 191sylan2b 594 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑞 ∈ (𝐴𝐷)) → (𝑇𝑞) ⊆ (𝐺 DProd (𝑇𝐷)))
193144, 192eqsstrd 3960 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑞 ∈ (𝐴𝐷)) → ((𝑇 ↾ (𝐴𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇𝐷)))
194136, 142, 133, 193dprdlub 19638 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴𝐷))) ⊆ (𝐺 DProd (𝑇𝐷)))
195 eqid 2739 . . . . . . . . . . . . . . . . . . . . 21 (LSSum‘𝐺) = (LSSum‘𝐺)
196195lsmss2 19282 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 DProd (𝑇𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴𝐷))) ⊆ (𝐺 DProd (𝑇𝐷))) → ((𝐺 DProd (𝑇𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴𝐷)))) = (𝐺 DProd (𝑇𝐷)))
197133, 138, 194, 196syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺 DProd (𝑇𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴𝐷)))) = (𝐺 DProd (𝑇𝐷)))
198 disjdif 4406 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∩ (𝐴𝐷)) = ∅
199198a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐷 ∩ (𝐴𝐷)) = ∅)
200 undif2 4411 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∪ (𝐴𝐷)) = (𝐷𝐴)
201 ssequn1 4115 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐷𝐴 ↔ (𝐷𝐴) = 𝐴)
20290, 201sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐷𝐴) = 𝐴)
203200, 202eqtr2id 2792 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 = (𝐷 ∪ (𝐴𝐷)))
2044, 199, 203, 195, 2dprdsplit 19660 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴𝐷)))))
2051simprd 496 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺 DProd 𝑇) = 𝐵)
206204, 205eqtr3d 2781 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺 DProd (𝑇𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴𝐷)))) = 𝐵)
207197, 206eqtr3d 2781 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 DProd (𝑇𝐷)) = 𝐵)
208131, 207jca 512 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺dom DProd (𝑇𝐷) ∧ (𝐺 DProd (𝑇𝐷)) = 𝐵))
209208adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇𝐷) ∧ (𝐺 DProd (𝑇𝐷)) = 𝐵))
2104, 90fssresd 6650 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑇𝐷):𝐷⟶(SubGrp‘𝐺))
211210fdmd 6620 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑇𝐷) = 𝐷)
212211adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → dom (𝑇𝐷) = 𝐷)
21390sselda 3922 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐷) → 𝑞𝐴)
214213, 59syldan 591 . . . . . . . . . . . . . . . . 17 ((𝜑𝑞𝐷) → 𝐶 ∈ ℕ0)
215214adantlr 712 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℙ) ∧ 𝑞𝐷) → 𝐶 ∈ ℕ0)
216 fvres 6802 . . . . . . . . . . . . . . . . . . . 20 (𝑞𝐷 → ((𝑇𝐷)‘𝑞) = (𝑇𝑞))
217216adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑞𝐷) → ((𝑇𝐷)‘𝑞) = (𝑇𝑞))
218217fveq2d 6787 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐷) → (♯‘((𝑇𝐷)‘𝑞)) = (♯‘(𝑇𝑞)))
219213, 56syldan 591 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑞𝐷) → (♯‘(𝑇𝑞)) = (𝑞𝐶))
220218, 219eqtrd 2779 . . . . . . . . . . . . . . . . 17 ((𝜑𝑞𝐷) → (♯‘((𝑇𝐷)‘𝑞)) = (𝑞𝐶))
221220adantlr 712 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℙ) ∧ 𝑞𝐷) → (♯‘((𝑇𝐷)‘𝑞)) = (𝑞𝐶))
222 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → 𝑥 ∈ ℙ)
223 fzfid 13702 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...(♯‘𝐵)) ∈ Fin)
224 prmnn 16388 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℙ → 𝑤 ∈ ℕ)
2252243ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ)
226 prmz 16389 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℙ → 𝑤 ∈ ℤ)
227 dvdsle 16028 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
228226, 45, 227syl2anr 597 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵)))
2292283impia 1116 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵))
23045nnzd 12434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (♯‘𝐵) ∈ ℤ)
2312303ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
232 fznn 13333 . . . . . . . . . . . . . . . . . . . . . 22 ((♯‘𝐵) ∈ ℤ → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
233231, 232syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵))))
234225, 229, 233mpbir2and 710 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵)))
235234rabssdv 4009 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
236126, 235eqsstrid 3970 . . . . . . . . . . . . . . . . . 18 (𝜑𝐷 ⊆ (1...(♯‘𝐵)))
237223, 236ssfid 9051 . . . . . . . . . . . . . . . . 17 (𝜑𝐷 ∈ Fin)
238237adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℙ) → 𝐷 ∈ Fin)
2396, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238ablfac1eulem 19684 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})))))
240239ralrimiva 3104 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})))))
241240adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑥})))))
242122, 241, 36rspcdva 3563 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))))
243 coprm 16425 . . . . . . . . . . . . 13 ((𝑞 ∈ ℙ ∧ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
24436, 114, 243syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
245242, 244mpbid 231 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)
246 rpexp1i 16437 . . . . . . . . . . . 12 ((𝑞 ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
24758, 114, 47, 246syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1))
248245, 247mpd 15 . . . . . . . . . 10 ((𝜑𝑞𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)
249 coprmdvds2 16368 . . . . . . . . . 10 ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)))
25049, 114, 65, 248, 249syl31anc 1372 . . . . . . . . 9 ((𝜑𝑞𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)))
25187, 103, 250mp2and 696 . . . . . . . 8 ((𝜑𝑞𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))
252 eqid 2739 . . . . . . . . . 10 (Cntz‘𝐺) = (Cntz‘𝐺)
253 inss1 4163 . . . . . . . . . . . . . 14 (𝐷 ∩ {𝑞}) ⊆ 𝐷
254253a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑞𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷)
25593, 96, 254dprdres 19640 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → (𝐺dom DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇𝐷))))
256255simpld 495 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → 𝐺dom DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))
257 dprdsubg 19636 . . . . . . . . . . 11 (𝐺dom DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺))
258256, 257syl 17 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺))
259 inass 4154 . . . . . . . . . . . . 13 ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞})))
260 disjdif 4406 . . . . . . . . . . . . . 14 ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅
261260ineq2i 4144 . . . . . . . . . . . . 13 (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅)
262 in0 4326 . . . . . . . . . . . . 13 (𝐷 ∩ ∅) = ∅
263259, 261, 2623eqtri 2771 . . . . . . . . . . . 12 ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅
264263a1i 11 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅)
26593, 96, 254, 97, 264, 104dprddisj2 19651 . . . . . . . . . 10 ((𝜑𝑞𝐴) → ((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g𝐺)})
26693, 96, 254, 97, 264, 252dprdcntz2 19650 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))))
2676dprdssv 19628 . . . . . . . . . . 11 (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵
268 ssfi 8965 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin)
26919, 267, 268sylancl 586 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin)
270195, 104, 252, 258, 101, 265, 266, 269, 110lsmhash 19320 . . . . . . . . 9 ((𝜑𝑞𝐴) → (♯‘((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))))
271 inundif 4413 . . . . . . . . . . . . . 14 ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷
272271eqcomi 2748 . . . . . . . . . . . . 13 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))
273272a1i 11 . . . . . . . . . . . 12 ((𝜑𝑞𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})))
27495, 264, 273, 195, 93dprdsplit 19660 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺 DProd (𝑇𝐷)) = ((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))))
275207adantr 481 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺 DProd (𝑇𝐷)) = 𝐵)
276274, 275eqtr3d 2781 . . . . . . . . . 10 ((𝜑𝑞𝐴) → ((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵)
277276fveq2d 6787 . . . . . . . . 9 ((𝜑𝑞𝐴) → (♯‘((𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵))
278 snssi 4742 . . . . . . . . . . . . . . . . 17 (𝑞𝐷 → {𝑞} ⊆ 𝐷)
279278adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → {𝑞} ⊆ 𝐷)
280 sseqin2 4150 . . . . . . . . . . . . . . . 16 ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞})
281279, 280sylib 217 . . . . . . . . . . . . . . 15 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → (𝐷 ∩ {𝑞}) = {𝑞})
282281reseq2d 5894 . . . . . . . . . . . . . 14 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇𝐷) ↾ {𝑞}))
283282oveq2d 7300 . . . . . . . . . . . . 13 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇𝐷) ↾ {𝑞})))
28493adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → 𝐺dom DProd (𝑇𝐷))
285211ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → dom (𝑇𝐷) = 𝐷)
286 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → 𝑞𝐷)
287284, 285, 286dpjlem 19663 . . . . . . . . . . . . 13 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → (𝐺 DProd ((𝑇𝐷) ↾ {𝑞})) = ((𝑇𝐷)‘𝑞))
288216adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → ((𝑇𝐷)‘𝑞) = (𝑇𝑞))
289283, 287, 2883eqtrd 2783 . . . . . . . . . . . 12 (((𝜑𝑞𝐴) ∧ 𝑞𝐷) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇𝑞))
290 simprr 770 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → ¬ 𝑞𝐷)
291 disjsn 4648 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞𝐷)
292290, 291sylibr 233 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝐷 ∩ {𝑞}) = ∅)
293292reseq2d 5894 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇𝐷) ↾ ∅))
294 res0 5898 . . . . . . . . . . . . . . . 16 ((𝑇𝐷) ↾ ∅) = ∅
295293, 294eqtrdi 2795 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅)
296295oveq2d 7300 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅))
297104dprd0 19643 . . . . . . . . . . . . . . . . 17 (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = {(0g𝐺)}))
29840, 297syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = {(0g𝐺)}))
299298simprd 496 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 DProd ∅) = {(0g𝐺)})
300299adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝐺 DProd ∅) = {(0g𝐺)})
301296, 300, 1863eqtrd 2783 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑞𝐴 ∧ ¬ 𝑞𝐷)) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇𝑞))
302301anassrs 468 . . . . . . . . . . . 12 (((𝜑𝑞𝐴) ∧ ¬ 𝑞𝐷) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇𝑞))
303289, 302pm2.61dan 810 . . . . . . . . . . 11 ((𝜑𝑞𝐴) → (𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇𝑞))
304303fveq2d 6787 . . . . . . . . . 10 ((𝜑𝑞𝐴) → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇𝑞)))
305304oveq1d 7299 . . . . . . . . 9 ((𝜑𝑞𝐴) → ((♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇𝑞)) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))))
306270, 277, 3053eqtr3d 2787 . . . . . . . 8 ((𝜑𝑞𝐴) → (♯‘𝐵) = ((♯‘(𝑇𝑞)) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))))
307251, 306breqtrd 5101 . . . . . . 7 ((𝜑𝑞𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇𝑞)) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))))
308113nnne0d 12032 . . . . . . . 8 ((𝜑𝑞𝐴) → (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)
309 dvdsmulcr 16004 . . . . . . . 8 (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘(𝑇𝑞)) ∈ ℤ ∧ ((♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇𝑞)) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇𝑞))))
31049, 34, 114, 308, 309syl112anc 1373 . . . . . . 7 ((𝜑𝑞𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇𝑞)) · (♯‘(𝐺 DProd ((𝑇𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇𝑞))))
311307, 310mpbid 231 . . . . . 6 ((𝜑𝑞𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇𝑞)))
312 dvdseq 16032 . . . . . 6 ((((♯‘(𝑇𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0) ∧ ((♯‘(𝑇𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇𝑞)))) → (♯‘(𝑇𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
31333, 85, 73, 311, 312syl22anc 836 . . . . 5 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
3146, 7, 8, 9, 10, 11ablfac1a 19681 . . . . 5 ((𝜑𝑞𝐴) → (♯‘(𝑆𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵))))
315313, 314eqtr4d 2782 . . . 4 ((𝜑𝑞𝐴) → (♯‘(𝑇𝑞)) = (♯‘(𝑆𝑞)))
316 hashen 14070 . . . . 5 (((𝑇𝑞) ∈ Fin ∧ (𝑆𝑞) ∈ Fin) → ((♯‘(𝑇𝑞)) = (♯‘(𝑆𝑞)) ↔ (𝑇𝑞) ≈ (𝑆𝑞)))
31731, 23, 316syl2anc 584 . . . 4 ((𝜑𝑞𝐴) → ((♯‘(𝑇𝑞)) = (♯‘(𝑆𝑞)) ↔ (𝑇𝑞) ≈ (𝑆𝑞)))
318315, 317mpbid 231 . . 3 ((𝜑𝑞𝐴) → (𝑇𝑞) ≈ (𝑆𝑞))
319 fisseneq 9043 . . 3 (((𝑆𝑞) ∈ Fin ∧ (𝑇𝑞) ⊆ (𝑆𝑞) ∧ (𝑇𝑞) ≈ (𝑆𝑞)) → (𝑇𝑞) = (𝑆𝑞))
32023, 84, 318, 319syl3anc 1370 . 2 ((𝜑𝑞𝐴) → (𝑇𝑞) = (𝑆𝑞))
3215, 18, 320eqfnfvd 6921 1 (𝜑𝑇 = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2107  wne 2944  wral 3065  {crab 3069  Vcvv 3433  cdif 3885  cun 3886  cin 3887  wss 3888  c0 4257  {csn 4562   class class class wbr 5075  cmpt 5158  dom cdm 5590  cres 5592  wf 6433  cfv 6437  (class class class)co 7284  cen 8739  Fincfn 8742  0cc0 10880  1c1 10881   · cmul 10885  cle 11019  cn 11982  0cn0 12242  cz 12328  cuz 12591  ...cfz 13248  cexp 13791  chash 14053  cdvds 15972   gcd cgcd 16210  cprime 16385   pCnt cpc 16546  Basecbs 16921  0gc0g 17159  Grpcgrp 18586  SubGrpcsubg 18758  Cntzccntz 18930  odcod 19141  LSSumclsm 19248  Abelcabl 19396   DProd cdprd 19605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-disj 5041  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-tpos 8051  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-oadd 8310  df-omul 8311  df-er 8507  df-ec 8509  df-qs 8513  df-map 8626  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-sup 9210  df-inf 9211  df-oi 9278  df-dju 9668  df-card 9706  df-acn 9709  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-n0 12243  df-xnn0 12315  df-z 12329  df-uz 12592  df-q 12698  df-rp 12740  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-fac 13997  df-bc 14026  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-sum 15407  df-dvds 15973  df-gcd 16211  df-prm 16386  df-pc 16547  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-0g 17161  df-gsum 17162  df-mre 17304  df-mrc 17305  df-acs 17307  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-mhm 18439  df-submnd 18440  df-grp 18589  df-minusg 18590  df-sbg 18591  df-mulg 18710  df-subg 18761  df-eqg 18763  df-ghm 18841  df-gim 18884  df-ga 18905  df-cntz 18932  df-oppg 18959  df-od 19145  df-lsm 19250  df-pj1 19251  df-cmn 19397  df-abl 19398  df-dprd 19607
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator