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