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		1ex	⊢ 1 ∈ V
15	14	tpid2	⊢ 1 ∈ { 0 , 1 , 2 }
16		s3len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = 3
17	16	oveq2i	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = ( 0 ..^ 3 )
18		fzo0to3tp	⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
19	17 18	eqtri	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) = { 0 , 1 , 2 }
20	15 19	eleqtrri	⊢ 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) )
21		wrdsymbcl	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑉 ∧ 1 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∈ 𝑉 )
22	13 20 21	sylancl	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∈ 𝑉 )
23	22	adantr	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ 𝑈 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) ∈ 𝑉 )
24	9 23	eqeltrd	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ 𝑈 ) → 𝐵 ∈ 𝑉 )
25	24	ex	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
26	25	3ad2ant2	⊢ ( ( 2 ∈ ℕ₀ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ) = ( 2 + 1 ) ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
27	6 26	syl	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
28	27	3ad2ant1	⊢ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 2 WWalksN 𝐺 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
29	5 28	sylbi	⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) → ( 𝐵 ∈ 𝑈 → 𝐵 ∈ 𝑉 ) )
30	29	impcom	⊢ ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → 𝐵 ∈ 𝑉 )
31	30	adantr	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
32		simprr	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
33	4 31 32	3jca	⊢ ( ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
34	3 33	mpdan	⊢ ( ( 𝐵 ∈ 𝑈 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐶 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )

Metamath Proof Explorer

Theorem wwlks2onv

Proof