Step |
Hyp |
Ref |
Expression |
1 |
|
finsumvtxdg2sstep.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
finsumvtxdg2sstep.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
|
finsumvtxdg2sstep.k |
⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } ) |
4 |
|
finsumvtxdg2sstep.i |
⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) } |
5 |
|
finsumvtxdg2sstep.p |
⊢ 𝑃 = ( 𝐸 ↾ 𝐼 ) |
6 |
|
finsumvtxdg2sstep.s |
⊢ 𝑆 = 〈 𝐾 , 𝑃 〉 |
7 |
|
finsumvtxdg2ssteplem.j |
⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } |
8 |
|
dmfi |
⊢ ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin ) |
9 |
8
|
adantl |
⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → dom 𝐸 ∈ Fin ) |
10 |
|
simpr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 ) |
11 |
|
eqid |
⊢ dom 𝐸 = dom 𝐸 |
12 |
1 2 11
|
vtxdgfival |
⊢ ( ( dom 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) |
13 |
9 10 12
|
syl2anr |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) |
14 |
7
|
eqcomi |
⊢ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } = 𝐽 |
15 |
14
|
fveq2i |
⊢ ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) = ( ♯ ‘ 𝐽 ) |
16 |
15
|
a1i |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) = ( ♯ ‘ 𝐽 ) ) |
17 |
16
|
oveq1d |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) |
18 |
13 17
|
eqtrd |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) |