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

Metamath Proof Explorer

Theorem clwwlk1loop

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

Ref Expression
Assertion clwwlk1loop ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 isclwwlk ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
4 lsw1 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 0 ) )
5 4 preq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } )
6 5 eleq1d ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
7 6 biimpd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
8 7 ex ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 1 → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
9 8 com23 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 1 → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
10 9 adantr ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 1 → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
11 10 imp ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = 1 → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
12 11 3adant2 ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑊 ) = 1 → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
13 3 12 sylbi ⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( ♯ ‘ 𝑊 ) = 1 → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
14 13 imp ⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )