Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdginducedm1.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
vtxdginducedm1.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
|
vtxdginducedm1.k |
⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } ) |
4 |
|
vtxdginducedm1.i |
⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) } |
5 |
|
vtxdginducedm1.p |
⊢ 𝑃 = ( 𝐸 ↾ 𝐼 ) |
6 |
|
vtxdginducedm1.s |
⊢ 𝑆 = 〈 𝐾 , 𝑃 〉 |
7 |
|
vtxdginducedm1.j |
⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } |
8 |
1 2 3 4 5 6 7
|
vtxdginducedm1 |
⊢ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) |
9 |
5
|
dmeqi |
⊢ dom 𝑃 = dom ( 𝐸 ↾ 𝐼 ) |
10 |
|
finresfin |
⊢ ( 𝐸 ∈ Fin → ( 𝐸 ↾ 𝐼 ) ∈ Fin ) |
11 |
|
dmfi |
⊢ ( ( 𝐸 ↾ 𝐼 ) ∈ Fin → dom ( 𝐸 ↾ 𝐼 ) ∈ Fin ) |
12 |
10 11
|
syl |
⊢ ( 𝐸 ∈ Fin → dom ( 𝐸 ↾ 𝐼 ) ∈ Fin ) |
13 |
9 12
|
eqeltrid |
⊢ ( 𝐸 ∈ Fin → dom 𝑃 ∈ Fin ) |
14 |
6
|
fveq2i |
⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 〈 𝐾 , 𝑃 〉 ) |
15 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
16 |
15
|
difexi |
⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V |
17 |
3 16
|
eqeltri |
⊢ 𝐾 ∈ V |
18 |
2
|
fvexi |
⊢ 𝐸 ∈ V |
19 |
18
|
resex |
⊢ ( 𝐸 ↾ 𝐼 ) ∈ V |
20 |
5 19
|
eqeltri |
⊢ 𝑃 ∈ V |
21 |
17 20
|
opvtxfvi |
⊢ ( Vtx ‘ 〈 𝐾 , 𝑃 〉 ) = 𝐾 |
22 |
14 21 3
|
3eqtrri |
⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 ) |
23 |
1 2 3 4 5 6
|
vtxdginducedm1lem1 |
⊢ ( iEdg ‘ 𝑆 ) = 𝑃 |
24 |
23
|
eqcomi |
⊢ 𝑃 = ( iEdg ‘ 𝑆 ) |
25 |
|
eqid |
⊢ dom 𝑃 = dom 𝑃 |
26 |
22 24 25
|
vtxdgfisnn0 |
⊢ ( ( dom 𝑃 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℕ0 ) |
27 |
13 26
|
sylan |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℕ0 ) |
28 |
27
|
nn0red |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℝ ) |
29 |
|
dmfi |
⊢ ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin ) |
30 |
|
rabfi |
⊢ ( dom 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin ) |
31 |
29 30
|
syl |
⊢ ( 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin ) |
32 |
7 31
|
eqeltrid |
⊢ ( 𝐸 ∈ Fin → 𝐽 ∈ Fin ) |
33 |
|
rabfi |
⊢ ( 𝐽 ∈ Fin → { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ∈ Fin ) |
34 |
|
hashcl |
⊢ ( { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ∈ Fin → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℕ0 ) |
35 |
32 33 34
|
3syl |
⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℕ0 ) |
36 |
35
|
adantr |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℕ0 ) |
37 |
36
|
nn0red |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℝ ) |
38 |
28 37
|
rexaddd |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) |
39 |
38
|
eqeq2d |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) ) |
40 |
39
|
biimpd |
⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) ) |
41 |
40
|
ralimdva |
⊢ ( 𝐸 ∈ Fin → ( ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) ) |
42 |
8 41
|
mpi |
⊢ ( 𝐸 ∈ Fin → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) |