Theorem eupth2lem3

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

	Ref	Expression
Hypotheses	eupth2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	eupth2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	eupth2.g	⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
	eupth2.f	⊢ ( 𝜑 → Fun 𝐼 )
	eupth2.p	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
	eupth2.h	⊢ 𝐻 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩
	eupth2.x	⊢ 𝑋 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩
	eupth2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	eupth2.l	⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐹 ) )
	eupth2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	eupth2.o	⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) )
Assertion	eupth2lem3	⊢ ( 𝜑 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		eupth2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eupth2.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		eupth2.g	⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
4		eupth2.f	⊢ ( 𝜑 → Fun 𝐼 )
5		eupth2.p	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
6		eupth2.h	⊢ 𝐻 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩
7		eupth2.x	⊢ 𝑋 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩
8		eupth2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9		eupth2.l	⊢ ( 𝜑 → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐹 ) )
10		eupth2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
11		eupth2.o	⊢ ( 𝜑 → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐻 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑁 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑁 ) } ) )
12		eupthiswlk	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
13		wlkcl	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
14	5 12 13	3syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
15		nn0p1elfzo	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
16	8 14 9 15	syl3anc	⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17		eupthistrl	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
18	5 17	syl	⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
19	6	fveq2i	⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ )
20	1	fvexi	⊢ 𝑉 ∈ V
21	2	fvexi	⊢ 𝐼 ∈ V
22	21	resex	⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ∈ V
23	20 22	opvtxfvi	⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ ) = 𝑉
24	19 23	eqtri	⊢ ( Vtx ‘ 𝐻 ) = 𝑉
25	24	a1i	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
26		snex	⊢ { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ∈ V
27	20 26	opvtxfvi	⊢ ( Vtx ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = 𝑉
28	27	a1i	⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = 𝑉 )
29	7	fveq2i	⊢ ( Vtx ‘ 𝑋 ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ )
30	21	resex	⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ∈ V
31	20 30	opvtxfvi	⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ ) = 𝑉
32	29 31	eqtri	⊢ ( Vtx ‘ 𝑋 ) = 𝑉
33	32	a1i	⊢ ( 𝜑 → ( Vtx ‘ 𝑋 ) = 𝑉 )
34	6	fveq2i	⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ )
35	20 22	opiedgfvi	⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
36	34 35	eqtri	⊢ ( iEdg ‘ 𝐻 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
37	36	a1i	⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
38	20 26	opiedgfvi	⊢ ( iEdg ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ }
39	38	a1i	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } ⟩ ) = { ⟨ ( 𝐹 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ⟩ } )
40	7	fveq2i	⊢ ( iEdg ‘ 𝑋 ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ )
41	20 30	opiedgfvi	⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
42	40 41	eqtri	⊢ ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
43	8	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
44		fzval3	⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
45	44	eqcomd	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) )
46	43 45	syl	⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 + 1 ) ) = ( 0 ... 𝑁 ) )
47	46	imaeq2d	⊢ ( 𝜑 → ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( 𝐹 “ ( 0 ... 𝑁 ) ) )
48	47	reseq2d	⊢ ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
49	42 48	syl5eq	⊢ ( 𝜑 → ( iEdg ‘ 𝑋 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ... 𝑁 ) ) ) )
50		2fveq3	⊢ ( 𝑘 = 𝑁 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) )
51		fveq2	⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) )
52		fvoveq1	⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
53	51 52	preq12d	⊢ ( 𝑘 = 𝑁 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
54	50 53	eqeq12d	⊢ ( 𝑘 = 𝑁 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) )
55	5 12	syl	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
56	2	upgrwlkedg	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
57	3 55 56	syl2anc	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
58	54 57 16	rspcdva	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
59	1 2 4 16 10 18 25 28 33 37 39 49 11 58	eupth2lem3lem7	⊢ ( 𝜑 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 𝑋 ) ‘ 𝑈 ) ↔ 𝑈 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) )