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 ) ) )