Metamath Proof Explorer

Theorem rusgr0edg

Description: Special case for graphs without edges: There are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Hypotheses rusgrnumwwlk.v 
|- V = ( Vtx ` G )
rusgrnumwwlk.l 
|- L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
Assertion rusgr0edg 
|- ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> ( P L N ) = 0 )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v 
 |-  V = ( Vtx ` G )
2 rusgrnumwwlk.l 
 |-  L = ( v e. V , n e. NN0 |-> ( # ` { w e. ( n WWalksN G ) | ( w ` 0 ) = v } ) )
3 simp2 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> P e. V )
4 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
5 4 3ad2ant3 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> N e. NN0 )
6 1 2 rusgrnumwwlklem 
 |-  ( ( P e. V /\ N e. NN0 ) -> ( P L N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )
7 3 5 6 syl2anc 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> ( P L N ) = ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) )
8 rusgrusgr 
 |-  ( G RegUSGraph 0 -> G e. USGraph )
9 usgr0edg0rusgr 
 |-  ( G e. USGraph -> ( G RegUSGraph 0 <-> ( Edg ` G ) = (/) ) )
10 9 biimpcd 
 |-  ( G RegUSGraph 0 -> ( G e. USGraph -> ( Edg ` G ) = (/) ) )
11 8 10 mpd 
 |-  ( G RegUSGraph 0 -> ( Edg ` G ) = (/) )
12 0enwwlksnge1 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> ( N WWalksN G ) = (/) )
13 11 12 sylan 
 |-  ( ( G RegUSGraph 0 /\ N e. NN ) -> ( N WWalksN G ) = (/) )
14 eleq2 
 |-  ( ( N WWalksN G ) = (/) -> ( w e. ( N WWalksN G ) <-> w e. (/) ) )
15 noel 
 |-  -. w e. (/)
16 15 pm2.21i 
 |-  ( w e. (/) -> -. ( w ` 0 ) = P )
17 14 16 biimtrdi 
 |-  ( ( N WWalksN G ) = (/) -> ( w e. ( N WWalksN G ) -> -. ( w ` 0 ) = P ) )
18 13 17 syl 
 |-  ( ( G RegUSGraph 0 /\ N e. NN ) -> ( w e. ( N WWalksN G ) -> -. ( w ` 0 ) = P ) )
19 18 3adant2 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> ( w e. ( N WWalksN G ) -> -. ( w ` 0 ) = P ) )
20 19 ralrimiv 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> A. w e. ( N WWalksN G ) -. ( w ` 0 ) = P )
21 rabeq0 
 |-  ( { w e. ( N WWalksN G ) | ( w ` 0 ) = P } = (/) <-> A. w e. ( N WWalksN G ) -. ( w ` 0 ) = P )
22 20 21 sylibr 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> { w e. ( N WWalksN G ) | ( w ` 0 ) = P } = (/) )
23 22 fveq2d 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = ( # ` (/) ) )
24 hash0 
 |-  ( # ` (/) ) = 0
25 23 24 eqtrdi 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> ( # ` { w e. ( N WWalksN G ) | ( w ` 0 ) = P } ) = 0 )
26 7 25 eqtrd 
 |-  ( ( G RegUSGraph 0 /\ P e. V /\ N e. NN ) -> ( P L N ) = 0 )