Metamath Proof Explorer


Theorem poimirlem5

Description: Lemma for poimir to establish that, for the simplices defined by a walk along the edges of an N -cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
poimirlem9.1 φ T S
poimirlem5.2 φ 0 < 2 nd T
Assertion poimirlem5 φ F 0 = 1 st 1 st T

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
3 poimirlem9.1 φ T S
4 poimirlem5.2 φ 0 < 2 nd T
5 fveq2 t = T 2 nd t = 2 nd T
6 5 breq2d t = T y < 2 nd t y < 2 nd T
7 6 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
8 7 csbeq1d t = T if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd T y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
9 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
10 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
11 10 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
12 11 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
13 10 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
14 13 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
15 12 14 uneq12d t = T 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
16 9 15 oveq12d t = T 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
17 16 csbeq2dv t = T if y < 2 nd T y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
18 8 17 eqtrd t = T if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
19 18 mpteq2dv t = T y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
20 19 eqeq2d t = T F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
21 20 2 elrab2 T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
22 21 simprbi T S F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
23 3 22 syl φ F = y 0 N 1 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
24 breq1 y = 0 y < 2 nd T 0 < 2 nd T
25 id y = 0 y = 0
26 24 25 ifbieq1d y = 0 if y < 2 nd T y y + 1 = if 0 < 2 nd T 0 y + 1
27 4 iftrued φ if 0 < 2 nd T 0 y + 1 = 0
28 26 27 sylan9eqr φ y = 0 if y < 2 nd T y y + 1 = 0
29 28 csbeq1d φ y = 0 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 0 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
30 c0ex 0 V
31 oveq2 j = 0 1 j = 1 0
32 fz10 1 0 =
33 31 32 eqtrdi j = 0 1 j =
34 33 imaeq2d j = 0 2 nd 1 st T 1 j = 2 nd 1 st T
35 34 xpeq1d j = 0 2 nd 1 st T 1 j × 1 = 2 nd 1 st T × 1
36 oveq1 j = 0 j + 1 = 0 + 1
37 0p1e1 0 + 1 = 1
38 36 37 eqtrdi j = 0 j + 1 = 1
39 38 oveq1d j = 0 j + 1 N = 1 N
40 39 imaeq2d j = 0 2 nd 1 st T j + 1 N = 2 nd 1 st T 1 N
41 40 xpeq1d j = 0 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T 1 N × 0
42 35 41 uneq12d j = 0 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T × 1 2 nd 1 st T 1 N × 0
43 ima0 2 nd 1 st T =
44 43 xpeq1i 2 nd 1 st T × 1 = × 1
45 0xp × 1 =
46 44 45 eqtri 2 nd 1 st T × 1 =
47 46 uneq1i 2 nd 1 st T × 1 2 nd 1 st T 1 N × 0 = 2 nd 1 st T 1 N × 0
48 uncom 2 nd 1 st T 1 N × 0 = 2 nd 1 st T 1 N × 0
49 un0 2 nd 1 st T 1 N × 0 = 2 nd 1 st T 1 N × 0
50 47 48 49 3eqtri 2 nd 1 st T × 1 2 nd 1 st T 1 N × 0 = 2 nd 1 st T 1 N × 0
51 42 50 eqtrdi j = 0 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 2 nd 1 st T 1 N × 0
52 51 oveq2d j = 0 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 N × 0
53 30 52 csbie 0 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 N × 0
54 elrabi T t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
55 54 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
56 3 55 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
57 xp1st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
58 56 57 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
59 xp2nd 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
60 58 59 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
61 fvex 2 nd 1 st T V
62 f1oeq1 f = 2 nd 1 st T f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
63 61 62 elab 2 nd 1 st T f | f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
64 60 63 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
65 f1ofo 2 nd 1 st T : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N onto 1 N
66 64 65 syl φ 2 nd 1 st T : 1 N onto 1 N
67 foima 2 nd 1 st T : 1 N onto 1 N 2 nd 1 st T 1 N = 1 N
68 66 67 syl φ 2 nd 1 st T 1 N = 1 N
69 68 xpeq1d φ 2 nd 1 st T 1 N × 0 = 1 N × 0
70 69 oveq2d φ 1 st 1 st T + f 2 nd 1 st T 1 N × 0 = 1 st 1 st T + f 1 N × 0
71 53 70 syl5eq φ 0 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 1 N × 0
72 71 adantr φ y = 0 0 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 1 N × 0
73 29 72 eqtrd φ y = 0 if y < 2 nd T y y + 1 / j 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0 = 1 st 1 st T + f 1 N × 0
74 nnm1nn0 N N 1 0
75 1 74 syl φ N 1 0
76 0elfz N 1 0 0 0 N 1
77 75 76 syl φ 0 0 N 1
78 ovexd φ 1 st 1 st T + f 1 N × 0 V
79 23 73 77 78 fvmptd φ F 0 = 1 st 1 st T + f 1 N × 0
80 ovexd φ 1 N V
81 xp1st 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st T 0 ..^ K 1 N
82 58 81 syl φ 1 st 1 st T 0 ..^ K 1 N
83 elmapfn 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T Fn 1 N
84 82 83 syl φ 1 st 1 st T Fn 1 N
85 fnconstg 0 V 1 N × 0 Fn 1 N
86 30 85 mp1i φ 1 N × 0 Fn 1 N
87 eqidd φ n 1 N 1 st 1 st T n = 1 st 1 st T n
88 30 fvconst2 n 1 N 1 N × 0 n = 0
89 88 adantl φ n 1 N 1 N × 0 n = 0
90 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
91 82 90 syl φ 1 st 1 st T : 1 N 0 ..^ K
92 91 ffvelrnda φ n 1 N 1 st 1 st T n 0 ..^ K
93 elfzonn0 1 st 1 st T n 0 ..^ K 1 st 1 st T n 0
94 92 93 syl φ n 1 N 1 st 1 st T n 0
95 94 nn0cnd φ n 1 N 1 st 1 st T n
96 95 addid1d φ n 1 N 1 st 1 st T n + 0 = 1 st 1 st T n
97 80 84 86 84 87 89 96 offveq φ 1 st 1 st T + f 1 N × 0 = 1 st 1 st T
98 79 97 eqtrd φ F 0 = 1 st 1 st T