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 
|- ( ph -> T e. ( GrTriangles ` G ) )
grtriclwlk3.p 
|- ( ph -> P : ( 0 ..^ 3 ) -1-1-onto-> T )
Assertion grtriclwlk3 
|- ( ph -> P e. ( 3 ClWWalksN G ) )

Proof

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