Metamath Proof Explorer

Theorem p1evtxdeq

Description: If an edge E which does not contain vertex U is added to a graph G (yielding a graph F ), the degree of U is the same in both graphs. (Contributed by AV, 2-Mar-2021)

Ref Expression
Hypotheses p1evtxdeq.v 
|- V = ( Vtx ` G )
p1evtxdeq.i 
|- I = ( iEdg ` G )
p1evtxdeq.f 
|- ( ph -> Fun I )
p1evtxdeq.fv 
|- ( ph -> ( Vtx ` F ) = V )
p1evtxdeq.fi 
|- ( ph -> ( iEdg ` F ) = ( I u. { <. K , E >. } ) )
p1evtxdeq.k 
|- ( ph -> K e. X )
p1evtxdeq.d 
|- ( ph -> K e/ dom I )
p1evtxdeq.u 
|- ( ph -> U e. V )
p1evtxdeq.e 
|- ( ph -> E e. Y )
p1evtxdeq.n 
|- ( ph -> U e/ E )
Assertion p1evtxdeq 
|- ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( VtxDeg ` G ) ` U ) )

Proof

Step Hyp Ref Expression
1 p1evtxdeq.v 
 |-  V = ( Vtx ` G )
2 p1evtxdeq.i 
 |-  I = ( iEdg ` G )
3 p1evtxdeq.f 
 |-  ( ph -> Fun I )
4 p1evtxdeq.fv 
 |-  ( ph -> ( Vtx ` F ) = V )
5 p1evtxdeq.fi 
 |-  ( ph -> ( iEdg ` F ) = ( I u. { <. K , E >. } ) )
6 p1evtxdeq.k 
 |-  ( ph -> K e. X )
7 p1evtxdeq.d 
 |-  ( ph -> K e/ dom I )
8 p1evtxdeq.u 
 |-  ( ph -> U e. V )
9 p1evtxdeq.e 
 |-  ( ph -> E e. Y )
10 p1evtxdeq.n 
 |-  ( ph -> U e/ E )
11 1 2 3 4 5 6 7 8 9 p1evtxdeqlem 
 |-  ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) )
12 1 fvexi 
 |-  V e. _V
13 snex 
 |-  { <. K , E >. } e. _V
14 12 13 pm3.2i 
 |-  ( V e. _V /\ { <. K , E >. } e. _V )
15 opiedgfv 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( iEdg ` <. V , { <. K , E >. } >. ) = { <. K , E >. } )
16 14 15 mp1i 
 |-  ( ph -> ( iEdg ` <. V , { <. K , E >. } >. ) = { <. K , E >. } )
17 opvtxfv 
 |-  ( ( V e. _V /\ { <. K , E >. } e. _V ) -> ( Vtx ` <. V , { <. K , E >. } >. ) = V )
18 14 17 mp1i 
 |-  ( ph -> ( Vtx ` <. V , { <. K , E >. } >. ) = V )
19 16 18 6 8 9 10 1hevtxdg0 
 |-  ( ph -> ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) = 0 )
20 19 oveq2d 
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` U ) +e ( ( VtxDeg ` <. V , { <. K , E >. } >. ) ` U ) ) = ( ( ( VtxDeg ` G ) ` U ) +e 0 ) )
21 1 vtxdgelxnn0 
 |-  ( U e. V -> ( ( VtxDeg ` G ) ` U ) e. NN0* )
22 xnn0xr 
 |-  ( ( ( VtxDeg ` G ) ` U ) e. NN0* -> ( ( VtxDeg ` G ) ` U ) e. RR* )
23 8 21 22 3syl 
 |-  ( ph -> ( ( VtxDeg ` G ) ` U ) e. RR* )
24 23 xaddid1d 
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` U ) +e 0 ) = ( ( VtxDeg ` G ) ` U ) )
25 11 20 24 3eqtrd 
 |-  ( ph -> ( ( VtxDeg ` F ) ` U ) = ( ( VtxDeg ` G ) ` U ) )