wwlks2onv

Description: If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Proof shortened by AV, 14-Mar-2022)

		Ref	Expression
	Hypothesis	wwlks2onv.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	Assertion	wwlks2onv	⊢ ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		wwlks2onv.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	wwlksonvtx	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
3	2	adantl	⊢ ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4		simprl	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
5		wwlknon	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) )
6		wwlknbp1	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) → ( 2 ∈ ℕ₀ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 2 + 1 ) ) )
7		s3fv1	⊢ ( 𝐵 ∈ 𝑈 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
8	7	eqcomd	⊢ ( 𝐵 ∈ 𝑈 → 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
9	8	adantl	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ 𝑈 ) → 𝐵 = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) )
10	1	eqcomi	⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11	10	wrdeqi	⊢ Word ( Vtx ‘ 𝐺 ) = Word 𝑉
12	11	eleq2i	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑉 )
13	12	biimpi	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑉 )
14		1eltp012	⊢ 1 ∈ { 0 , 1 , 2 }
15		s3len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
16	15	oveq2i	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = ( 0 ..^ 3 )
17		fzo0to3tp	⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
18	16 17	eqtri	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = { 0 , 1 , 2 }
19	14 18	eleqtrri	⊢ 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
20		wrdsymbcl	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑉 ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∈ 𝑉 )
21	13 19 20	sylancl	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∈ 𝑉 )
22	21	adantr	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ 𝑈 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∈ 𝑉 )
23	9 22	eqeltrd	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ 𝑈 ) → 𝐵 ∈ 𝑉 )
24	23	ex	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
25	24	3ad2ant2	⊢ ( ( 2 ∈ ℕ₀ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 2 + 1 ) ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
26	6 25	syl	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
27	26	3ad2ant1	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
28	5 27	sylbi	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
29	28	impcom	⊢ ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → 𝐵 ∈ 𝑉 )
30	29	adantr	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
31		simprr	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
32	4 30 31	3jca	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
33	3 32	mpdan	⊢ ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )

Metamath Proof Explorer

Theorem wwlks2onv

Proof