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 ∈ 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 ∈ Edg ⁡ G
12 6 7 10 11 syl21anc ⊢ F = 1 ∧ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ 1 ∧ Fun ⁡ iEdg ⁡ G → P ⁡ 0 ∈ 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 ∈ Edg ⁡ G
14 13 3exp ⊢ F = 1 → F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ 1 → Fun ⁡ iEdg ⁡ G → P ⁡ 0 = P ⁡ 1 ∧ P ⁡ 0 ∈ 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 ∈ Edg ⁡ G
16 15 com13 ⊢ Fun ⁡ iEdg ⁡ G → F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F = 1 → P ⁡ 0 = P ⁡ 1 ∧ P ⁡ 0 ∈ Edg ⁡ G
17 1 16 biimtrid ⊢ Fun ⁡ iEdg ⁡ G → F ClWalks ⁡ G P → F = 1 → P ⁡ 0 = P ⁡ 1 ∧ P ⁡ 0 ∈ Edg ⁡ G
18 17 3imp ⊢ Fun ⁡ iEdg ⁡ G ∧ F ClWalks ⁡ G P ∧ F = 1 → P ⁡ 0 = P ⁡ 1 ∧ P ⁡ 0 ∈ Edg ⁡ G