Metamath Proof Explorer

Theorem clwwlknonex2lem2

Description: Lemma 2 for clwwlknonex2 : Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018) (Revised by AV, 27-Jan-2022)

Ref Expression
Hypotheses clwwlknonex2.v ⊢V=Vtx⁡G
clwwlknonex2.e ⊢E=Edg⁡G
Assertion clwwlknonex2lem2 ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→∀i∈0..^W−1∪W−1WW++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v ⊢V=Vtx⁡G
2 clwwlknonex2.e ⊢E=Edg⁡G
3 simpl ⊢W∈WordV∧X∈V∧Y∈V→W∈WordV
4 3 adantr ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W∈WordV
5 elfzonn0 ⊢i∈0..^W−1→i∈ℕ0
6 5 adantl ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→i∈ℕ0
7 lencl ⊢W∈WordV→W∈ℕ0
8 elfzo0 ⊢i∈0..^W−1↔i∈ℕ0∧W−1∈ℕ∧i<W−1
9 nn0re ⊢i∈ℕ0→i∈ℝ
10 9 adantr ⊢i∈ℕ0∧W∈ℕ0→i∈ℝ
11 nn0re ⊢W∈ℕ0→W∈ℝ
12 peano2rem ⊢W∈ℝ→W−1∈ℝ
13 11 12 syl ⊢W∈ℕ0→W−1∈ℝ
14 13 adantl ⊢i∈ℕ0∧W∈ℕ0→W−1∈ℝ
15 11 adantl ⊢i∈ℕ0∧W∈ℕ0→W∈ℝ
16 10 14 15 3jca ⊢i∈ℕ0∧W∈ℕ0→i∈ℝ∧W−1∈ℝ∧W∈ℝ
17 11 ltm1d ⊢W∈ℕ0→W−1<W
18 17 adantl ⊢i∈ℕ0∧W∈ℕ0→W−1<W
19 lttr ⊢i∈ℝ∧W−1∈ℝ∧W∈ℝ→i<W−1∧W−1<W→i<W
20 19 expcomd ⊢i∈ℝ∧W−1∈ℝ∧W∈ℝ→W−1<W→i<W−1→i<W
21 16 18 20 sylc ⊢i∈ℕ0∧W∈ℕ0→i<W−1→i<W
22 21 impancom ⊢i∈ℕ0∧i<W−1→W∈ℕ0→i<W
23 22 3adant2 ⊢i∈ℕ0∧W−1∈ℕ∧i<W−1→W∈ℕ0→i<W
24 8 23 sylbi ⊢i∈0..^W−1→W∈ℕ0→i<W
25 7 24 syl5com ⊢W∈WordV→i∈0..^W−1→i<W
26 25 adantr ⊢W∈WordV∧X∈V∧Y∈V→i∈0..^W−1→i<W
27 26 imp ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→i<W
28 ccat2s1fvw ⊢W∈WordV∧i∈ℕ0∧i<W→W++⟨“X”⟩++⟨“Y”⟩⁡i=W⁡i
29 4 6 27 28 syl3anc ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W++⟨“X”⟩++⟨“Y”⟩⁡i=W⁡i
30 29 eqcomd ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W⁡i=W++⟨“X”⟩++⟨“Y”⟩⁡i
31 peano2nn0 ⊢i∈ℕ0→i+1∈ℕ0
32 6 31 syl ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→i+1∈ℕ0
33 1red ⊢i∈ℕ0∧W∈ℕ0→1∈ℝ
34 10 33 15 ltaddsubd ⊢i∈ℕ0∧W∈ℕ0→i+1<W↔i<W−1
35 34 biimprd ⊢i∈ℕ0∧W∈ℕ0→i<W−1→i+1<W
36 35 impancom ⊢i∈ℕ0∧i<W−1→W∈ℕ0→i+1<W
37 36 3adant2 ⊢i∈ℕ0∧W−1∈ℕ∧i<W−1→W∈ℕ0→i+1<W
38 8 37 sylbi ⊢i∈0..^W−1→W∈ℕ0→i+1<W
39 7 38 mpan9 ⊢W∈WordV∧i∈0..^W−1→i+1<W
40 39 adantlr ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→i+1<W
41 ccat2s1fvw ⊢W∈WordV∧i+1∈ℕ0∧i+1<W→W++⟨“X”⟩++⟨“Y”⟩⁡i+1=W⁡i+1
42 4 32 40 41 syl3anc ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W++⟨“X”⟩++⟨“Y”⟩⁡i+1=W⁡i+1
43 42 eqcomd ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W⁡i+1=W++⟨“X”⟩++⟨“Y”⟩⁡i+1
44 30 43 preq12d ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W⁡iW⁡i+1=W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1
45 44 eleq1d ⊢W∈WordV∧X∈V∧Y∈V∧i∈0..^W−1→W⁡iW⁡i+1∈E↔W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
46 45 ralbidva ⊢W∈WordV∧X∈V∧Y∈V→∀i∈0..^W−1W⁡iW⁡i+1∈E↔∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
47 46 biimpd ⊢W∈WordV∧X∈V∧Y∈V→∀i∈0..^W−1W⁡iW⁡i+1∈E→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
48 47 impancom ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E→X∈V∧Y∈V→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
49 48 3adant3 ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→X∈V∧Y∈V→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
50 49 3ad2ant1 ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→X∈V∧Y∈V→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
51 50 com12 ⊢X∈V∧Y∈V→W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
52 51 a1dd ⊢X∈V∧Y∈V→W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→XY∈E→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
53 52 3adant3 ⊢X∈V∧Y∈V∧N∈ℤ≥3→W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→XY∈E→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
54 53 imp31 ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
55 ax-1 ⊢X∈V∧Y∈V→XY∈E→X∈V∧Y∈V
56 55 3adant3 ⊢X∈V∧Y∈V∧N∈ℤ≥3→XY∈E→X∈V∧Y∈V
57 simpl ⊢W∈WordV∧N∈ℤ≥3∧W=N−2→W∈WordV
58 oveq1 ⊢W=N−2→W−1=N-2-1
59 58 adantr ⊢W=N−2∧N∈ℤ≥3→W−1=N-2-1
60 eluzelcn ⊢N∈ℤ≥3→N∈ℂ
61 2cnd ⊢N∈ℤ≥3→2∈ℂ
62 1cnd ⊢N∈ℤ≥3→1∈ℂ
63 60 61 62 subsub4d ⊢N∈ℤ≥3→N-2-1=N−2+1
64 2p1e3 ⊢2+1=3
65 64 a1i ⊢N∈ℤ≥3→2+1=3
66 65 oveq2d ⊢N∈ℤ≥3→N−2+1=N−3
67 uznn0sub ⊢N∈ℤ≥3→N−3∈ℕ0
68 66 67 eqeltrd ⊢N∈ℤ≥3→N−2+1∈ℕ0
69 63 68 eqeltrd ⊢N∈ℤ≥3→N-2-1∈ℕ0
70 69 adantl ⊢W=N−2∧N∈ℤ≥3→N-2-1∈ℕ0
71 59 70 eqeltrd ⊢W=N−2∧N∈ℤ≥3→W−1∈ℕ0
72 71 ancoms ⊢N∈ℤ≥3∧W=N−2→W−1∈ℕ0
73 72 adantl ⊢W∈WordV∧N∈ℤ≥3∧W=N−2→W−1∈ℕ0
74 7 11 syl ⊢W∈WordV→W∈ℝ
75 74 adantr ⊢W∈WordV∧N∈ℤ≥3∧W=N−2→W∈ℝ
76 75 ltm1d ⊢W∈WordV∧N∈ℤ≥3∧W=N−2→W−1<W
77 57 73 76 3jca ⊢W∈WordV∧N∈ℤ≥3∧W=N−2→W∈WordV∧W−1∈ℕ0∧W−1<W
78 77 ex ⊢W∈WordV→N∈ℤ≥3∧W=N−2→W∈WordV∧W−1∈ℕ0∧W−1<W
79 78 adantr ⊢W∈WordV∧lastS⁡WW⁡0∈E→N∈ℤ≥3∧W=N−2→W∈WordV∧W−1∈ℕ0∧W−1<W
80 79 3ad2ant1 ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→N∈ℤ≥3∧W=N−2→W∈WordV∧W−1∈ℕ0∧W−1<W
81 80 imp ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X∧N∈ℤ≥3∧W=N−2→W∈WordV∧W−1∈ℕ0∧W−1<W
82 ccat2s1fvw ⊢W∈WordV∧W−1∈ℕ0∧W−1<W→W++⟨“X”⟩++⟨“Y”⟩⁡W−1=W⁡W−1
83 81 82 syl ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X∧N∈ℤ≥3∧W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1=W⁡W−1
84 nn0cn ⊢W∈ℕ0→W∈ℂ
85 ax-1cn ⊢1∈ℂ
86 npcan ⊢W∈ℂ∧1∈ℂ→W-1+1=W
87 84 85 86 sylancl ⊢W∈ℕ0→W-1+1=W
88 7 87 syl ⊢W∈WordV→W-1+1=W
89 88 adantr ⊢W∈WordV∧lastS⁡WW⁡0∈E→W-1+1=W
90 89 3ad2ant1 ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W-1+1=W
91 90 fveq2d ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1=W++⟨“X”⟩++⟨“Y”⟩⁡W
92 simp1l ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W∈WordV
93 eqidd ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W=W
94 simp2l ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→X∈V
95 ccatw2s1p1 ⊢W∈WordV∧W=W∧X∈V→W++⟨“X”⟩++⟨“Y”⟩⁡W=X
96 92 93 94 95 syl3anc ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W++⟨“X”⟩++⟨“Y”⟩⁡W=X
97 91 96 eqtrd ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1=X
98 97 adantr ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X∧N∈ℤ≥3∧W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1=X
99 83 98 preq12d ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X∧N∈ℤ≥3∧W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1=W⁡W−1X
100 lsw ⊢W∈WordV→lastS⁡W=W⁡W−1
101 100 adantl ⊢W⁡0=X∧W∈WordV→lastS⁡W=W⁡W−1
102 simpl ⊢W⁡0=X∧W∈WordV→W⁡0=X
103 101 102 preq12d ⊢W⁡0=X∧W∈WordV→lastS⁡WW⁡0=W⁡W−1X
104 103 eleq1d ⊢W⁡0=X∧W∈WordV→lastS⁡WW⁡0∈E↔W⁡W−1X∈E
105 104 biimpd ⊢W⁡0=X∧W∈WordV→lastS⁡WW⁡0∈E→W⁡W−1X∈E
106 105 expcom ⊢W∈WordV→W⁡0=X→lastS⁡WW⁡0∈E→W⁡W−1X∈E
107 106 com23 ⊢W∈WordV→lastS⁡WW⁡0∈E→W⁡0=X→W⁡W−1X∈E
108 107 imp31 ⊢W∈WordV∧lastS⁡WW⁡0∈E∧W⁡0=X→W⁡W−1X∈E
109 108 3adant2 ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X→W⁡W−1X∈E
110 109 adantr ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X∧N∈ℤ≥3∧W=N−2→W⁡W−1X∈E
111 99 110 eqeltrd ⊢W∈WordV∧lastS⁡WW⁡0∈E∧X∈V∧Y∈V∧W⁡0=X∧N∈ℤ≥3∧W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
112 111 exp520 ⊢W∈WordV∧lastS⁡WW⁡0∈E→X∈V∧Y∈V→W⁡0=X→N∈ℤ≥3→W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
113 112 com14 ⊢N∈ℤ≥3→X∈V∧Y∈V→W⁡0=X→W∈WordV∧lastS⁡WW⁡0∈E→W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
114 113 3ad2ant3 ⊢X∈V∧Y∈V∧N∈ℤ≥3→X∈V∧Y∈V→W⁡0=X→W∈WordV∧lastS⁡WW⁡0∈E→W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
115 56 114 syld ⊢X∈V∧Y∈V∧N∈ℤ≥3→XY∈E→W⁡0=X→W∈WordV∧lastS⁡WW⁡0∈E→W=N−2→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
116 115 com25 ⊢X∈V∧Y∈V∧N∈ℤ≥3→W=N−2→W⁡0=X→W∈WordV∧lastS⁡WW⁡0∈E→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
117 116 com14 ⊢W∈WordV∧lastS⁡WW⁡0∈E→W=N−2→W⁡0=X→X∈V∧Y∈V∧N∈ℤ≥3→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
118 117 3adant2 ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→W=N−2→W⁡0=X→X∈V∧Y∈V∧N∈ℤ≥3→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
119 118 3imp ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→X∈V∧Y∈V∧N∈ℤ≥3→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
120 119 impcom ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
121 120 imp ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
122 eqidd ⊢W∈WordV∧X∈V∧Y∈V→W=W
123 simprl ⊢W∈WordV∧X∈V∧Y∈V→X∈V
124 3 122 123 95 syl3anc ⊢W∈WordV∧X∈V∧Y∈V→W++⟨“X”⟩++⟨“Y”⟩⁡W=X
125 eqid ⊢W=W
126 ccatw2s1p2 ⊢W∈WordV∧W=W∧X∈V∧Y∈V→W++⟨“X”⟩++⟨“Y”⟩⁡W+1=Y
127 125 126 mpanl2 ⊢W∈WordV∧X∈V∧Y∈V→W++⟨“X”⟩++⟨“Y”⟩⁡W+1=Y
128 124 127 preq12d ⊢W∈WordV∧X∈V∧Y∈V→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
129 128 expcom ⊢X∈V∧Y∈V→W∈WordV→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
130 129 a1i ⊢XY∈E→X∈V∧Y∈V→W∈WordV→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
131 130 com13 ⊢W∈WordV→X∈V∧Y∈V→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
132 131 3ad2ant1 ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E→X∈V∧Y∈V→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
133 132 3ad2ant1 ⊢W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→X∈V∧Y∈V→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
134 133 com12 ⊢X∈V∧Y∈V→W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
135 134 3adant3 ⊢X∈V∧Y∈V∧N∈ℤ≥3→W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X→XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
136 135 imp31 ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1=XY
137 simpr ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→XY∈E
138 136 137 eqeltrd ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1∈E
139 ovex ⊢W−1∈V
140 fvex ⊢W∈V
141 fveq2 ⊢i=W−1→W++⟨“X”⟩++⟨“Y”⟩⁡i=W++⟨“X”⟩++⟨“Y”⟩⁡W−1
142 fvoveq1 ⊢i=W−1→W++⟨“X”⟩++⟨“Y”⟩⁡i+1=W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1
143 141 142 preq12d ⊢i=W−1→W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1=W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1
144 143 eleq1d ⊢i=W−1→W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E↔W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E
145 fveq2 ⊢i=W→W++⟨“X”⟩++⟨“Y”⟩⁡i=W++⟨“X”⟩++⟨“Y”⟩⁡W
146 fvoveq1 ⊢i=W→W++⟨“X”⟩++⟨“Y”⟩⁡i+1=W++⟨“X”⟩++⟨“Y”⟩⁡W+1
147 145 146 preq12d ⊢i=W→W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1=W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1
148 147 eleq1d ⊢i=W→W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E↔W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1∈E
149 139 140 144 148 ralpr ⊢∀i∈W−1WW++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E↔W++⟨“X”⟩++⟨“Y”⟩⁡W−1W++⟨“X”⟩++⟨“Y”⟩⁡W-1+1∈E∧W++⟨“X”⟩++⟨“Y”⟩⁡WW++⟨“X”⟩++⟨“Y”⟩⁡W+1∈E
150 121 138 149 sylanbrc ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→∀i∈W−1WW++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
151 ralunb ⊢∀i∈0..^W−1∪W−1WW++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E↔∀i∈0..^W−1W++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E∧∀i∈W−1WW++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E
152 54 150 151 sylanbrc ⊢X∈V∧Y∈V∧N∈ℤ≥3∧W∈WordV∧∀i∈0..^W−1W⁡iW⁡i+1∈E∧lastS⁡WW⁡0∈E∧W=N−2∧W⁡0=X∧XY∈E→∀i∈0..^W−1∪W−1WW++⟨“X”⟩++⟨“Y”⟩⁡iW++⟨“X”⟩++⟨“Y”⟩⁡i+1∈E