Metamath Proof Explorer

Theorem trlsegvdeg

Description: Formerly part of proof of eupth2lem3 : If a trail in a graph G induces a subgraph Z with the vertices V of G and the edges being the edges of the walk, and a subgraph X with the vertices V of G and the edges being the edges of the walk except the last one, and a subgraph Y with the vertices V of G and one edges being the last edge of the walk, then the vertex degree of any vertex U of G within Z is the sum of the vertex degree of U within X and the vertex degree of U within Y . Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v 
|- V = ( Vtx ` G )
trlsegvdeg.i 
|- I = ( iEdg ` G )
trlsegvdeg.f 
|- ( ph -> Fun I )
trlsegvdeg.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
trlsegvdeg.u 
|- ( ph -> U e. V )
trlsegvdeg.w 
|- ( ph -> F ( Trails ` G ) P )
trlsegvdeg.vx 
|- ( ph -> ( Vtx ` X ) = V )
trlsegvdeg.vy 
|- ( ph -> ( Vtx ` Y ) = V )
trlsegvdeg.vz 
|- ( ph -> ( Vtx ` Z ) = V )
trlsegvdeg.ix 
|- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
trlsegvdeg.iy 
|- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
trlsegvdeg.iz 
|- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
Assertion trlsegvdeg 
|- ( ph -> ( ( VtxDeg ` Z ) ` U ) = ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) )

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v 
 |-  V = ( Vtx ` G )
2 trlsegvdeg.i 
 |-  I = ( iEdg ` G )
3 trlsegvdeg.f 
 |-  ( ph -> Fun I )
4 trlsegvdeg.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 trlsegvdeg.u 
 |-  ( ph -> U e. V )
6 trlsegvdeg.w 
 |-  ( ph -> F ( Trails ` G ) P )
7 trlsegvdeg.vx 
 |-  ( ph -> ( Vtx ` X ) = V )
8 trlsegvdeg.vy 
 |-  ( ph -> ( Vtx ` Y ) = V )
9 trlsegvdeg.vz 
 |-  ( ph -> ( Vtx ` Z ) = V )
10 trlsegvdeg.ix 
 |-  ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
11 trlsegvdeg.iy 
 |-  ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
12 trlsegvdeg.iz 
 |-  ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
13 eqid 
 |-  ( iEdg ` X ) = ( iEdg ` X )
14 eqid 
 |-  ( iEdg ` Y ) = ( iEdg ` Y )
15 eqid 
 |-  ( Vtx ` X ) = ( Vtx ` X )
16 8 7 eqtr4d 
 |-  ( ph -> ( Vtx ` Y ) = ( Vtx ` X ) )
17 9 7 eqtr4d 
 |-  ( ph -> ( Vtx ` Z ) = ( Vtx ` X ) )
18 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem4 
 |-  ( ph -> dom ( iEdg ` X ) = ( ( F " ( 0 ..^ N ) ) i^i dom I ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem5 
 |-  ( ph -> dom ( iEdg ` Y ) = { ( F ` N ) } )
20 18 19 ineq12d 
 |-  ( ph -> ( dom ( iEdg ` X ) i^i dom ( iEdg ` Y ) ) = ( ( ( F " ( 0 ..^ N ) ) i^i dom I ) i^i { ( F ` N ) } ) )
21 fzonel 
 |-  -. N e. ( 0 ..^ N )
22 2 trlf1 
 |-  ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
23 6 22 syl 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
24 elfzouz2 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
25 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
26 4 24 25 3syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
27 f1elima 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ N e. ( 0 ..^ ( # ` F ) ) /\ ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) ) -> ( ( F ` N ) e. ( F " ( 0 ..^ N ) ) <-> N e. ( 0 ..^ N ) ) )
28 23 4 26 27 syl3anc 
 |-  ( ph -> ( ( F ` N ) e. ( F " ( 0 ..^ N ) ) <-> N e. ( 0 ..^ N ) ) )
29 21 28 mtbiri 
 |-  ( ph -> -. ( F ` N ) e. ( F " ( 0 ..^ N ) ) )
30 29 orcd 
 |-  ( ph -> ( -. ( F ` N ) e. ( F " ( 0 ..^ N ) ) \/ -. ( F ` N ) e. dom I ) )
31 ianor 
 |-  ( -. ( ( F ` N ) e. ( F " ( 0 ..^ N ) ) /\ ( F ` N ) e. dom I ) <-> ( -. ( F ` N ) e. ( F " ( 0 ..^ N ) ) \/ -. ( F ` N ) e. dom I ) )
32 elin 
 |-  ( ( F ` N ) e. ( ( F " ( 0 ..^ N ) ) i^i dom I ) <-> ( ( F ` N ) e. ( F " ( 0 ..^ N ) ) /\ ( F ` N ) e. dom I ) )
33 31 32 xchnxbir 
 |-  ( -. ( F ` N ) e. ( ( F " ( 0 ..^ N ) ) i^i dom I ) <-> ( -. ( F ` N ) e. ( F " ( 0 ..^ N ) ) \/ -. ( F ` N ) e. dom I ) )
34 30 33 sylibr 
 |-  ( ph -> -. ( F ` N ) e. ( ( F " ( 0 ..^ N ) ) i^i dom I ) )
35 disjsn 
 |-  ( ( ( ( F " ( 0 ..^ N ) ) i^i dom I ) i^i { ( F ` N ) } ) = (/) <-> -. ( F ` N ) e. ( ( F " ( 0 ..^ N ) ) i^i dom I ) )
36 34 35 sylibr 
 |-  ( ph -> ( ( ( F " ( 0 ..^ N ) ) i^i dom I ) i^i { ( F ` N ) } ) = (/) )
37 20 36 eqtrd 
 |-  ( ph -> ( dom ( iEdg ` X ) i^i dom ( iEdg ` Y ) ) = (/) )
38 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem2 
 |-  ( ph -> Fun ( iEdg ` X ) )
39 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem3 
 |-  ( ph -> Fun ( iEdg ` Y ) )
40 5 7 eleqtrrd 
 |-  ( ph -> U e. ( Vtx ` X ) )
41 f1f 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
42 6 22 41 3syl 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
43 3 42 4 resunimafz0 
 |-  ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )
44 10 11 uneq12d 
 |-  ( ph -> ( ( iEdg ` X ) u. ( iEdg ` Y ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )
45 43 12 44 3eqtr4d 
 |-  ( ph -> ( iEdg ` Z ) = ( ( iEdg ` X ) u. ( iEdg ` Y ) ) )
46 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem6 
 |-  ( ph -> dom ( iEdg ` X ) e. Fin )
47 1 2 3 4 5 6 7 8 9 10 11 12 trlsegvdeglem7 
 |-  ( ph -> dom ( iEdg ` Y ) e. Fin )
48 13 14 15 16 17 37 38 39 40 45 46 47 vtxdfiun 
 |-  ( ph -> ( ( VtxDeg ` Z ) ` U ) = ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) )