Metamath Proof Explorer


Theorem 1loopgrvd0

Description: The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1loopgruspgr.v
|- ( ph -> ( Vtx ` G ) = V )
1loopgruspgr.a
|- ( ph -> A e. X )
1loopgruspgr.n
|- ( ph -> N e. V )
1loopgruspgr.i
|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
1loopgrvd0.k
|- ( ph -> K e. ( V \ { N } ) )
Assertion 1loopgrvd0
|- ( ph -> ( ( VtxDeg ` G ) ` K ) = 0 )

Proof

Step Hyp Ref Expression
1 1loopgruspgr.v
 |-  ( ph -> ( Vtx ` G ) = V )
2 1loopgruspgr.a
 |-  ( ph -> A e. X )
3 1loopgruspgr.n
 |-  ( ph -> N e. V )
4 1loopgruspgr.i
 |-  ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
5 1loopgrvd0.k
 |-  ( ph -> K e. ( V \ { N } ) )
6 5 eldifbd
 |-  ( ph -> -. K e. { N } )
7 snex
 |-  { N } e. _V
8 fvsng
 |-  ( ( A e. X /\ { N } e. _V ) -> ( { <. A , { N } >. } ` A ) = { N } )
9 2 7 8 sylancl
 |-  ( ph -> ( { <. A , { N } >. } ` A ) = { N } )
10 9 eleq2d
 |-  ( ph -> ( K e. ( { <. A , { N } >. } ` A ) <-> K e. { N } ) )
11 6 10 mtbird
 |-  ( ph -> -. K e. ( { <. A , { N } >. } ` A ) )
12 4 dmeqd
 |-  ( ph -> dom ( iEdg ` G ) = dom { <. A , { N } >. } )
13 dmsnopg
 |-  ( { N } e. _V -> dom { <. A , { N } >. } = { A } )
14 7 13 mp1i
 |-  ( ph -> dom { <. A , { N } >. } = { A } )
15 12 14 eqtrd
 |-  ( ph -> dom ( iEdg ` G ) = { A } )
16 4 fveq1d
 |-  ( ph -> ( ( iEdg ` G ) ` i ) = ( { <. A , { N } >. } ` i ) )
17 16 eleq2d
 |-  ( ph -> ( K e. ( ( iEdg ` G ) ` i ) <-> K e. ( { <. A , { N } >. } ` i ) ) )
18 15 17 rexeqbidv
 |-  ( ph -> ( E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) <-> E. i e. { A } K e. ( { <. A , { N } >. } ` i ) ) )
19 fveq2
 |-  ( i = A -> ( { <. A , { N } >. } ` i ) = ( { <. A , { N } >. } ` A ) )
20 19 eleq2d
 |-  ( i = A -> ( K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
21 20 rexsng
 |-  ( A e. X -> ( E. i e. { A } K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
22 2 21 syl
 |-  ( ph -> ( E. i e. { A } K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
23 18 22 bitrd
 |-  ( ph -> ( E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) )
24 11 23 mtbird
 |-  ( ph -> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) )
25 5 eldifad
 |-  ( ph -> K e. V )
26 1 eleq2d
 |-  ( ph -> ( K e. ( Vtx ` G ) <-> K e. V ) )
27 25 26 mpbird
 |-  ( ph -> K e. ( Vtx ` G ) )
28 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
30 eqid
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
31 28 29 30 vtxd0nedgb
 |-  ( K e. ( Vtx ` G ) -> ( ( ( VtxDeg ` G ) ` K ) = 0 <-> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) )
32 27 31 syl
 |-  ( ph -> ( ( ( VtxDeg ` G ) ` K ) = 0 <-> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) )
33 24 32 mpbird
 |-  ( ph -> ( ( VtxDeg ` G ) ` K ) = 0 )