| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ablfac1eu.1 | . . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) | 
| 2 | 1 | simpld 494 | . . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑇) | 
| 3 |  | ablfac1eu.2 | . . . 4
⊢ (𝜑 → dom 𝑇 = 𝐴) | 
| 4 | 2, 3 | dprdf2 20028 | . . 3
⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺)) | 
| 5 | 4 | ffnd 6736 | . 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
⊢ (𝜑 → 𝐴 ⊆ ℙ) | 
| 12 | 6, 7, 8, 9, 10, 11 | ablfac1b 20091 | . . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) | 
| 13 | 6 | fvexi 6919 | . . . . . . 7
⊢ 𝐵 ∈ V | 
| 14 | 13 | rabex 5338 | . . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V | 
| 15 | 14, 8 | dmmpti 6711 | . . . . 5
⊢ dom 𝑆 = 𝐴 | 
| 16 | 15 | a1i 11 | . . . 4
⊢ (𝜑 → dom 𝑆 = 𝐴) | 
| 17 | 12, 16 | dprdf2 20028 | . . 3
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) | 
| 18 | 17 | ffnd 6736 | . 2
⊢ (𝜑 → 𝑆 Fn 𝐴) | 
| 19 | 10 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin) | 
| 20 | 17 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) | 
| 21 | 6 | subgss 19146 | . . . . 5
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵) | 
| 22 | 20, 21 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵) | 
| 23 | 19, 22 | ssfid 9302 | . . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin) | 
| 24 | 4 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) | 
| 25 | 6 | subgss 19146 | . . . . . 6
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵) | 
| 26 | 24, 25 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵) | 
| 27 | 26 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵) | 
| 28 | 6, 7 | odcl 19555 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈
ℕ0) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈
ℕ0) | 
| 30 | 29 | nn0zd 12641 | . . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ) | 
| 31 | 19, 26 | ssfid 9302 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin) | 
| 32 |  | hashcl 14396 | . . . . . . . . 9
⊢ ((𝑇‘𝑞) ∈ Fin → (♯‘(𝑇‘𝑞)) ∈
ℕ0) | 
| 33 | 31, 32 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈
ℕ0) | 
| 34 | 33 | nn0zd 12641 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℤ) | 
| 35 | 34 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∈ ℤ) | 
| 36 | 11 | sselda 3982 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) | 
| 37 |  | prmnn 16712 | . . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ) | 
| 39 |  | ablgrp 19804 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | 
| 40 | 9, 39 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 41 | 6 | grpbn0 18985 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) | 
| 42 | 40, 41 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ≠ ∅) | 
| 43 |  | hashnncl 14406 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ Fin →
((♯‘𝐵) ∈
ℕ ↔ 𝐵 ≠
∅)) | 
| 44 | 10, 43 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) | 
| 45 | 42, 44 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) | 
| 46 | 45 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ) | 
| 47 | 36, 46 | pccld 16889 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
ℕ0) | 
| 48 | 38, 47 | nnexpcld 14285 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ) | 
| 49 | 48 | nnzd 12642 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) | 
| 50 | 49 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) | 
| 51 | 24 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) | 
| 52 | 31 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin) | 
| 53 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞)) | 
| 54 | 7 | odsubdvds 19590 | . . . . . . 7
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) | 
| 55 | 51, 52, 53, 54 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) | 
| 56 |  | ablfac1eu.4 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) | 
| 57 |  | prmz 16713 | . . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) | 
| 58 | 36, 57 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ) | 
| 59 |  | ablfac1eu.3 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈
ℕ0) | 
| 60 | 59 | nn0zd 12641 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ) | 
| 61 | 47 | nn0zd 12641 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) | 
| 62 | 6 | lagsubg 19214 | . . . . . . . . . . . . 13
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) | 
| 63 | 24, 19, 62 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) | 
| 64 | 56, 63 | eqbrtrrd 5166 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (♯‘𝐵)) | 
| 65 | 46 | nnzd 12642 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℤ) | 
| 66 |  | pcdvdsb 16908 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℤ ∧ 𝐶 ∈
ℕ0) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) | 
| 67 | 36, 65, 59, 66 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) | 
| 68 | 64, 67 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))) | 
| 69 |  | eluz2 12885 | . . . . . . . . . 10
⊢ ((𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))) | 
| 70 | 60, 61, 68, 69 | syl3anbrc 1343 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶)) | 
| 71 |  | dvdsexp 16366 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0
∧ (𝑞 pCnt
(♯‘𝐵)) ∈
(ℤ≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 72 | 58, 59, 70, 71 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 73 | 56, 72 | eqbrtrd 5164 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 74 | 73 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 75 | 30, 35, 50, 55, 74 | dvdstrd 16333 | . . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 76 | 26, 75 | ssrabdv 4073 | . . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) | 
| 77 |  | id 22 | . . . . . . . . 9
⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞) | 
| 78 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵))) | 
| 79 | 77, 78 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 80 | 79 | breq2d 5154 | . . . . . . 7
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) | 
| 81 | 80 | rabbidv 3443 | . . . . . 6
⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) | 
| 82 | 81, 8, 14 | fvmpt3i 7020 | . . . . 5
⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) | 
| 83 | 82 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) | 
| 84 | 76, 83 | sseqtrrd 4020 | . . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞)) | 
| 85 | 48 | nnnn0d 12589 | . . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈
ℕ0) | 
| 86 |  | pcdvds 16903 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) | 
| 87 | 36, 46, 86 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) | 
| 88 | 2 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇) | 
| 89 | 3 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴) | 
| 90 |  | ablfac1.2 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ⊆ 𝐴) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴) | 
| 92 | 88, 89, 91 | dprdres 20049 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) | 
| 93 | 92 | simpld 494 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷)) | 
| 94 | 4 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺)) | 
| 95 | 94, 91 | fssresd 6774 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) | 
| 96 | 95 | fdmd 6745 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷) | 
| 97 |  | difssd 4136 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷) | 
| 98 | 93, 96, 97 | dprdres 20049 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) | 
| 99 | 98 | simpld 494 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) | 
| 100 |  | dprdsubg 20045 | . . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) | 
| 101 | 99, 100 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) | 
| 102 | 6 | lagsubg 19214 | . . . . . . . . . 10
⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) | 
| 103 | 101, 19, 102 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) | 
| 104 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 105 | 104 | subg0cl 19153 | . . . . . . . . . . . . . 14
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) | 
| 106 | 101, 105 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) | 
| 107 | 106 | ne0d 4341 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅) | 
| 108 | 6 | dprdssv 20037 | . . . . . . . . . . . . . 14
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵 | 
| 109 |  | ssfi 9214 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) | 
| 110 | 19, 108, 109 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) | 
| 111 |  | hashnncl 14406 | . . . . . . . . . . . . 13
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) | 
| 112 | 110, 111 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) | 
| 113 | 107, 112 | mpbird 257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ) | 
| 114 | 113 | nnzd 12642 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) | 
| 115 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞) | 
| 116 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞}) | 
| 117 | 116 | difeq2d 4125 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞})) | 
| 118 | 117 | reseq2d 5996 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) | 
| 119 | 118 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) | 
| 120 | 119 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) | 
| 121 | 115, 120 | breq12d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) | 
| 122 | 121 | notbid 318 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) | 
| 123 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) | 
| 124 | 9 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel) | 
| 125 | 10 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin) | 
| 126 |  | ablfac1c.d | . . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} | 
| 127 | 126 | ssrab3 4081 | . . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆
ℙ | 
| 128 | 127 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ) | 
| 129 |  | ssidd 4006 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷) | 
| 130 | 2, 3, 90 | dprdres 20049 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) | 
| 131 | 130 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷)) | 
| 132 |  | dprdsubg 20045 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) | 
| 133 | 131, 132 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) | 
| 134 |  | difssd 4136 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴) | 
| 135 | 2, 3, 134 | dprdres 20049 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇))) | 
| 136 | 135 | simpld 494 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) | 
| 137 |  | dprdsubg 20045 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) | 
| 138 | 136, 137 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) | 
| 139 |  | difss 4135 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴 | 
| 140 |  | fssres 6773 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) | 
| 141 | 4, 139, 140 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) | 
| 142 | 141 | fdmd 6745 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷)) | 
| 143 |  | fvres 6924 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) | 
| 144 | 143 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) | 
| 145 |  | eldif 3960 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) | 
| 146 | 31 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin) | 
| 147 | 104 | subg0cl 19153 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑇‘𝑞)) | 
| 148 | 24, 147 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑇‘𝑞)) | 
| 149 | 148 | snssd 4808 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) | 
| 150 | 149 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) | 
| 151 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0g‘𝐺) ∈ V | 
| 152 |  | hashsng 14409 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0g‘𝐺) ∈ V →
(♯‘{(0g‘𝐺)}) = 1) | 
| 153 | 151, 152 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(♯‘{(0g‘𝐺)}) = 1 | 
| 154 | 56 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) | 
| 155 | 36 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ) | 
| 156 |  | iddvdsexp 16318 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) | 
| 157 | 58, 156 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) | 
| 158 | 64 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (♯‘𝐵)) | 
| 159 | 56, 34 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ) | 
| 160 |  | dvdstr 16332 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) | 
| 161 | 58, 159, 65, 160 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) | 
| 162 | 161 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) | 
| 163 | 157, 158,
162 | mp2and 699 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵)) | 
| 164 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵))) | 
| 165 | 164, 126 | elrab2 3694 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵))) | 
| 166 | 155, 163,
165 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷) | 
| 167 | 166 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷)) | 
| 168 | 167 | con3d 152 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ)) | 
| 169 | 168 | impr 454 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ) | 
| 170 | 59 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈
ℕ0) | 
| 171 |  | elnn0 12530 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐶 ∈ ℕ0
↔ (𝐶 ∈ ℕ
∨ 𝐶 =
0)) | 
| 172 | 170, 171 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0)) | 
| 173 | 172 | ord 864 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0)) | 
| 174 | 169, 173 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0) | 
| 175 | 174 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0)) | 
| 176 | 38 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ) | 
| 177 | 176 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ) | 
| 178 | 177 | exp0d 14181 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1) | 
| 179 | 154, 175,
178 | 3eqtrd 2780 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = 1) | 
| 180 | 153, 179 | eqtr4id 2795 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
(♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞))) | 
| 181 |  | snfi 9084 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
{(0g‘𝐺)} ∈ Fin | 
| 182 |  | hashen 14387 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(({(0g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) | 
| 183 | 181, 146,
182 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) | 
| 184 | 180, 183 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ≈ (𝑇‘𝑞)) | 
| 185 |  | fisseneq 9294 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑇‘𝑞) ∈ Fin ∧
{(0g‘𝐺)}
⊆ (𝑇‘𝑞) ∧
{(0g‘𝐺)}
≈ (𝑇‘𝑞)) →
{(0g‘𝐺)} =
(𝑇‘𝑞)) | 
| 186 | 146, 150,
184, 185 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} = (𝑇‘𝑞)) | 
| 187 | 104 | subg0cl 19153 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 188 | 133, 187 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 189 | 188 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 190 | 189 | snssd 4808 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 191 | 186, 190 | eqsstrrd 4018 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 192 | 145, 191 | sylan2b 594 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 193 | 144, 192 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 194 | 136, 142,
133, 193 | dprdlub 20047 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 195 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) | 
| 196 | 195 | lsmss2 19686 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 197 | 133, 138,
194, 196 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) | 
| 198 |  | disjdif 4471 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅ | 
| 199 | 198 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅) | 
| 200 |  | undif2 4476 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴) | 
| 201 |  | ssequn1 4185 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴) | 
| 202 | 90, 201 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴) | 
| 203 | 200, 202 | eqtr2id 2789 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷))) | 
| 204 | 4, 199, 203, 195, 2 | dprdsplit 20069 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))))) | 
| 205 | 1 | simprd 495 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵) | 
| 206 | 204, 205 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵) | 
| 207 | 197, 206 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) | 
| 208 | 131, 207 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) | 
| 209 | 208 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) | 
| 210 | 4, 90 | fssresd 6774 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) | 
| 211 | 210 | fdmd 6745 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷) | 
| 212 | 211 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷) | 
| 213 | 90 | sselda 3982 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴) | 
| 214 | 213, 59 | syldan 591 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) | 
| 215 | 214 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) | 
| 216 |  | fvres 6924 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) | 
| 217 | 216 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) | 
| 218 | 217 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (♯‘(𝑇‘𝑞))) | 
| 219 | 213, 56 | syldan 591 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) | 
| 220 | 218, 219 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) | 
| 221 | 220 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) | 
| 222 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ) | 
| 223 |  | fzfid 14015 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(♯‘𝐵)) ∈ Fin) | 
| 224 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℕ) | 
| 225 | 224 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ) | 
| 226 |  | prmz 16713 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℤ) | 
| 227 |  | dvdsle 16348 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ ℤ ∧
(♯‘𝐵) ∈
ℕ) → (𝑤 ∥
(♯‘𝐵) →
𝑤 ≤ (♯‘𝐵))) | 
| 228 | 226, 45, 227 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵))) | 
| 229 | 228 | 3impia 1117 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵)) | 
| 230 | 45 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) | 
| 231 | 230 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) | 
| 232 |  | fznn 13633 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐵)
∈ ℤ → (𝑤
∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) | 
| 233 | 231, 232 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) | 
| 234 | 225, 229,
233 | mpbir2and 713 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵))) | 
| 235 | 234 | rabssdv 4074 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))) | 
| 236 | 126, 235 | eqsstrid 4021 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ⊆ (1...(♯‘𝐵))) | 
| 237 | 223, 236 | ssfid 9302 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ Fin) | 
| 238 | 237 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin) | 
| 239 | 6, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238 | ablfac1eulem 20093 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) | 
| 240 | 239 | ralrimiva 3145 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) | 
| 241 | 240 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) | 
| 242 | 122, 241,
36 | rspcdva 3622 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) | 
| 243 |  | coprm 16749 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) | 
| 244 | 36, 114, 243 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) | 
| 245 | 242, 244 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) | 
| 246 |  | rpexp1i 16761 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
→ ((𝑞 gcd
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) | 
| 247 | 58, 114, 47, 246 | syl3anc 1372 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) | 
| 248 | 245, 247 | mpd 15 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) | 
| 249 |  | coprmdvds2 16692 | . . . . . . . . . 10
⊢ ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘𝐵) ∈
ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) | 
| 250 | 49, 114, 65, 248, 249 | syl31anc 1374 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) | 
| 251 | 87, 103, 250 | mp2and 699 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)) | 
| 252 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) | 
| 253 |  | inss1 4236 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷 | 
| 254 | 253 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷) | 
| 255 | 93, 96, 254 | dprdres 20049 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) | 
| 256 | 255 | simpld 494 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) | 
| 257 |  | dprdsubg 20045 | . . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) | 
| 258 | 256, 257 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) | 
| 259 |  | inass 4227 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) | 
| 260 |  | disjdif 4471 | . . . . . . . . . . . . . 14
⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅ | 
| 261 | 260 | ineq2i 4216 | . . . . . . . . . . . . 13
⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅) | 
| 262 |  | in0 4394 | . . . . . . . . . . . . 13
⊢ (𝐷 ∩ ∅) =
∅ | 
| 263 | 259, 261,
262 | 3eqtri 2768 | . . . . . . . . . . . 12
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅ | 
| 264 | 263 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅) | 
| 265 | 93, 96, 254, 97, 264, 104 | dprddisj2 20060 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g‘𝐺)}) | 
| 266 | 93, 96, 254, 97, 264, 252 | dprdcntz2 20059 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) | 
| 267 | 6 | dprdssv 20037 | . . . . . . . . . . 11
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵 | 
| 268 |  | ssfi 9214 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) | 
| 269 | 19, 267, 268 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) | 
| 270 | 195, 104,
252, 258, 101, 265, 266, 269, 110 | lsmhash 19724 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) | 
| 271 |  | inundif 4478 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷 | 
| 272 | 271 | eqcomi 2745 | . . . . . . . . . . . . 13
⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) | 
| 273 | 272 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))) | 
| 274 | 95, 264, 273, 195, 93 | dprdsplit 20069 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) | 
| 275 | 207 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) | 
| 276 | 274, 275 | eqtr3d 2778 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵) | 
| 277 | 276 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵)) | 
| 278 |  | snssi 4807 | . . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷) | 
| 279 | 278 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷) | 
| 280 |  | sseqin2 4222 | . . . . . . . . . . . . . . . 16
⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞}) | 
| 281 | 279, 280 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞}) | 
| 282 | 281 | reseq2d 5996 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞})) | 
| 283 | 282 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞}))) | 
| 284 | 93 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷)) | 
| 285 | 211 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷) | 
| 286 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷) | 
| 287 | 284, 285,
286 | dpjlem 20072 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞)) | 
| 288 | 216 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) | 
| 289 | 283, 287,
288 | 3eqtrd 2780 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) | 
| 290 |  | simprr 772 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷) | 
| 291 |  | disjsn 4710 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷) | 
| 292 | 290, 291 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅) | 
| 293 | 292 | reseq2d 5996 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅)) | 
| 294 |  | res0 6000 | . . . . . . . . . . . . . . . 16
⊢ ((𝑇 ↾ 𝐷) ↾ ∅) =
∅ | 
| 295 | 293, 294 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅) | 
| 296 | 295 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅)) | 
| 297 | 104 | dprd0 20052 | . . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) | 
| 298 | 40, 297 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) | 
| 299 | 298 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 DProd ∅) =
{(0g‘𝐺)}) | 
| 300 | 299 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) =
{(0g‘𝐺)}) | 
| 301 | 296, 300,
186 | 3eqtrd 2780 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) | 
| 302 | 301 | anassrs 467 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) | 
| 303 | 289, 302 | pm2.61dan 812 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) | 
| 304 | 303 | fveq2d 6909 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇‘𝑞))) | 
| 305 | 304 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) | 
| 306 | 270, 277,
305 | 3eqtr3d 2784 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) | 
| 307 | 251, 306 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) | 
| 308 | 113 | nnne0d 12317 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0) | 
| 309 |  | dvdsmulcr 16324 | . . . . . . . 8
⊢ (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝑇‘𝑞)) ∈ ℤ ∧
((♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) | 
| 310 | 49, 34, 114, 308, 309 | syl112anc 1375 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) | 
| 311 | 307, 310 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))) | 
| 312 |  | dvdseq 16352 | . . . . . 6
⊢
((((♯‘(𝑇‘𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0) ∧
((♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 313 | 33, 85, 73, 311, 312 | syl22anc 838 | . . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 314 | 6, 7, 8, 9, 10, 11 | ablfac1a 20090 | . . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) | 
| 315 | 313, 314 | eqtr4d 2779 | . . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞))) | 
| 316 |  | hashen 14387 | . . . . 5
⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) | 
| 317 | 31, 23, 316 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) | 
| 318 | 315, 317 | mpbid 232 | . . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞)) | 
| 319 |  | fisseneq 9294 | . . 3
⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞)) | 
| 320 | 23, 84, 318, 319 | syl3anc 1372 | . 2
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞)) | 
| 321 | 5, 18, 320 | eqfnfvd 7053 | 1
⊢ (𝜑 → 𝑇 = 𝑆) |