Proof of Theorem cusgrasizeinds
Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25987 |
. . . 4
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | usgrafis 25944 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝐸 ∈ Fin) |
3 | 2 | a1d 25 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝑁 ∈ 𝑉 → 𝐸 ∈ Fin)) |
4 | 3 | ex 449 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → 𝐸 ∈ Fin))) |
5 | 1, 4 | syl 17 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 ∈ Fin → (𝑁 ∈ 𝑉 → 𝐸 ∈ Fin))) |
6 | 5 | 3imp 1249 |
. 2
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → 𝐸 ∈ Fin) |
7 | | usgrafun 25878 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
8 | 1, 7 | syl 17 |
. . . . . 6
⊢ (𝑉 ComplUSGrph 𝐸 → Fun 𝐸) |
9 | 8 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → Fun 𝐸) |
10 | 9 | adantr 480 |
. . . 4
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → Fun 𝐸) |
11 | | hashfun 13084 |
. . . . 5
⊢ (𝐸 ∈ Fin → (Fun 𝐸 ↔ (#‘𝐸) = (#‘dom 𝐸))) |
12 | 11 | adantl 481 |
. . . 4
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (Fun 𝐸 ↔ (#‘𝐸) = (#‘dom 𝐸))) |
13 | 10, 12 | mpbid 221 |
. . 3
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘𝐸) = (#‘dom 𝐸)) |
14 | | cusgrares.f |
. . . . . . 7
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) |
15 | 14 | usgrafilem1 25940 |
. . . . . 6
⊢ dom 𝐸 = (dom 𝐹 ∪ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) |
16 | 15 | a1i 11 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → dom 𝐸 = (dom 𝐹 ∪ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) |
17 | 16 | fveq2d 6107 |
. . . 4
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘dom 𝐸) = (#‘(dom 𝐹 ∪ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}))) |
18 | | finresfin 8071 |
. . . . . . . 8
⊢ (𝐸 ∈ Fin → (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ∈ Fin) |
19 | 14, 18 | syl5eqel 2692 |
. . . . . . 7
⊢ (𝐸 ∈ Fin → 𝐹 ∈ Fin) |
20 | | dmfi 8129 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → dom 𝐹 ∈ Fin) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝐸 ∈ Fin → dom 𝐹 ∈ Fin) |
22 | 21 | adantl 481 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → dom 𝐹 ∈ Fin) |
23 | | dmfi 8129 |
. . . . . . 7
⊢ (𝐸 ∈ Fin → dom 𝐸 ∈ Fin) |
24 | | rabfi 8070 |
. . . . . . 7
⊢ (dom
𝐸 ∈ Fin → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ Fin) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ (𝐸 ∈ Fin → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ Fin) |
26 | 25 | adantl 481 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ Fin) |
27 | 14 | cusgrasizeindslem1 26002 |
. . . . . 6
⊢ (dom
𝐹 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ∅ |
28 | 27 | a1i 11 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (dom 𝐹 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ∅) |
29 | | hashun 13032 |
. . . . 5
⊢ ((dom
𝐹 ∈ Fin ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)} ∈ Fin ∧ (dom 𝐹 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ∅) → (#‘(dom 𝐹 ∪ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) = ((#‘dom 𝐹) + (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}))) |
30 | 22, 26, 28, 29 | syl3anc 1318 |
. . . 4
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘(dom 𝐹 ∪ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) = ((#‘dom 𝐹) + (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}))) |
31 | 14 | cusgrasizeindslem2 26003 |
. . . . . . 7
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ((#‘𝑉) − 1)) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ((#‘𝑉) − 1)) |
33 | 32 | oveq2d 6565 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → ((#‘dom 𝐹) + (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) = ((#‘dom 𝐹) + ((#‘𝑉) − 1))) |
34 | | hashcl 13009 |
. . . . . . . . 9
⊢ (dom
𝐹 ∈ Fin →
(#‘dom 𝐹) ∈
ℕ0) |
35 | 34 | nn0cnd 11230 |
. . . . . . . 8
⊢ (dom
𝐹 ∈ Fin →
(#‘dom 𝐹) ∈
ℂ) |
36 | 19, 20, 35 | 3syl 18 |
. . . . . . 7
⊢ (𝐸 ∈ Fin → (#‘dom
𝐹) ∈
ℂ) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘dom 𝐹) ∈
ℂ) |
38 | | hashcl 13009 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
39 | | nn0cn 11179 |
. . . . . . . . . 10
⊢
((#‘𝑉) ∈
ℕ0 → (#‘𝑉) ∈ ℂ) |
40 | | 1cnd 9935 |
. . . . . . . . . 10
⊢
((#‘𝑉) ∈
ℕ0 → 1 ∈ ℂ) |
41 | 39, 40 | subcld 10271 |
. . . . . . . . 9
⊢
((#‘𝑉) ∈
ℕ0 → ((#‘𝑉) − 1) ∈
ℂ) |
42 | 38, 41 | syl 17 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((#‘𝑉) − 1)
∈ ℂ) |
43 | 42 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘𝑉) − 1) ∈
ℂ) |
44 | 43 | adantr 480 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → ((#‘𝑉) − 1) ∈
ℂ) |
45 | 37, 44 | addcomd 10117 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → ((#‘dom 𝐹) + ((#‘𝑉) − 1)) = (((#‘𝑉) − 1) + (#‘dom 𝐹))) |
46 | 33, 45 | eqtrd 2644 |
. . . 4
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → ((#‘dom 𝐹) + (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)})) = (((#‘𝑉) − 1) + (#‘dom 𝐹))) |
47 | 17, 30, 46 | 3eqtrd 2648 |
. . 3
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘dom 𝐸) = (((#‘𝑉) − 1) + (#‘dom 𝐹))) |
48 | 14 | cusgrares 26001 |
. . . . . . . . 9
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) ComplUSGrph 𝐹) |
49 | | cusisusgra 25987 |
. . . . . . . . 9
⊢ ((𝑉 ∖ {𝑁}) ComplUSGrph 𝐹 → (𝑉 ∖ {𝑁}) USGrph 𝐹) |
50 | | usgrafun 25878 |
. . . . . . . . 9
⊢ ((𝑉 ∖ {𝑁}) USGrph 𝐹 → Fun 𝐹) |
51 | 48, 49, 50 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → Fun 𝐹) |
52 | 51 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → Fun 𝐹) |
53 | 52 | adantr 480 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → Fun 𝐹) |
54 | 19 | adantl 481 |
. . . . . . 7
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → 𝐹 ∈ Fin) |
55 | | hashfun 13084 |
. . . . . . 7
⊢ (𝐹 ∈ Fin → (Fun 𝐹 ↔ (#‘𝐹) = (#‘dom 𝐹))) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (Fun 𝐹 ↔ (#‘𝐹) = (#‘dom 𝐹))) |
57 | 53, 56 | mpbid 221 |
. . . . 5
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘𝐹) = (#‘dom 𝐹)) |
58 | 57 | eqcomd 2616 |
. . . 4
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘dom 𝐹) = (#‘𝐹)) |
59 | 58 | oveq2d 6565 |
. . 3
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (((#‘𝑉) − 1) + (#‘dom
𝐹)) = (((#‘𝑉) − 1) + (#‘𝐹))) |
60 | 13, 47, 59 | 3eqtrd 2648 |
. 2
⊢ (((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) ∧ 𝐸 ∈ Fin) → (#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹))) |
61 | 6, 60 | mpdan 699 |
1
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹))) |