Proof of Theorem tgbtwnconn1lem2
Step | Hyp | Ref
| Expression |
1 | | tgbtwnconn1.p |
. . . . 5
|
2 | | tgbtwnconn1.m |
. . . . 5
|
3 | | tgbtwnconn1.i |
. . . . 5
Itv |
4 | | tgbtwnconn1.g |
. . . . 5
TarskiG |
5 | | tgbtwnconn1.e |
. . . . 5
|
6 | | tgbtwnconn1.f |
. . . . 5
|
7 | 1, 2, 3, 4, 5, 6 | axtgcgrrflx 25361 |
. . . 4
|
8 | 7 | adantr 481 |
. . 3
|
9 | 4 | adantr 481 |
. . . . . . 7
TarskiG |
10 | 5 | adantr 481 |
. . . . . . 7
|
11 | | tgbtwnconn1.h |
. . . . . . . 8
|
12 | 11 | adantr 481 |
. . . . . . 7
|
13 | | tgbtwnconn1.c |
. . . . . . . 8
|
14 | 13 | adantr 481 |
. . . . . . 7
|
15 | | tgbtwnconn1.10 |
. . . . . . . . 9
|
16 | 15 | adantr 481 |
. . . . . . . 8
|
17 | | simpr 477 |
. . . . . . . . 9
|
18 | 17 | oveq1d 6665 |
. . . . . . . 8
|
19 | 16, 18 | eqtrd 2656 |
. . . . . . 7
|
20 | 1, 2, 3, 9, 10, 12, 14, 19 | axtgcgrid 25362 |
. . . . . 6
|
21 | | tgbtwnconn1.a |
. . . . . . . 8
|
22 | | tgbtwnconn1.b |
. . . . . . . 8
|
23 | | tgbtwnconn1.d |
. . . . . . . 8
|
24 | | tgbtwnconn1.1 |
. . . . . . . 8
|
25 | | tgbtwnconn1.2 |
. . . . . . . 8
|
26 | | tgbtwnconn1.3 |
. . . . . . . 8
|
27 | | tgbtwnconn1.j |
. . . . . . . 8
|
28 | | tgbtwnconn1.4 |
. . . . . . . 8
|
29 | | tgbtwnconn1.5 |
. . . . . . . 8
|
30 | | tgbtwnconn1.6 |
. . . . . . . 8
|
31 | | tgbtwnconn1.7 |
. . . . . . . 8
|
32 | | tgbtwnconn1.8 |
. . . . . . . 8
|
33 | | tgbtwnconn1.9 |
. . . . . . . 8
|
34 | | tgbtwnconn1.11 |
. . . . . . . 8
|
35 | 1, 3, 4, 21, 22, 13, 23, 24, 25, 26, 2, 5, 6, 11, 27, 28, 29, 30, 31, 32, 33, 15, 34 | tgbtwnconn1lem1 25467 |
. . . . . . 7
|
36 | 35 | adantr 481 |
. . . . . 6
|
37 | 20, 36 | eqtrd 2656 |
. . . . 5
|
38 | 37 | oveq2d 6666 |
. . . 4
|
39 | 34 | adantr 481 |
. . . 4
|
40 | 17 | oveq1d 6665 |
. . . 4
|
41 | 38, 39, 40 | 3eqtrd 2660 |
. . 3
|
42 | 8, 41 | eqtrd 2656 |
. 2
|
43 | 4 | adantr 481 |
. . 3
TarskiG |
44 | 6 | adantr 481 |
. . 3
|
45 | 5 | adantr 481 |
. . 3
|
46 | 23 | adantr 481 |
. . 3
|
47 | 13 | adantr 481 |
. . 3
|
48 | 22 | adantr 481 |
. . . 4
|
49 | 27 | adantr 481 |
. . . 4
|
50 | | simpr 477 |
. . . 4
|
51 | 1, 2, 3, 4, 21, 22, 13, 6, 25, 29 | tgbtwnexch3 25389 |
. . . . 5
|
52 | 51 | adantr 481 |
. . . 4
|
53 | 35 | oveq2d 6666 |
. . . . . . . 8
|
54 | 30, 53 | eleqtrd 2703 |
. . . . . . 7
|
55 | 1, 2, 3, 4, 21, 23, 5, 27, 28, 54 | tgbtwnexch3 25389 |
. . . . . 6
|
56 | 1, 2, 3, 4, 23, 5,
27, 55 | tgbtwncom 25383 |
. . . . 5
|
57 | 56 | adantr 481 |
. . . 4
|
58 | 35 | adantr 481 |
. . . . . 6
|
59 | 58 | oveq2d 6666 |
. . . . 5
|
60 | 15 | adantr 481 |
. . . . 5
|
61 | 1, 2, 3, 43, 45, 49 | axtgcgrrflx 25361 |
. . . . 5
|
62 | 59, 60, 61 | 3eqtr3d 2664 |
. . . 4
|
63 | 33, 32 | eqtr4d 2659 |
. . . . 5
|
64 | 63 | adantr 481 |
. . . 4
|
65 | 1, 2, 3, 4, 21, 22, 23, 5, 26, 28 | tgbtwnexch3 25389 |
. . . . . 6
|
66 | 65 | adantr 481 |
. . . . 5
|
67 | 1, 2, 3, 4, 21, 13, 6, 27, 29, 31 | tgbtwnexch3 25389 |
. . . . . . 7
|
68 | 1, 2, 3, 4, 13, 6,
27, 67 | tgbtwncom 25383 |
. . . . . 6
|
69 | 68 | adantr 481 |
. . . . 5
|
70 | 1, 2, 3, 4, 27, 6 | axtgcgrrflx 25361 |
. . . . . . 7
|
71 | 70, 34 | eqtr2d 2657 |
. . . . . 6
|
72 | 71 | adantr 481 |
. . . . 5
|
73 | 1, 2, 3, 4, 13, 6,
5, 23, 63 | tgcgrcomlr 25375 |
. . . . . . 7
|
74 | 73 | adantr 481 |
. . . . . 6
|
75 | 74 | eqcomd 2628 |
. . . . 5
|
76 | 1, 2, 3, 43, 48, 46, 45, 49, 44, 47, 66, 69, 72, 75 | tgcgrextend 25380 |
. . . 4
|
77 | 1, 2, 3, 43, 47, 45 | axtgcgrrflx 25361 |
. . . 4
|
78 | 1, 2, 3, 43, 48, 47, 44, 49, 45, 46, 45, 47, 50, 52, 57, 62, 64, 76, 77 | axtg5seg 25364 |
. . 3
|
79 | 1, 2, 3, 43, 44, 45, 46, 47, 78 | tgcgrcomlr 25375 |
. 2
|
80 | 42, 79 | pm2.61dane 2881 |
1
|