This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐺 ) ∧ 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 isclwlk ⊢ ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
2 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 1 ) )
3 2 eqeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) )
4 3 anbi2d ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ) )
5 simp2r ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) )
6 simp3 ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ∧ Fun ( iEdg ‘ 𝐺 ) ) → Fun ( iEdg ‘ 𝐺 ) )
7 simp2l ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ∧ Fun ( iEdg ‘ 𝐺 ) ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
8 simpr ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) )
9 8 anim2i ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) )
10 9 3adant3 ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) )
11 wlkl1loop ⊢ ( ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) ∧ ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ) → { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
12 6 7 10 11 syl21anc ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ∧ Fun ( iEdg ‘ 𝐺 ) ) → { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
13 5 12 jca ⊢ ( ( ( ♯ ‘ 𝐹 ) = 1 ∧ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) ∧ Fun ( iEdg ‘ 𝐺 ) ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
14 13 3exp ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ) → ( Fun ( iEdg ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
15 4 14 sylbid ⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( Fun ( iEdg ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
16 15 com13 ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
17 1 16 biimtrid ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
18 17 3imp ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝐹 ( ClWalks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 1 ) ∧ { ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )