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 |
7
|
rabeq2i |
⊢ ( 𝑖 ∈ 𝐽 ↔ ( 𝑖 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) ) |
9 |
8
|
anbi1i |
⊢ ( ( 𝑖 ∈ 𝐽 ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( ( 𝑖 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ) |
10 |
|
anass |
⊢ ( ( ( 𝑖 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) |
11 |
9 10
|
bitri |
⊢ ( ( 𝑖 ∈ 𝐽 ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ) ) |
12 |
11
|
rabbia2 |
⊢ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } |
13 |
12
|
fveq2i |
⊢ ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) |
14 |
13
|
a1i |
⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) ) |
15 |
14
|
sumeq2dv |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) = Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) ) |
16 |
15
|
oveq1d |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) |
17 |
|
simpll |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝐺 ∈ UPGraph ) |
18 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) |
19 |
|
simplr |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝑁 ∈ 𝑉 ) |
20 |
1 2
|
numedglnl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) |
21 |
17 18 19 20
|
syl3anc |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) |
22 |
16 21
|
eqtrd |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) |
23 |
7
|
fveq2i |
⊢ ( ♯ ‘ 𝐽 ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) |
24 |
22 23
|
eqtr4di |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ 𝐽 ) ) |