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 17856 |
. 2
⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧)) |
9 | | inass 3785 |
. . . . . . 7
⊢ (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) = ((𝑌 / ∼ ) ∩ (𝒫
𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍))) |
10 | | disjdif 3992 |
. . . . . . . 8
⊢
(𝒫 𝑍 ∩
((𝑌 / ∼ )
∖ 𝒫 𝑍)) =
∅ |
11 | 10 | ineq2i 3773 |
. . . . . . 7
⊢ ((𝑌 / ∼ ) ∩ (𝒫
𝑍 ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍))) = ((𝑌 / ∼ ) ∩
∅) |
12 | | in0 3920 |
. . . . . . 7
⊢ ((𝑌 / ∼ ) ∩ ∅) =
∅ |
13 | 9, 11, 12 | 3eqtri 2636 |
. . . . . 6
⊢ (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) =
∅ |
14 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∩ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) =
∅) |
15 | | inundif 3998 |
. . . . . . 7
⊢ (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) = (𝑌 / ∼ ) |
16 | 15 | eqcomi 2619 |
. . . . . 6
⊢ (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) |
17 | 16 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑌 / ∼ ) = (((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∪ ((𝑌 / ∼ ) ∖ 𝒫
𝑍))) |
18 | | pwfi 8144 |
. . . . . . 7
⊢ (𝑌 ∈ Fin ↔ 𝒫
𝑌 ∈
Fin) |
19 | 5, 18 | sylib 207 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑌 ∈ Fin) |
20 | 7, 1 | gaorber 17564 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ∼ Er 𝑌) |
21 | 2, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ∼ Er 𝑌) |
22 | 21 | qsss 7695 |
. . . . . 6
⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫
𝑌) |
23 | 19, 22 | ssfid 8068 |
. . . . 5
⊢ (𝜑 → (𝑌 / ∼ ) ∈
Fin) |
24 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin) |
25 | 22 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌) |
26 | 25 | elpwid 4118 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌) |
27 | 24, 26 | ssfid 8068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin) |
28 | | hashcl 13009 |
. . . . . . 7
⊢ (𝑧 ∈ Fin →
(#‘𝑧) ∈
ℕ0) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) →
(#‘𝑧) ∈
ℕ0) |
30 | 29 | nn0cnd 11230 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) →
(#‘𝑧) ∈
ℂ) |
31 | 14, 17, 23, 30 | fsumsplit 14318 |
. . . 4
⊢ (𝜑 → Σ𝑧 ∈ (𝑌 / ∼ )(#‘𝑧) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(#‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧))) |
32 | 21, 5 | qshash 14398 |
. . . 4
⊢ (𝜑 → (#‘𝑌) = Σ𝑧 ∈ (𝑌 / ∼ )(#‘𝑧)) |
33 | | inss1 3795 |
. . . . . . . 8
⊢ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ⊆ (𝑌 / ∼ ) |
34 | | ssfi 8065 |
. . . . . . . 8
⊢ (((𝑌 / ∼ ) ∈ Fin ∧
((𝑌 / ∼ )
∩ 𝒫 𝑍) ⊆
(𝑌 / ∼ ))
→ ((𝑌 / ∼ )
∩ 𝒫 𝑍) ∈
Fin) |
35 | 23, 33, 34 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈
Fin) |
36 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
37 | | fsumconst 14364 |
. . . . . . 7
⊢ ((((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈ Fin ∧ 1
∈ ℂ) → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)1 = ((#‘((𝑌 / ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
38 | 35, 36, 37 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)1 = ((#‘((𝑌 / ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
39 | | elin 3758 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) |
40 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑌 / ∼ ) = (𝑌 / ∼ ) |
41 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍)) |
42 | | selpw 4115 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍) |
43 | 41, 42 | syl6bbr 277 |
. . . . . . . . . . . . . 14
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍)) |
44 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ≈
1𝑜 ↔ 𝑧 ≈
1𝑜)) |
45 | 43, 44 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ ([𝑤] ∼ = 𝑧 → (([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈
1𝑜) ↔ (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈
1𝑜))) |
46 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌) |
47 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌) |
48 | 46, 47 | erref 7649 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤) |
49 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
50 | 49, 49 | elec 7673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤) |
51 | 48, 50 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ ) |
52 | | ssel 3562 |
. . . . . . . . . . . . . . 15
⊢ ([𝑤] ∼ ⊆ 𝑍 → (𝑤 ∈ [𝑤] ∼ → 𝑤 ∈ 𝑍)) |
53 | 51, 52 | syl5com 31 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍)) |
54 | 1, 2, 3, 4, 5, 6, 7 | sylow2alem1 17855 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤}) |
55 | 49 | ensn1 7906 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑤} ≈
1𝑜 |
56 | 54, 55 | syl6eqbr 4622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ≈
1𝑜) |
57 | 56 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈
1𝑜)) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ≈
1𝑜)) |
59 | 53, 58 | syld 46 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ ⊆ 𝑍 → [𝑤] ∼ ≈
1𝑜)) |
60 | 40, 45, 59 | ectocld 7701 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈
1𝑜)) |
61 | 60 | impr 647 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍)) → 𝑧 ≈
1𝑜) |
62 | 39, 61 | sylan2b 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ≈
1𝑜) |
63 | | en1b 7910 |
. . . . . . . . . 10
⊢ (𝑧 ≈ 1𝑜
↔ 𝑧 = {∪ 𝑧}) |
64 | 62, 63 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 = {∪
𝑧}) |
65 | 64 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → (#‘𝑧) = (#‘{∪ 𝑧})) |
66 | | vuniex 6852 |
. . . . . . . . 9
⊢ ∪ 𝑧
∈ V |
67 | | hashsng 13020 |
. . . . . . . . 9
⊢ (∪ 𝑧
∈ V → (#‘{∪ 𝑧}) = 1) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . 8
⊢
(#‘{∪ 𝑧}) = 1 |
69 | 65, 68 | syl6eq 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → (#‘𝑧) = 1) |
70 | 69 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(#‘𝑧) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)1) |
71 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} ⊆ 𝑌 |
72 | 6, 71 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ 𝑍 ⊆ 𝑌 |
73 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ Fin) |
74 | 5, 72, 73 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ Fin) |
75 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝑍 ∈ Fin →
(#‘𝑍) ∈
ℕ0) |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑍) ∈
ℕ0) |
77 | 76 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑍) ∈ ℂ) |
78 | 77 | mulid1d 9936 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝑍) · 1) = (#‘𝑍)) |
79 | 6, 5 | rabexd 4741 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ V) |
80 | | inss2 3796 |
. . . . . . . . . . 11
⊢ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ⊆ 𝒫 𝑍 |
81 | | pwexg 4776 |
. . . . . . . . . . . 12
⊢ (𝑍 ∈ Fin → 𝒫
𝑍 ∈
V) |
82 | 74, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝒫 𝑍 ∈ V) |
83 | | ssexg 4732 |
. . . . . . . . . . 11
⊢ ((((𝑌 / ∼ ) ∩ 𝒫
𝑍) ⊆ 𝒫 𝑍 ∧ 𝒫 𝑍 ∈ V) → ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈
V) |
84 | 80, 82, 83 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈
V) |
85 | 7 | relopabi 5167 |
. . . . . . . . . . . . . . . . 17
⊢ Rel ∼ |
86 | | relssdmrn 5573 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
∼
→ ∼ ⊆ (dom ∼
× ran ∼ )) |
87 | 85, 86 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ∼
⊆ (dom ∼ × ran ∼
) |
88 | | erdm 7639 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( ∼ Er
𝑌 → dom ∼ =
𝑌) |
89 | 21, 88 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom ∼ = 𝑌) |
90 | 89, 5 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom ∼ ∈
Fin) |
91 | | errn 7651 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( ∼ Er
𝑌 → ran ∼ =
𝑌) |
92 | 21, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ran ∼ = 𝑌) |
93 | 92, 5 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran ∼ ∈
Fin) |
94 | | xpexg 6858 |
. . . . . . . . . . . . . . . . 17
⊢ ((dom
∼
∈ Fin ∧ ran ∼ ∈ Fin) →
(dom ∼ × ran ∼ )
∈ V) |
95 | 90, 93, 94 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (dom ∼ × ran ∼ )
∈ V) |
96 | | ssexg 4732 |
. . . . . . . . . . . . . . . 16
⊢ (( ∼
⊆ (dom ∼ × ran ∼ )
∧ (dom ∼ × ran ∼ )
∈ V) → ∼ ∈
V) |
97 | 87, 95, 96 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∼ ∈
V) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∼ ∈
V) |
99 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍) |
100 | 72, 99 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑌) |
101 | | ecelqsg 7689 |
. . . . . . . . . . . . . 14
⊢ (( ∼ ∈
V ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈ (𝑌 / ∼ )) |
102 | 98, 100, 101 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ∈ (𝑌 / ∼ )) |
103 | 54, 102 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ (𝑌 / ∼ )) |
104 | | snelpwi 4839 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝑍 → {𝑤} ∈ 𝒫 𝑍) |
105 | 104 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ 𝒫 𝑍) |
106 | 103, 105 | elind 3760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) |
107 | 106 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ 𝑍 → {𝑤} ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) |
108 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) |
109 | 80, 108 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ∈ 𝒫 𝑍) |
110 | 109 | elpwid 4118 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → 𝑧 ⊆ 𝑍) |
111 | 64, 110 | eqsstr3d 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → {∪ 𝑧}
⊆ 𝑍) |
112 | 66 | snss 4259 |
. . . . . . . . . . . 12
⊢ (∪ 𝑧
∈ 𝑍 ↔ {∪ 𝑧}
⊆ 𝑍) |
113 | 111, 112 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → ∪ 𝑧
∈ 𝑍) |
114 | 113 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) → ∪ 𝑧
∈ 𝑍)) |
115 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ∪
𝑧 → {𝑤} = {∪ 𝑧}) |
116 | 115 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∪
𝑧 → (𝑧 = {𝑤} ↔ 𝑧 = {∪ 𝑧})) |
117 | 64, 116 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → (𝑤 = ∪
𝑧 → 𝑧 = {𝑤})) |
118 | 117 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) → (𝑤 = ∪
𝑧 → 𝑧 = {𝑤})) |
119 | | unieq 4380 |
. . . . . . . . . . . . 13
⊢ (𝑧 = {𝑤} → ∪ 𝑧 = ∪
{𝑤}) |
120 | 49 | unisn 4387 |
. . . . . . . . . . . . 13
⊢ ∪ {𝑤}
= 𝑤 |
121 | 119, 120 | syl6req 2661 |
. . . . . . . . . . . 12
⊢ (𝑧 = {𝑤} → 𝑤 = ∪ 𝑧) |
122 | 118, 121 | impbid1 214 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) → (𝑤 = ∪
𝑧 ↔ 𝑧 = {𝑤})) |
123 | 122 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) → (𝑤 = ∪
𝑧 ↔ 𝑧 = {𝑤}))) |
124 | 79, 84, 107, 114, 123 | en3d 7878 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ≈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)) |
125 | | hashen 12997 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ Fin ∧ ((𝑌 / ∼ ) ∩ 𝒫
𝑍) ∈ Fin) →
((#‘𝑍) =
(#‘((𝑌 / ∼ )
∩ 𝒫 𝑍)) ↔
𝑍 ≈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) |
126 | 74, 35, 125 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝑍) = (#‘((𝑌 / ∼ ) ∩ 𝒫
𝑍)) ↔ 𝑍 ≈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍))) |
127 | 124, 126 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑍) = (#‘((𝑌 / ∼ ) ∩ 𝒫
𝑍))) |
128 | 127 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝑍) · 1) =
((#‘((𝑌 /
∼
) ∩ 𝒫 𝑍))
· 1)) |
129 | 78, 128 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → (#‘𝑍) = ((#‘((𝑌 / ∼ ) ∩ 𝒫
𝑍)) ·
1)) |
130 | 38, 70, 129 | 3eqtr4rd 2655 |
. . . . 5
⊢ (𝜑 → (#‘𝑍) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(#‘𝑧)) |
131 | 130 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → ((#‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧)) = (Σ𝑧 ∈ ((𝑌 / ∼ ) ∩ 𝒫
𝑍)(#‘𝑧) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧))) |
132 | 31, 32, 131 | 3eqtr4rd 2655 |
. . 3
⊢ (𝜑 → ((#‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧)) = (#‘𝑌)) |
133 | | hashcl 13009 |
. . . . . 6
⊢ (𝑌 ∈ Fin →
(#‘𝑌) ∈
ℕ0) |
134 | 5, 133 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝑌) ∈
ℕ0) |
135 | 134 | nn0cnd 11230 |
. . . 4
⊢ (𝜑 → (#‘𝑌) ∈ ℂ) |
136 | | diffi 8077 |
. . . . . 6
⊢ ((𝑌 / ∼ ) ∈ Fin →
((𝑌 / ∼ )
∖ 𝒫 𝑍) ∈
Fin) |
137 | 23, 136 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫
𝑍) ∈
Fin) |
138 | | eldifi 3694 |
. . . . . 6
⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍) → 𝑧 ∈ (𝑌 / ∼ )) |
139 | 138, 30 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) → (#‘𝑧) ∈
ℂ) |
140 | 137, 139 | fsumcl 14311 |
. . . 4
⊢ (𝜑 → Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧) ∈
ℂ) |
141 | 135, 77, 140 | subaddd 10289 |
. . 3
⊢ (𝜑 → (((#‘𝑌) − (#‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧) ↔ ((#‘𝑍) + Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧)) = (#‘𝑌))) |
142 | 132, 141 | mpbird 246 |
. 2
⊢ (𝜑 → ((#‘𝑌) − (#‘𝑍)) = Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(#‘𝑧)) |
143 | 8, 142 | breqtrrd 4611 |
1
⊢ (𝜑 → 𝑃 ∥ ((#‘𝑌) − (#‘𝑍))) |