Metamath Proof Explorer


Theorem 3pthdlem1

Description: Lemma 1 for 3pthd . (Contributed by AV, 9-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p P = ⟨“ ABCD ”⟩
3wlkd.f F = ⟨“ JKL ”⟩
3wlkd.s φ A V B V C V D V
3wlkd.n φ A B A C B C B D C D
Assertion 3pthdlem1 φ k 0 ..^ P j 1 ..^ F k j P k P j

Proof

Step Hyp Ref Expression
1 3wlkd.p P = ⟨“ ABCD ”⟩
2 3wlkd.f F = ⟨“ JKL ”⟩
3 3wlkd.s φ A V B V C V D V
4 3wlkd.n φ A B A C B C B D C D
5 1 2 3 3wlkdlem3 φ P 0 = A P 1 = B P 2 = C P 3 = D
6 simpr1l P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D A B
7 simpl P 0 = A P 1 = B P 0 = A
8 7 adantr P 0 = A P 1 = B P 2 = C P 3 = D P 0 = A
9 simpr P 0 = A P 1 = B P 1 = B
10 9 adantr P 0 = A P 1 = B P 2 = C P 3 = D P 1 = B
11 8 10 neeq12d P 0 = A P 1 = B P 2 = C P 3 = D P 0 P 1 A B
12 11 adantr P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 0 P 1 A B
13 6 12 mpbird P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 0 P 1
14 13 a1d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 0 1 P 0 P 1
15 simpr1r P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D A C
16 simpl P 2 = C P 3 = D P 2 = C
17 16 adantl P 0 = A P 1 = B P 2 = C P 3 = D P 2 = C
18 8 17 neeq12d P 0 = A P 1 = B P 2 = C P 3 = D P 0 P 2 A C
19 18 adantr P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 0 P 2 A C
20 15 19 mpbird P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 0 P 2
21 20 a1d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 0 2 P 0 P 2
22 14 21 jca P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 0 1 P 0 P 1 0 2 P 0 P 2
23 eqid 1 = 1
24 23 2a1i P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 1 = P 1 1 = 1
25 24 necon3d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 1 1 P 1 P 1
26 simpr2l P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D B C
27 10 17 neeq12d P 0 = A P 1 = B P 2 = C P 3 = D P 1 P 2 B C
28 27 adantr P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 1 P 2 B C
29 26 28 mpbird P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 1 P 2
30 29 a1d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 1 2 P 1 P 2
31 25 30 jca P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 1 1 P 1 P 1 1 2 P 1 P 2
32 29 necomd P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 2 P 1
33 32 a1d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 2 1 P 2 P 1
34 eqid 2 = 2
35 34 2a1i P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 2 = P 2 2 = 2
36 35 necon3d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 2 2 P 2 P 2
37 simpr2r P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D B D
38 simpr P 2 = C P 3 = D P 3 = D
39 38 adantl P 0 = A P 1 = B P 2 = C P 3 = D P 3 = D
40 10 39 neeq12d P 0 = A P 1 = B P 2 = C P 3 = D P 1 P 3 B D
41 40 adantr P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 1 P 3 B D
42 37 41 mpbird P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 1 P 3
43 42 necomd P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 3 P 1
44 43 a1d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 3 1 P 3 P 1
45 simp3 A B A C B C B D C D C D
46 45 necomd A B A C B C B D C D D C
47 46 adantl P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D D C
48 simpl P 3 = D P 2 = C P 3 = D
49 simpr P 3 = D P 2 = C P 2 = C
50 48 49 neeq12d P 3 = D P 2 = C P 3 P 2 D C
51 50 ancoms P 2 = C P 3 = D P 3 P 2 D C
52 51 adantl P 0 = A P 1 = B P 2 = C P 3 = D P 3 P 2 D C
53 52 adantr P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 3 P 2 D C
54 47 53 mpbird P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D P 3 P 2
55 54 a1d P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 3 2 P 3 P 2
56 44 55 jca P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 3 1 P 3 P 1 3 2 P 3 P 2
57 33 36 56 jca31 P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 2 1 P 2 P 1 2 2 P 2 P 2 3 1 P 3 P 1 3 2 P 3 P 2
58 22 31 57 jca31 P 0 = A P 1 = B P 2 = C P 3 = D A B A C B C B D C D 0 1 P 0 P 1 0 2 P 0 P 2 1 1 P 1 P 1 1 2 P 1 P 2 2 1 P 2 P 1 2 2 P 2 P 2 3 1 P 3 P 1 3 2 P 3 P 2
59 5 4 58 syl2anc φ 0 1 P 0 P 1 0 2 P 0 P 2 1 1 P 1 P 1 1 2 P 1 P 2 2 1 P 2 P 1 2 2 P 2 P 2 3 1 P 3 P 1 3 2 P 3 P 2
60 1 fveq2i P = ⟨“ ABCD ”⟩
61 s4len ⟨“ ABCD ”⟩ = 4
62 60 61 eqtri P = 4
63 62 oveq2i 0 ..^ P = 0 ..^ 4
64 fzo0to42pr 0 ..^ 4 = 0 1 2 3
65 63 64 eqtri 0 ..^ P = 0 1 2 3
66 65 raleqi k 0 ..^ P k 1 P k P 1 k 2 P k P 2 k 0 1 2 3 k 1 P k P 1 k 2 P k P 2
67 ralunb k 0 1 2 3 k 1 P k P 1 k 2 P k P 2 k 0 1 k 1 P k P 1 k 2 P k P 2 k 2 3 k 1 P k P 1 k 2 P k P 2
68 c0ex 0 V
69 1ex 1 V
70 neeq1 k = 0 k 1 0 1
71 fveq2 k = 0 P k = P 0
72 71 neeq1d k = 0 P k P 1 P 0 P 1
73 70 72 imbi12d k = 0 k 1 P k P 1 0 1 P 0 P 1
74 neeq1 k = 0 k 2 0 2
75 71 neeq1d k = 0 P k P 2 P 0 P 2
76 74 75 imbi12d k = 0 k 2 P k P 2 0 2 P 0 P 2
77 73 76 anbi12d k = 0 k 1 P k P 1 k 2 P k P 2 0 1 P 0 P 1 0 2 P 0 P 2
78 neeq1 k = 1 k 1 1 1
79 fveq2 k = 1 P k = P 1
80 79 neeq1d k = 1 P k P 1 P 1 P 1
81 78 80 imbi12d k = 1 k 1 P k P 1 1 1 P 1 P 1
82 neeq1 k = 1 k 2 1 2
83 79 neeq1d k = 1 P k P 2 P 1 P 2
84 82 83 imbi12d k = 1 k 2 P k P 2 1 2 P 1 P 2
85 81 84 anbi12d k = 1 k 1 P k P 1 k 2 P k P 2 1 1 P 1 P 1 1 2 P 1 P 2
86 68 69 77 85 ralpr k 0 1 k 1 P k P 1 k 2 P k P 2 0 1 P 0 P 1 0 2 P 0 P 2 1 1 P 1 P 1 1 2 P 1 P 2
87 2ex 2 V
88 3ex 3 V
89 neeq1 k = 2 k 1 2 1
90 fveq2 k = 2 P k = P 2
91 90 neeq1d k = 2 P k P 1 P 2 P 1
92 89 91 imbi12d k = 2 k 1 P k P 1 2 1 P 2 P 1
93 neeq1 k = 2 k 2 2 2
94 90 neeq1d k = 2 P k P 2 P 2 P 2
95 93 94 imbi12d k = 2 k 2 P k P 2 2 2 P 2 P 2
96 92 95 anbi12d k = 2 k 1 P k P 1 k 2 P k P 2 2 1 P 2 P 1 2 2 P 2 P 2
97 neeq1 k = 3 k 1 3 1
98 fveq2 k = 3 P k = P 3
99 98 neeq1d k = 3 P k P 1 P 3 P 1
100 97 99 imbi12d k = 3 k 1 P k P 1 3 1 P 3 P 1
101 neeq1 k = 3 k 2 3 2
102 98 neeq1d k = 3 P k P 2 P 3 P 2
103 101 102 imbi12d k = 3 k 2 P k P 2 3 2 P 3 P 2
104 100 103 anbi12d k = 3 k 1 P k P 1 k 2 P k P 2 3 1 P 3 P 1 3 2 P 3 P 2
105 87 88 96 104 ralpr k 2 3 k 1 P k P 1 k 2 P k P 2 2 1 P 2 P 1 2 2 P 2 P 2 3 1 P 3 P 1 3 2 P 3 P 2
106 86 105 anbi12i k 0 1 k 1 P k P 1 k 2 P k P 2 k 2 3 k 1 P k P 1 k 2 P k P 2 0 1 P 0 P 1 0 2 P 0 P 2 1 1 P 1 P 1 1 2 P 1 P 2 2 1 P 2 P 1 2 2 P 2 P 2 3 1 P 3 P 1 3 2 P 3 P 2
107 66 67 106 3bitri k 0 ..^ P k 1 P k P 1 k 2 P k P 2 0 1 P 0 P 1 0 2 P 0 P 2 1 1 P 1 P 1 1 2 P 1 P 2 2 1 P 2 P 1 2 2 P 2 P 2 3 1 P 3 P 1 3 2 P 3 P 2
108 59 107 sylibr φ k 0 ..^ P k 1 P k P 1 k 2 P k P 2
109 2 fveq2i F = ⟨“ JKL ”⟩
110 s3len ⟨“ JKL ”⟩ = 3
111 109 110 eqtri F = 3
112 111 oveq2i 1 ..^ F = 1 ..^ 3
113 fzo13pr 1 ..^ 3 = 1 2
114 112 113 eqtri 1 ..^ F = 1 2
115 114 raleqi j 1 ..^ F k j P k P j j 1 2 k j P k P j
116 neeq2 j = 1 k j k 1
117 fveq2 j = 1 P j = P 1
118 117 neeq2d j = 1 P k P j P k P 1
119 116 118 imbi12d j = 1 k j P k P j k 1 P k P 1
120 neeq2 j = 2 k j k 2
121 fveq2 j = 2 P j = P 2
122 121 neeq2d j = 2 P k P j P k P 2
123 120 122 imbi12d j = 2 k j P k P j k 2 P k P 2
124 69 87 119 123 ralpr j 1 2 k j P k P j k 1 P k P 1 k 2 P k P 2
125 115 124 bitri j 1 ..^ F k j P k P j k 1 P k P 1 k 2 P k P 2
126 125 ralbii k 0 ..^ P j 1 ..^ F k j P k P j k 0 ..^ P k 1 P k P 1 k 2 P k P 2
127 108 126 sylibr φ k 0 ..^ P j 1 ..^ F k j P k P j