| Step | Hyp | Ref
| Expression |
| 1 | | sylow2a.x |
. . 3
⊢ 𝑋 = (Base‘𝐺) |
| 2 | | sylow2a.m |
. . 3
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
| 3 | | sylow2a.p |
. . 3
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
| 4 | | sylow2a.f |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 5 | | sylow2a.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ Fin) |
| 6 | | sylow2a.z |
. . 3
⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} |
| 7 | | sylow2a.r |
. . 3
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
| 8 | 1, 2, 3, 4, 5, 6, 7 | sylow2alem2 19636 |
. 2
⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧)) |
| 9 | | inass 4228 |
. . . . . . 7
⊢ (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) = ((𝑌 / ∼ ) ∩ (𝒫
𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍))) |
| 10 | | disjdif 4472 |
. . . . . . . 8
⊢
(𝒫 𝑍 ∩
((𝑌 / ∼ )
∖ 𝒫 𝑍)) =
∅ |
| 11 | 10 | ineq2i 4217 |
. . . . . . 7
⊢ ((𝑌 / ∼ ) ∩ (𝒫
𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍))) = ((𝑌 / ∼ ) ∩
∅) |
| 12 | | in0 4395 |
. . . . . . 7
⊢ ((𝑌 / ∼ ) ∩ ∅) =
∅ |
| 13 | 9, 11, 12 | 3eqtri 2769 |
. . . . . 6
⊢ (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) =
∅ |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) =
∅) |
| 15 | | inundif 4479 |
. . . . . . 7
⊢ (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) = (𝑌 / ∼ ) |
| 16 | 15 | eqcomi 2746 |
. . . . . 6
⊢ (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) |
| 17 | 16 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫
𝑍))) |
| 18 | | pwfi 9357 |
. . . . . . 7
⊢ (𝑌 ∈ Fin ↔ 𝒫
𝑌 ∈
Fin) |
| 19 | 5, 18 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑌 ∈ Fin) |
| 20 | 7, 1 | gaorber 19326 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ∼ Er 𝑌) |
| 21 | 2, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∼ Er 𝑌) |
| 22 | 21 | qsss 8818 |
. . . . . 6
⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫
𝑌) |
| 23 | 19, 22 | ssfid 9301 |
. . . . 5
⊢ (𝜑 → (𝑌 / ∼ ) ∈
Fin) |
| 24 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin) |
| 25 | 22 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌) |
| 26 | 25 | elpwid 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌) |
| 27 | 24, 26 | ssfid 9301 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin) |
| 28 | | hashcl 14395 |
. . . . . . 7
⊢ (𝑧 ∈ Fin →
(♯‘𝑧) ∈
ℕ0) |
| 29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) →
(♯‘𝑧) ∈
ℕ0) |
| 30 | 29 | nn0cnd 12589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) →
(♯‘𝑧) ∈
ℂ) |
| 31 | 14, 17, 23, 30 | fsumsplit 15777 |
. . . 4
⊢ (𝜑 → Σ𝑧 ∈ (𝑌 / ∼
)(♯‘𝑧) =
(Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧))) |
| 32 | 21, 5 | qshash 15863 |
. . . 4
⊢ (𝜑 → (♯‘𝑌) = Σ𝑧 ∈ (𝑌 / ∼
)(♯‘𝑧)) |
| 33 | | inss1 4237 |
. . . . . . . 8
⊢ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ⊆ (𝑌 / ∼ ) |
| 34 | | ssfi 9213 |
. . . . . . . 8
⊢ (((𝑌 / ∼ ) ∈ Fin ∧
((𝑌 / ∼ )
∩ 𝒫 𝑍) ⊆
(𝑌 / ∼ ))
→ ((𝑌 / ∼ )
∩ 𝒫 𝑍) ∈
Fin) |
| 35 | 23, 33, 34 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈
Fin) |
| 36 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 37 | | fsumconst 15826 |
. . . . . . 7
⊢ ((((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈ Fin ∧ 1
∈ ℂ) → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)1 =
((♯‘((𝑌
/ ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
| 38 | 35, 36, 37 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)1 =
((♯‘((𝑌
/ ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
| 39 | | elin 3967 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) |
| 40 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑌 / ∼ ) = (𝑌 / ∼ ) |
| 41 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍)) |
| 42 | | velpw 4605 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍) |
| 43 | 41, 42 | bitr4di 289 |
. . . . . . . . . . . . . 14
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍)) |
| 44 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ≈
1o ↔ 𝑧
≈ 1o)) |
| 45 | 43, 44 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ ([𝑤] ∼ = 𝑧 → (([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈
1o) ↔ (𝑧
∈ 𝒫 𝑍 →
𝑧 ≈
1o))) |
| 46 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌) |
| 47 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌) |
| 48 | 46, 47 | erref 8765 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤) |
| 49 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
| 50 | 49, 49 | elec 8791 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤) |
| 51 | 48, 50 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ ) |
| 52 | | ssel 3977 |
. . . . . . . . . . . . . . 15
⊢ ([𝑤] ∼ ⊆ 𝑍 → (𝑤 ∈ [𝑤] ∼ → 𝑤 ∈ 𝑍)) |
| 53 | 51, 52 | syl5com 31 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍)) |
| 54 | 1, 2, 3, 4, 5, 6, 7 | sylow2alem1 19635 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤}) |
| 55 | 49 | ensn1 9061 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑤} ≈
1o |
| 56 | 54, 55 | eqbrtrdi 5182 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ≈
1o) |
| 57 | 56 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈
1o)) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈
1o)) |
| 59 | 53, 58 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈
1o)) |
| 60 | 40, 45, 59 | ectocld 8824 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1o)) |
| 61 | 60 | impr 454 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) → 𝑧 ≈ 1o) |
| 62 | 39, 61 | sylan2b 594 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ≈
1o) |
| 63 | | en1b 9065 |
. . . . . . . . . 10
⊢ (𝑧 ≈ 1o ↔
𝑧 = {∪ 𝑧}) |
| 64 | 62, 63 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 = {∪
𝑧}) |
| 65 | 64 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) →
(♯‘𝑧) =
(♯‘{∪ 𝑧})) |
| 66 | | vuniex 7759 |
. . . . . . . . 9
⊢ ∪ 𝑧
∈ V |
| 67 | | hashsng 14408 |
. . . . . . . . 9
⊢ (∪ 𝑧
∈ V → (♯‘{∪ 𝑧}) = 1) |
| 68 | 66, 67 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘{∪ 𝑧}) = 1 |
| 69 | 65, 68 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) →
(♯‘𝑧) =
1) |
| 70 | 69 | sumeq2dv 15738 |
. . . . . 6
⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(♯‘𝑧) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)1) |
| 71 | 6 | ssrab3 4082 |
. . . . . . . . . . 11
⊢ 𝑍 ⊆ 𝑌 |
| 72 | | ssfi 9213 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ Fin) |
| 73 | 5, 71, 72 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ Fin) |
| 74 | | hashcl 14395 |
. . . . . . . . . 10
⊢ (𝑍 ∈ Fin →
(♯‘𝑍) ∈
ℕ0) |
| 75 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑍) ∈
ℕ0) |
| 76 | 75 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑍) ∈
ℂ) |
| 77 | 76 | mulridd 11278 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝑍) · 1) =
(♯‘𝑍)) |
| 78 | 6, 5 | rabexd 5340 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ V) |
| 79 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑍 ↦ {𝑤}) = (𝑤 ∈ 𝑍 ↦ {𝑤}) |
| 80 | 7 | relopabiv 5830 |
. . . . . . . . . . . . . . 15
⊢ Rel ∼ |
| 81 | | relssdmrn 6288 |
. . . . . . . . . . . . . . 15
⊢ (Rel
∼
→ ∼ ⊆ (dom ∼
× ran ∼ )) |
| 82 | 80, 81 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ∼
⊆ (dom ∼ × ran ∼
) |
| 83 | | erdm 8755 |
. . . . . . . . . . . . . . . . 17
⊢ ( ∼ Er
𝑌 → dom ∼ =
𝑌) |
| 84 | 21, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom ∼ = 𝑌) |
| 85 | 84, 5 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom ∼ ∈
Fin) |
| 86 | | errn 8767 |
. . . . . . . . . . . . . . . . 17
⊢ ( ∼ Er
𝑌 → ran ∼ =
𝑌) |
| 87 | 21, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran ∼ = 𝑌) |
| 88 | 87, 5 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran ∼ ∈
Fin) |
| 89 | 85, 88 | xpexd 7771 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (dom ∼ × ran ∼ )
∈ V) |
| 90 | | ssexg 5323 |
. . . . . . . . . . . . . 14
⊢ (( ∼
⊆ (dom ∼ × ran ∼ )
∧ (dom ∼ × ran ∼ )
∈ V) → ∼ ∈
V) |
| 91 | 82, 89, 90 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∼ ∈
V) |
| 92 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍) |
| 93 | 71, 92 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑌) |
| 94 | | ecelqsg 8812 |
. . . . . . . . . . . . 13
⊢ (( ∼ ∈
V ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈ (𝑌 / ∼ )) |
| 95 | 91, 93, 94 | syl2an2r 685 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ∈ (𝑌 / ∼ )) |
| 96 | 54, 95 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ (𝑌 / ∼ )) |
| 97 | | snelpwi 5448 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑍 → {𝑤} ∈ 𝒫 𝑍) |
| 98 | 97 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ 𝒫 𝑍) |
| 99 | 96, 98 | elind 4200 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) |
| 100 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) |
| 101 | 100 | elin2d 4205 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ∈ 𝒫 𝑍) |
| 102 | 101 | elpwid 4609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ⊆ 𝑍) |
| 103 | 64, 102 | eqsstrrd 4019 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → {∪ 𝑧}
⊆ 𝑍) |
| 104 | 66 | snss 4785 |
. . . . . . . . . . 11
⊢ (∪ 𝑧
∈ 𝑍 ↔ {∪ 𝑧}
⊆ 𝑍) |
| 105 | 103, 104 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → ∪ 𝑧
∈ 𝑍) |
| 106 | | sneq 4636 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∪
𝑧 → {𝑤} = {∪ 𝑧}) |
| 107 | 106 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ∪
𝑧 → (𝑧 = {𝑤} ↔ 𝑧 = {∪ 𝑧})) |
| 108 | 64, 107 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → (𝑤 = ∪
𝑧 → 𝑧 = {𝑤})) |
| 109 | 108 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) → (𝑤 = ∪
𝑧 → 𝑧 = {𝑤})) |
| 110 | | unieq 4918 |
. . . . . . . . . . . 12
⊢ (𝑧 = {𝑤} → ∪ 𝑧 = ∪
{𝑤}) |
| 111 | | unisnv 4927 |
. . . . . . . . . . . 12
⊢ ∪ {𝑤}
= 𝑤 |
| 112 | 110, 111 | eqtr2di 2794 |
. . . . . . . . . . 11
⊢ (𝑧 = {𝑤} → 𝑤 = ∪ 𝑧) |
| 113 | 109, 112 | impbid1 225 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) → (𝑤 = ∪
𝑧 ↔ 𝑧 = {𝑤})) |
| 114 | 79, 99, 105, 113 | f1o2d 7687 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ 𝑍 ↦ {𝑤}):𝑍–1-1-onto→((𝑌 / ∼ ) ∩ 𝒫
𝑍)) |
| 115 | 78, 114 | hasheqf1od 14392 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑍) = (♯‘((𝑌 / ∼ ) ∩ 𝒫
𝑍))) |
| 116 | 115 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝑍) · 1) =
((♯‘((𝑌
/ ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
| 117 | 77, 116 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (♯‘𝑍) = ((♯‘((𝑌 / ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
| 118 | 38, 70, 117 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝜑 → (♯‘𝑍) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(♯‘𝑧)) |
| 119 | 118 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧)) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(♯‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧))) |
| 120 | 31, 32, 119 | 3eqtr4rd 2788 |
. . 3
⊢ (𝜑 → ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧)) = (♯‘𝑌)) |
| 121 | | hashcl 14395 |
. . . . . 6
⊢ (𝑌 ∈ Fin →
(♯‘𝑌) ∈
ℕ0) |
| 122 | 5, 121 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑌) ∈
ℕ0) |
| 123 | 122 | nn0cnd 12589 |
. . . 4
⊢ (𝜑 → (♯‘𝑌) ∈
ℂ) |
| 124 | | diffi 9215 |
. . . . . 6
⊢ ((𝑌 / ∼ ) ∈ Fin →
((𝑌 / ∼ )
∖ 𝒫 𝑍) ∈
Fin) |
| 125 | 23, 124 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫
𝑍) ∈
Fin) |
| 126 | | eldifi 4131 |
. . . . . 6
⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍) → 𝑧 ∈ (𝑌 / ∼ )) |
| 127 | 126, 30 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) →
(♯‘𝑧) ∈
ℂ) |
| 128 | 125, 127 | fsumcl 15769 |
. . . 4
⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧) ∈
ℂ) |
| 129 | 123, 76, 128 | subaddd 11638 |
. . 3
⊢ (𝜑 → (((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧) ↔ ((♯‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧)) = (♯‘𝑌))) |
| 130 | 120, 129 | mpbird 257 |
. 2
⊢ (𝜑 → ((♯‘𝑌) − (♯‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧)) |
| 131 | 8, 130 | breqtrrd 5171 |
1
⊢ (𝜑 → 𝑃 ∥ ((♯‘𝑌) − (♯‘𝑍))) |