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

Metamath Proof Explorer

Theorem cycl3grtrilem

Description: Lemma for cycl3grtri . (Contributed by AV, 5-Oct-2025)

Ref Expression
Assertion cycl3grtrilem ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 2 upgrwlkvtxedg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
4 1 3 sylan2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
5 4 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
6 oveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 3 ) )
7 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
8 6 7 eqtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 , 2 } )
9 8 adantl ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 , 2 } )
10 9 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 , 2 } )
11 10 raleqdv ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑥 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
12 fveq2 ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 3 ) )
13 12 eqeq2d ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ) )
14 c0ex ⊢ 0 ∈ V
15 1ex ⊢ 1 ∈ V
16 2ex ⊢ 2 ∈ V
17 fveq2 ⊢ ( 𝑥 = 0 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 0 ) )
18 fv0p1e1 ⊢ ( 𝑥 = 0 → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 1 ) )
19 17 18 preq12d ⊢ ( 𝑥 = 0 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
20 19 eleq1d ⊢ ( 𝑥 = 0 → ( { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
21 fveq2 ⊢ ( 𝑥 = 1 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 1 ) )
22 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 + 1 ) = ( 1 + 1 ) )
23 1p1e2 ⊢ ( 1 + 1 ) = 2
24 22 23 eqtrdi ⊢ ( 𝑥 = 1 → ( 𝑥 + 1 ) = 2 )
25 24 fveq2d ⊢ ( 𝑥 = 1 → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 2 ) )
26 21 25 preq12d ⊢ ( 𝑥 = 1 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
27 26 eleq1d ⊢ ( 𝑥 = 1 → ( { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
28 fveq2 ⊢ ( 𝑥 = 2 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 2 ) )
29 oveq1 ⊢ ( 𝑥 = 2 → ( 𝑥 + 1 ) = ( 2 + 1 ) )
30 2p1e3 ⊢ ( 2 + 1 ) = 3
31 29 30 eqtrdi ⊢ ( 𝑥 = 2 → ( 𝑥 + 1 ) = 3 )
32 31 fveq2d ⊢ ( 𝑥 = 2 → ( 𝑃 ‘ ( 𝑥 + 1 ) ) = ( 𝑃 ‘ 3 ) )
33 28 32 preq12d ⊢ ( 𝑥 = 2 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } )
34 33 eleq1d ⊢ ( 𝑥 = 2 → ( { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) )
35 14 15 16 20 27 34 raltp ⊢ ( ∀ 𝑥 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) )
36 simpr1 ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
37 preq2 ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } )
38 prcom ⊢ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) }
39 37 38 eqtr3di ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } )
40 39 eleq1d ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
41 40 biimpcd ⊢ ( { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
42 41 3ad2ant3 ⊢ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
43 42 impcom ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) )
44 simpr2 ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) )
45 36 43 44 3jca ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) ∧ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
46 45 ex ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 3 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
47 35 46 biimtrid ⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 3 ) → ( ∀ 𝑥 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
48 13 47 biimtrdi ⊢ ( ( ♯ ‘ 𝐹 ) = 3 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑥 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
49 48 impcom ⊢ ( ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) → ( ∀ 𝑥 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
50 49 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ∀ 𝑥 ∈ { 0 , 1 , 2 } { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
51 11 50 sylbid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
52 5 51 mpd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ∧ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) = 3 ) ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )