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

Metamath Proof Explorer

Theorem clwlkcompbp

Description: Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022)

		Ref	Expression
	Hypotheses	clwlkcompbp.1	⊢ 𝐹 = ( 1^st ‘ 𝑊 )
		clwlkcompbp.2	⊢ 𝑃 = ( 2^nd ‘ 𝑊 )
	Assertion	clwlkcompbp	⊢ ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkcompbp.1	⊢ 𝐹 = ( 1^st ‘ 𝑊 )
2		clwlkcompbp.2	⊢ 𝑃 = ( 2^nd ‘ 𝑊 )
3		clwlkwlk	⊢ ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) → 𝑊 ∈ ( Walks ‘ 𝐺 ) )
4		wlkop	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
5	3 4	syl	⊢ ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
6		eleq1	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) ↔ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) )
7		df-br	⊢ ( ( 1^st ‘ 𝑊 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ↔ ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
8	6 7	bitr4di	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑊 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ) )
9		isclwlk	⊢ ( ( 1^st ‘ 𝑊 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ↔ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ∧ ( ( 2^nd ‘ 𝑊 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑊 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ) )
10	1 2	breq12i	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) )
11	2	fveq1i	⊢ ( 𝑃 ‘ 0 ) = ( ( 2^nd ‘ 𝑊 ) ‘ 0 )
12	1	fveq2i	⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 1^st ‘ 𝑊 ) )
13	2 12	fveq12i	⊢ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( ( 2^nd ‘ 𝑊 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) )
14	11 13	eqeq12i	⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( ( 2^nd ‘ 𝑊 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑊 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) )
15	10 14	anbi12i	⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) ∧ ( ( 2^nd ‘ 𝑊 ) ‘ 0 ) = ( ( 2^nd ‘ 𝑊 ) ‘ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ) )
16	9 15	sylbb2	⊢ ( ( 1^st ‘ 𝑊 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
17	8 16	biimtrdi	⊢ ( 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ → ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
18	5 17	mpcom	⊢ ( 𝑊 ∈ ( ClWalks ‘ 𝐺 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )