Proof of Theorem vdegp1ai
Step | Hyp | Ref
| Expression |
1 | | vdegp1ai.f |
. . . . 5
⊢ 𝐹 = (𝐸 ++ 〈“{𝑋, 𝑌}”〉) |
2 | | vdegp1ai.1 |
. . . . . . 7
⊢ (⊤
→ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
3 | 2 | trud 1484 |
. . . . . 6
⊢ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} |
4 | | vdeg0i.v |
. . . . . . . 8
⊢ 𝑉 ∈ V |
5 | | vdegp1ai.3 |
. . . . . . . 8
⊢ 𝑋 ∈ 𝑉 |
6 | | vdegp1ai.5 |
. . . . . . . 8
⊢ 𝑌 ∈ 𝑉 |
7 | 4, 5, 6 | umgrabi 26510 |
. . . . . . 7
⊢ (⊤
→ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
8 | 7 | trud 1484 |
. . . . . 6
⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} |
9 | | cats1un 13327 |
. . . . . 6
⊢ ((𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ∧ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) → (𝐸 ++ 〈“{𝑋, 𝑌}”〉) = (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉})) |
10 | 3, 8, 9 | mp2an 704 |
. . . . 5
⊢ (𝐸 ++ 〈“{𝑋, 𝑌}”〉) = (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉}) |
11 | 1, 10 | eqtri 2632 |
. . . 4
⊢ 𝐹 = (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉}) |
12 | 11 | oveq2i 6560 |
. . 3
⊢ (𝑉 VDeg 𝐹) = (𝑉 VDeg (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉})) |
13 | 12 | fveq1i 6104 |
. 2
⊢ ((𝑉 VDeg 𝐹)‘𝑈) = ((𝑉 VDeg (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉}))‘𝑈) |
14 | | wrdf 13165 |
. . . . . . 7
⊢ (𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → 𝐸:(0..^(#‘𝐸))⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
15 | | ffn 5958 |
. . . . . . 7
⊢ (𝐸:(0..^(#‘𝐸))⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → 𝐸 Fn (0..^(#‘𝐸))) |
16 | 3, 14, 15 | mp2b 10 |
. . . . . 6
⊢ 𝐸 Fn (0..^(#‘𝐸)) |
17 | 16 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝐸 Fn
(0..^(#‘𝐸))) |
18 | | fvex 6113 |
. . . . . . 7
⊢
(#‘𝐸) ∈
V |
19 | | prex 4836 |
. . . . . . 7
⊢ {𝑋, 𝑌} ∈ V |
20 | 18, 19 | f1osn 6088 |
. . . . . 6
⊢
{〈(#‘𝐸),
{𝑋, 𝑌}〉}:{(#‘𝐸)}–1-1-onto→{{𝑋, 𝑌}} |
21 | | f1ofn 6051 |
. . . . . 6
⊢
({〈(#‘𝐸),
{𝑋, 𝑌}〉}:{(#‘𝐸)}–1-1-onto→{{𝑋, 𝑌}} → {〈(#‘𝐸), {𝑋, 𝑌}〉} Fn {(#‘𝐸)}) |
22 | 20, 21 | mp1i 13 |
. . . . 5
⊢ (⊤
→ {〈(#‘𝐸),
{𝑋, 𝑌}〉} Fn {(#‘𝐸)}) |
23 | | fzofi 12635 |
. . . . . 6
⊢
(0..^(#‘𝐸))
∈ Fin |
24 | 23 | a1i 11 |
. . . . 5
⊢ (⊤
→ (0..^(#‘𝐸))
∈ Fin) |
25 | | snfi 7923 |
. . . . . 6
⊢
{(#‘𝐸)} ∈
Fin |
26 | 25 | a1i 11 |
. . . . 5
⊢ (⊤
→ {(#‘𝐸)} ∈
Fin) |
27 | | fzonel 12352 |
. . . . . . 7
⊢ ¬
(#‘𝐸) ∈
(0..^(#‘𝐸)) |
28 | | disjsn 4192 |
. . . . . . 7
⊢
(((0..^(#‘𝐸))
∩ {(#‘𝐸)}) =
∅ ↔ ¬ (#‘𝐸) ∈ (0..^(#‘𝐸))) |
29 | 27, 28 | mpbir 220 |
. . . . . 6
⊢
((0..^(#‘𝐸))
∩ {(#‘𝐸)}) =
∅ |
30 | 29 | a1i 11 |
. . . . 5
⊢ (⊤
→ ((0..^(#‘𝐸))
∩ {(#‘𝐸)}) =
∅) |
31 | | wrdumgra 25845 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) → (𝑉 UMGrph 𝐸 ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
32 | 4, 3, 31 | mp2an 704 |
. . . . . 6
⊢ (𝑉 UMGrph 𝐸 ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
33 | 2, 32 | sylibr 223 |
. . . . 5
⊢ (⊤
→ 𝑉 UMGrph 𝐸) |
34 | | umgra1 25855 |
. . . . . . 7
⊢ (((𝑉 ∈ V ∧ (#‘𝐸) ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑉 UMGrph {〈(#‘𝐸), {𝑋, 𝑌}〉}) |
35 | 4, 18, 5, 6, 34 | mp4an 705 |
. . . . . 6
⊢ 𝑉 UMGrph {〈(#‘𝐸), {𝑋, 𝑌}〉} |
36 | 35 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑉 UMGrph
{〈(#‘𝐸), {𝑋, 𝑌}〉}) |
37 | | vdegp1ai.u |
. . . . . 6
⊢ 𝑈 ∈ 𝑉 |
38 | 37 | a1i 11 |
. . . . 5
⊢ (⊤
→ 𝑈 ∈ 𝑉) |
39 | 17, 22, 24, 26, 30, 33, 36, 38 | vdgrfiun 26429 |
. . . 4
⊢ (⊤
→ ((𝑉 VDeg (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉}))‘𝑈) = (((𝑉 VDeg 𝐸)‘𝑈) + ((𝑉 VDeg {〈(#‘𝐸), {𝑋, 𝑌}〉})‘𝑈))) |
40 | 39 | trud 1484 |
. . 3
⊢ ((𝑉 VDeg (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉}))‘𝑈) = (((𝑉 VDeg 𝐸)‘𝑈) + ((𝑉 VDeg {〈(#‘𝐸), {𝑋, 𝑌}〉})‘𝑈)) |
41 | 4 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝑉 ∈
V) |
42 | 18 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (#‘𝐸) ∈
V) |
43 | 5 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝑋 ∈ 𝑉) |
44 | | vdegp1ai.4 |
. . . . . . 7
⊢ 𝑋 ≠ 𝑈 |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝑋 ≠ 𝑈) |
46 | 6 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝑌 ∈ 𝑉) |
47 | | vdegp1ai.6 |
. . . . . . 7
⊢ 𝑌 ≠ 𝑈 |
48 | 47 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 𝑌 ≠ 𝑈) |
49 | 41, 42, 38, 43, 45, 46, 48 | vdgr1a 26433 |
. . . . 5
⊢ (⊤
→ ((𝑉 VDeg
{〈(#‘𝐸), {𝑋, 𝑌}〉})‘𝑈) = 0) |
50 | 49 | trud 1484 |
. . . 4
⊢ ((𝑉 VDeg {〈(#‘𝐸), {𝑋, 𝑌}〉})‘𝑈) = 0 |
51 | 50 | oveq2i 6560 |
. . 3
⊢ (((𝑉 VDeg 𝐸)‘𝑈) + ((𝑉 VDeg {〈(#‘𝐸), {𝑋, 𝑌}〉})‘𝑈)) = (((𝑉 VDeg 𝐸)‘𝑈) + 0) |
52 | | vdgrfif 26426 |
. . . . . . . 8
⊢ ((𝑉 ∈ V ∧ 𝐸 Fn (0..^(#‘𝐸)) ∧ (0..^(#‘𝐸)) ∈ Fin) → (𝑉 VDeg 𝐸):𝑉⟶ℕ0) |
53 | 4, 16, 23, 52 | mp3an 1416 |
. . . . . . 7
⊢ (𝑉 VDeg 𝐸):𝑉⟶ℕ0 |
54 | 53 | ffvelrni 6266 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → ((𝑉 VDeg 𝐸)‘𝑈) ∈
ℕ0) |
55 | 37, 54 | ax-mp 5 |
. . . . 5
⊢ ((𝑉 VDeg 𝐸)‘𝑈) ∈
ℕ0 |
56 | 55 | nn0cni 11181 |
. . . 4
⊢ ((𝑉 VDeg 𝐸)‘𝑈) ∈ ℂ |
57 | 56 | addid1i 10102 |
. . 3
⊢ (((𝑉 VDeg 𝐸)‘𝑈) + 0) = ((𝑉 VDeg 𝐸)‘𝑈) |
58 | 40, 51, 57 | 3eqtri 2636 |
. 2
⊢ ((𝑉 VDeg (𝐸 ∪ {〈(#‘𝐸), {𝑋, 𝑌}〉}))‘𝑈) = ((𝑉 VDeg 𝐸)‘𝑈) |
59 | | vdegp1ai.2 |
. 2
⊢ ((𝑉 VDeg 𝐸)‘𝑈) = 𝑃 |
60 | 13, 58, 59 | 3eqtri 2636 |
1
⊢ ((𝑉 VDeg 𝐹)‘𝑈) = 𝑃 |