Metamath Proof Explorer

Theorem grtriclwlk3

Description: A triangle induces a closed walk of length 3 . (Contributed by AV, 26-Jul-2025)

Ref Expression
Hypotheses grtriclwlk3.t ⊢ ( 𝜑 → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
grtriclwlk3.p ⊢ ( 𝜑 → 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )
Assertion grtriclwlk3 ( 𝜑 → 𝑃 ∈ ( 3 ClWWalksN 𝐺 ) )

Proof

Step Hyp Ref Expression
1 grtriclwlk3.t ⊢ ( 𝜑 → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
2 grtriclwlk3.p ⊢ ( 𝜑 → 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )
3 f1ofn ⊢ ( 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → 𝑃 Fn ( 0 ..^ 3 ) )
4 hashfn ⊢ ( 𝑃 Fn ( 0 ..^ 3 ) → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) )
5 2 3 4 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ( 0 ..^ 3 ) ) )
6 3nn0 ⊢ 3 ∈ ℕ0
7 hashfzo0 ⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
8 6 7 mp1i ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
9 5 8 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = 3 )
10 f1of ⊢ ( 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 )
11 2 10 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 )
12 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
13 12 grtrissvtx ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → 𝑇 ⊆ ( Vtx ‘ 𝐺 ) )
14 1 13 syl ⊢ ( 𝜑 → 𝑇 ⊆ ( Vtx ‘ 𝐺 ) )
15 11 14 jca ⊢ ( 𝜑 → ( 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 ∧ 𝑇 ⊆ ( Vtx ‘ 𝐺 ) ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 ∧ 𝑇 ⊆ ( Vtx ‘ 𝐺 ) ) )
17 fss ⊢ ( ( 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 ∧ 𝑇 ⊆ ( Vtx ‘ 𝐺 ) ) → 𝑃 : ( 0 ..^ 3 ) ⟶ ( Vtx ‘ 𝐺 ) )
18 iswrdi ⊢ ( 𝑃 : ( 0 ..^ 3 ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
19 16 17 18 3syl ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) )
20 oveq1 ⊢ ( ( ♯ ‘ 𝑃 ) = 3 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( 3 − 1 ) )
21 3m1e2 ⊢ ( 3 − 1 ) = 2
22 20 21 eqtrdi ⊢ ( ( ♯ ‘ 𝑃 ) = 3 → ( ( ♯ ‘ 𝑃 ) − 1 ) = 2 )
23 22 oveq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 3 → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ..^ 2 ) )
24 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
25 23 24 eqtrdi ⊢ ( ( ♯ ‘ 𝑃 ) = 3 → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = { 0 , 1 } )
26 25 eleq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 3 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ 𝑖 ∈ { 0 , 1 } ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↔ 𝑖 ∈ { 0 , 1 } ) )
28 1 2 jca ⊢ ( 𝜑 → ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ∧ 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) )
29 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
30 12 29 grtrif1o ⊢ ( ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) ∧ 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 ) → ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
31 simp1 ⊢ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
32 28 30 31 3syl ⊢ ( 𝜑 → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
34 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
35 fv0p1e1 ⊢ ( 𝑖 = 0 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ 1 ) )
36 34 35 preq12d ⊢ ( 𝑖 = 0 → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
37 36 eleq1d ⊢ ( 𝑖 = 0 → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
38 33 37 imbitrrid ⊢ ( 𝑖 = 0 → ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
39 simp3 ⊢ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) )
40 28 30 39 3syl ⊢ ( 𝜑 → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) )
42 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 1 ) )
43 oveq1 ⊢ ( 𝑖 = 1 → ( 𝑖 + 1 ) = ( 1 + 1 ) )
44 1p1e2 ⊢ ( 1 + 1 ) = 2
45 43 44 eqtrdi ⊢ ( 𝑖 = 1 → ( 𝑖 + 1 ) = 2 )
46 45 fveq2d ⊢ ( 𝑖 = 1 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ 2 ) )
47 42 46 preq12d ⊢ ( 𝑖 = 1 → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
48 47 eleq1d ⊢ ( 𝑖 = 1 → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) )
49 41 48 imbitrrid ⊢ ( 𝑖 = 1 → ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
50 38 49 jaoi ⊢ ( ( 𝑖 = 0 ∨ 𝑖 = 1 ) → ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
51 elpri ⊢ ( 𝑖 ∈ { 0 , 1 } → ( 𝑖 = 0 ∨ 𝑖 = 1 ) )
52 50 51 syl11 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( 𝑖 ∈ { 0 , 1 } → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
53 27 52 sylbid ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
54 53 ralrimiv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
55 ovexd ⊢ ( 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( 0 ..^ 3 ) ∈ V )
56 10 55 jca ⊢ ( 𝑃 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 → ( 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 ∧ ( 0 ..^ 3 ) ∈ V ) )
57 fex ⊢ ( ( 𝑃 : ( 0 ..^ 3 ) ⟶ 𝑇 ∧ ( 0 ..^ 3 ) ∈ V ) → 𝑃 ∈ V )
58 2 56 57 3syl ⊢ ( 𝜑 → 𝑃 ∈ V )
59 58 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → 𝑃 ∈ V )
60 lsw ⊢ ( 𝑃 ∈ V → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
61 59 60 syl ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
62 22 fveq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 3 → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ 2 ) )
63 62 adantl ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( 𝑃 ‘ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 𝑃 ‘ 2 ) )
64 61 63 eqtrd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( lastS ‘ 𝑃 ) = ( 𝑃 ‘ 2 ) )
65 64 preq1d ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } )
66 prcom ⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) }
67 66 eleq1i ⊢ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
68 67 biimpi ⊢ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
69 68 3ad2ant2 ⊢ ( ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ∈ ( Edg ‘ 𝐺 ) ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
70 28 30 69 3syl ⊢ ( 𝜑 → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
72 65 71 eqeltrd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) )
73 19 54 72 3jca ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) )
74 simpr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( ♯ ‘ 𝑃 ) = 3 )
75 73 74 jca ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 3 ) → ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑃 ) = 3 ) )
76 9 75 mpdan ⊢ ( 𝜑 → ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑃 ) = 3 ) )
77 3nn ⊢ 3 ∈ ℕ
78 12 29 isclwwlknx ⊢ ( 3 ∈ ℕ → ( 𝑃 ∈ ( 3 ClWWalksN 𝐺 ) ↔ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑃 ) = 3 ) ) )
79 77 78 mp1i ⊢ ( 𝜑 → ( 𝑃 ∈ ( 3 ClWWalksN 𝐺 ) ↔ ( ( 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑃 ) , ( 𝑃 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑃 ) = 3 ) ) )
80 76 79 mpbird ⊢ ( 𝜑 → 𝑃 ∈ ( 3 ClWWalksN 𝐺 ) )