Metamath Proof Explorer

Theorem clwlkl1loop

Description: A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021)

Ref Expression
Assertion clwlkl1loop 
|- ( ( Fun ( iEdg ` G ) /\ F ( ClWalks ` G ) P /\ ( # ` F ) = 1 ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) )

Proof

Step Hyp Ref Expression
1 isclwlk 
 |-  ( F ( ClWalks ` G ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
2 fveq2 
 |-  ( ( # ` F ) = 1 -> ( P ` ( # ` F ) ) = ( P ` 1 ) )
3 2 eqeq2d 
 |-  ( ( # ` F ) = 1 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` 1 ) ) )
4 3 anbi2d 
 |-  ( ( # ` F ) = 1 -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) ) )
5 simp2r 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> ( P ` 0 ) = ( P ` 1 ) )
6 simp3 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> Fun ( iEdg ` G ) )
7 simp2l 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> F ( Walks ` G ) P )
8 simpr 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) -> ( P ` 0 ) = ( P ` 1 ) )
9 8 anim2i 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) )
10 9 3adant3 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) )
11 wlkl1loop 
 |-  ( ( ( Fun ( iEdg ` G ) /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) )
12 6 7 10 11 syl21anc 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) )
13 5 12 jca 
 |-  ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) )
14 13 3exp 
 |-  ( ( # ` F ) = 1 -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) -> ( Fun ( iEdg ` G ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) )
15 4 14 sylbid 
 |-  ( ( # ` F ) = 1 -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( Fun ( iEdg ` G ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) )
16 15 com13 
 |-  ( Fun ( iEdg ` G ) -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 1 -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) )
17 1 16 syl5bi 
 |-  ( Fun ( iEdg ` G ) -> ( F ( ClWalks ` G ) P -> ( ( # ` F ) = 1 -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) )
18 17 3imp 
 |-  ( ( Fun ( iEdg ` G ) /\ F ( ClWalks ` G ) P /\ ( # ` F ) = 1 ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) )