Metamath Proof Explorer

Theorem vtxdginducedm1fi

Description: The degree of a vertex v in the induced subgraph S of a pseudograph G of finite size obtained by removing one vertex N plus the number of edges joining the vertex v and the vertex N is the degree of the vertex v in the pseudograph G . (Contributed by AV, 18-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v 
|- V = ( Vtx ` G )
vtxdginducedm1.e 
|- E = ( iEdg ` G )
vtxdginducedm1.k 
|- K = ( V \ { N } )
vtxdginducedm1.i 
|- I = { i e. dom E | N e/ ( E ` i ) }
vtxdginducedm1.p 
|- P = ( E |` I )
vtxdginducedm1.s 
|- S = <. K , P >.
vtxdginducedm1.j 
|- J = { i e. dom E | N e. ( E ` i ) }
Assertion vtxdginducedm1fi 
|- ( E e. Fin -> A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { l e. J | v e. ( E ` l ) } ) ) )

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v 
 |-  V = ( Vtx ` G )
2 vtxdginducedm1.e 
 |-  E = ( iEdg ` G )
3 vtxdginducedm1.k 
 |-  K = ( V \ { N } )
4 vtxdginducedm1.i 
 |-  I = { i e. dom E | N e/ ( E ` i ) }
5 vtxdginducedm1.p 
 |-  P = ( E |` I )
6 vtxdginducedm1.s 
 |-  S = <. K , P >.
7 vtxdginducedm1.j 
 |-  J = { i e. dom E | N e. ( E ` i ) }
8 1 2 3 4 5 6 7 vtxdginducedm1 
 |-  A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) )
9 5 dmeqi 
 |-  dom P = dom ( E |` I )
10 finresfin 
 |-  ( E e. Fin -> ( E |` I ) e. Fin )
11 dmfi 
 |-  ( ( E |` I ) e. Fin -> dom ( E |` I ) e. Fin )
12 10 11 syl 
 |-  ( E e. Fin -> dom ( E |` I ) e. Fin )
13 9 12 eqeltrid 
 |-  ( E e. Fin -> dom P e. Fin )
14 6 fveq2i 
 |-  ( Vtx ` S ) = ( Vtx ` <. K , P >. )
15 1 fvexi 
 |-  V e. _V
16 15 difexi 
 |-  ( V \ { N } ) e. _V
17 3 16 eqeltri 
 |-  K e. _V
18 2 fvexi 
 |-  E e. _V
19 18 resex 
 |-  ( E |` I ) e. _V
20 5 19 eqeltri 
 |-  P e. _V
21 17 20 opvtxfvi 
 |-  ( Vtx ` <. K , P >. ) = K
22 14 21 3 3eqtrri 
 |-  ( V \ { N } ) = ( Vtx ` S )
23 1 2 3 4 5 6 vtxdginducedm1lem1 
 |-  ( iEdg ` S ) = P
24 23 eqcomi 
 |-  P = ( iEdg ` S )
25 eqid 
 |-  dom P = dom P
26 22 24 25 vtxdgfisnn0 
 |-  ( ( dom P e. Fin /\ v e. ( V \ { N } ) ) -> ( ( VtxDeg ` S ) ` v ) e. NN0 )
27 13 26 sylan 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( ( VtxDeg ` S ) ` v ) e. NN0 )
28 27 nn0red 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( ( VtxDeg ` S ) ` v ) e. RR )
29 dmfi 
 |-  ( E e. Fin -> dom E e. Fin )
30 rabfi 
 |-  ( dom E e. Fin -> { i e. dom E | N e. ( E ` i ) } e. Fin )
31 29 30 syl 
 |-  ( E e. Fin -> { i e. dom E | N e. ( E ` i ) } e. Fin )
32 7 31 eqeltrid 
 |-  ( E e. Fin -> J e. Fin )
33 rabfi 
 |-  ( J e. Fin -> { l e. J | v e. ( E ` l ) } e. Fin )
34 hashcl 
 |-  ( { l e. J | v e. ( E ` l ) } e. Fin -> ( # ` { l e. J | v e. ( E ` l ) } ) e. NN0 )
35 32 33 34 3syl 
 |-  ( E e. Fin -> ( # ` { l e. J | v e. ( E ` l ) } ) e. NN0 )
36 35 adantr 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( # ` { l e. J | v e. ( E ` l ) } ) e. NN0 )
37 36 nn0red 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( # ` { l e. J | v e. ( E ` l ) } ) e. RR )
38 28 37 rexaddd 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { l e. J | v e. ( E ` l ) } ) ) )
39 38 eqeq2d 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) <-> ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { l e. J | v e. ( E ` l ) } ) ) ) )
40 39 biimpd 
 |-  ( ( E e. Fin /\ v e. ( V \ { N } ) ) -> ( ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) -> ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { l e. J | v e. ( E ` l ) } ) ) ) )
41 40 ralimdva 
 |-  ( E e. Fin -> ( A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) +e ( # ` { l e. J | v e. ( E ` l ) } ) ) -> A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { l e. J | v e. ( E ` l ) } ) ) ) )
42 8 41 mpi 
 |-  ( E e. Fin -> A. v e. ( V \ { N } ) ( ( VtxDeg ` G ) ` v ) = ( ( ( VtxDeg ` S ) ` v ) + ( # ` { l e. J | v e. ( E ` l ) } ) ) )