Proof of Theorem hypcgrlem1
Step | Hyp | Ref
| Expression |
1 | | hypcgr.p |
. . 3
|
2 | | hypcgr.m |
. . 3
|
3 | | hypcgr.i |
. . 3
Itv |
4 | | hypcgr.g |
. . . 4
TarskiG |
5 | 4 | adantr 481 |
. . 3
midG
TarskiG |
6 | | hypcgr.c |
. . . 4
|
7 | 6 | adantr 481 |
. . 3
midG
|
8 | | hypcgr.a |
. . . 4
|
9 | 8 | adantr 481 |
. . 3
midG
|
10 | | hypcgr.f |
. . . 4
|
11 | 10 | adantr 481 |
. . 3
midG
|
12 | | hypcgr.d |
. . . 4
|
13 | 12 | adantr 481 |
. . 3
midG
|
14 | | eqid 2622 |
. . . . . . 7
LineG LineG |
15 | | eqid 2622 |
. . . . . . 7
pInvG pInvG |
16 | | hypcgr.b |
. . . . . . 7
|
17 | | hypcgr.1 |
. . . . . . 7
∟G |
18 | 1, 2, 3, 14, 15, 4, 8, 16, 6,
17 | ragcom 25593 |
. . . . . 6
∟G |
19 | 1, 2, 3, 14, 15, 4, 6, 16, 8 | israg 25592 |
. . . . . 6
∟G
pInvG |
20 | 18, 19 | mpbid 222 |
. . . . 5
pInvG |
21 | 20 | adantr 481 |
. . . 4
midG
pInvG |
22 | | hypcgrlem1.a |
. . . . . . 7
|
23 | 22 | eqcomd 2628 |
. . . . . 6
|
24 | 23 | adantr 481 |
. . . . 5
midG
|
25 | | hypcgr.h |
. . . . . . 7
DimTarskiG≥ |
26 | 1, 2, 3, 4, 25, 8,
12, 15, 16 | ismidb 25670 |
. . . . . 6
pInvG
midG |
27 | 26 | biimpar 502 |
. . . . 5
midG
pInvG |
28 | 24, 27 | oveq12d 6668 |
. . . 4
midG
pInvG |
29 | 21, 28 | eqtr4d 2659 |
. . 3
midG
|
30 | 1, 2, 3, 5, 7, 9, 11, 13, 29 | tgcgrcomlr 25375 |
. 2
midG
|
31 | | simpr 477 |
. . . 4
midG
|
32 | 22 | ad2antrr 762 |
. . . 4
midG
|
33 | 31, 32 | oveq12d 6668 |
. . 3
midG
|
34 | 17 | ad2antrr 762 |
. . . . . 6
midG
∟G |
35 | 4 | ad2antrr 762 |
. . . . . . 7
midG
TarskiG |
36 | 8 | ad2antrr 762 |
. . . . . . 7
midG
|
37 | 16 | ad2antrr 762 |
. . . . . . 7
midG
|
38 | 6 | ad2antrr 762 |
. . . . . . 7
midG
|
39 | 1, 2, 3, 14, 15, 35, 36, 37, 38 | israg 25592 |
. . . . . 6
midG
∟G pInvG |
40 | 34, 39 | mpbid 222 |
. . . . 5
midG
pInvG |
41 | 25 | ad2antrr 762 |
. . . . . . 7
midG
DimTarskiG≥ |
42 | | hypcgrlem1.s |
. . . . . . 7
lInvGmidGLineG |
43 | 12 | ad2antrr 762 |
. . . . . . . . 9
midG
|
44 | 1, 2, 3, 35, 41, 36, 43 | midcl 25669 |
. . . . . . . 8
midG
midG |
45 | | simplr 792 |
. . . . . . . 8
midG
midG |
46 | 1, 3, 14, 35, 44, 37, 45 | tgelrnln 25525 |
. . . . . . 7
midG
midGLineG LineG |
47 | | eqid 2622 |
. . . . . . 7
pInvG pInvG |
48 | | eqid 2622 |
. . . . . . . . 9
cgrG cgrG |
49 | 1, 2, 3, 14, 15, 35, 37, 47, 38 | mircl 25556 |
. . . . . . . . 9
midG
pInvG |
50 | | simpr 477 |
. . . . . . . . 9
midG
|
51 | 1, 2, 3, 35, 41, 36, 43 | midbtwn 25671 |
. . . . . . . . . 10
midG
midG |
52 | 1, 14, 3, 35, 36, 44, 43, 51 | btwncolg3 25452 |
. . . . . . . . 9
midG
LineGmidG midG |
53 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
54 | | hypcgrlem2.b |
. . . . . . . . . . . . 13
|
55 | 53, 54, 22 | s3eqd 13609 |
. . . . . . . . . . . 12
|
56 | 55 | ad2antrr 762 |
. . . . . . . . . . 11
midG
|
57 | | hypcgr.2 |
. . . . . . . . . . . 12
∟G |
58 | 57 | ad2antrr 762 |
. . . . . . . . . . 11
midG
∟G |
59 | 56, 58 | eqeltrd 2701 |
. . . . . . . . . 10
midG
∟G |
60 | 1, 2, 3, 14, 15, 35, 43, 37, 38 | israg 25592 |
. . . . . . . . . 10
midG
∟G pInvG |
61 | 59, 60 | mpbid 222 |
. . . . . . . . 9
midG
pInvG |
62 | 1, 14, 3, 35, 36, 43, 44, 48, 38, 49, 2, 50, 52, 40, 61 | lncgr 25464 |
. . . . . . . 8
midG
midG midG pInvG |
63 | 1, 2, 3, 14, 15, 35, 44, 37, 38 | israg 25592 |
. . . . . . . 8
midG
midG ∟G midG midG pInvG |
64 | 62, 63 | mpbird 247 |
. . . . . . 7
midG
midG ∟G |
65 | 1, 3, 14, 35, 44, 37, 45 | tglinerflx1 25528 |
. . . . . . 7
midG
midG midGLineG |
66 | 1, 3, 14, 35, 44, 37, 45 | tglinerflx2 25529 |
. . . . . . 7
midG
midGLineG |
67 | 1, 2, 3, 35, 41, 42, 14, 46, 44, 47, 64, 65, 66, 38, 45 | lmimid 25686 |
. . . . . 6
midG
pInvG |
68 | 67 | oveq2d 6666 |
. . . . 5
midG
pInvG |
69 | 40, 68 | eqtr4d 2659 |
. . . 4
midG
|
70 | 1, 2, 3, 35, 41, 43, 36 | midcom 25674 |
. . . . . . . 8
midG
midG midG |
71 | 70, 65 | eqeltrd 2701 |
. . . . . . 7
midG
midG midGLineG |
72 | 50 | necomd 2849 |
. . . . . . . . . 10
midG
|
73 | 1, 3, 14, 35, 43, 36, 72 | tgelrnln 25525 |
. . . . . . . . 9
midG
LineG LineG |
74 | 1, 2, 3, 35, 36, 44, 43, 51 | tgbtwncom 25383 |
. . . . . . . . . . 11
midG
midG |
75 | 1, 3, 14, 35, 43, 36, 44, 72, 74 | btwnlng1 25514 |
. . . . . . . . . 10
midG
midG LineG |
76 | 65, 75 | elind 3798 |
. . . . . . . . 9
midG
midG midGLineG LineG |
77 | 1, 3, 14, 35, 43, 36, 72 | tglinerflx2 25529 |
. . . . . . . . 9
midG
LineG |
78 | 45 | necomd 2849 |
. . . . . . . . 9
midG
midG |
79 | 4 | ad2antrr 762 |
. . . . . . . . . . . . 13
midG
midG TarskiG |
80 | 8 | ad2antrr 762 |
. . . . . . . . . . . . 13
midG
midG |
81 | 12 | ad2antrr 762 |
. . . . . . . . . . . . 13
midG
midG |
82 | 25 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
midG
midG DimTarskiG≥ |
83 | | simpr 477 |
. . . . . . . . . . . . . . . 16
midG
midG midG |
84 | 83 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
midG
midG midG |
85 | 1, 2, 3, 79, 82, 80, 81, 84 | midcgr 25672 |
. . . . . . . . . . . . . 14
midG
midG |
86 | 85 | eqcomd 2628 |
. . . . . . . . . . . . 13
midG
midG |
87 | 1, 2, 3, 79, 80, 81, 80, 86 | axtgcgrid 25362 |
. . . . . . . . . . . 12
midG
midG |
88 | 87 | ex 450 |
. . . . . . . . . . 11
midG
midG |
89 | 88 | necon3d 2815 |
. . . . . . . . . 10
midG
midG |
90 | 89 | imp 445 |
. . . . . . . . 9
midG
midG |
91 | | hypcgr.e |
. . . . . . . . . . . . . 14
|
92 | | hypcgr.3 |
. . . . . . . . . . . . . 14
|
93 | 1, 2, 3, 4, 8, 16,
12, 91, 92 | tgcgrcomlr 25375 |
. . . . . . . . . . . . 13
|
94 | 54 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
95 | 93, 94 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
96 | 95 | ad2antrr 762 |
. . . . . . . . . . 11
midG
|
97 | | eqidd 2623 |
. . . . . . . . . . . . 13
midG
midG midG |
98 | 1, 2, 3, 35, 41, 36, 43, 15, 44 | ismidb 25670 |
. . . . . . . . . . . . 13
midG
pInvGmidG
midG midG |
99 | 97, 98 | mpbird 247 |
. . . . . . . . . . . 12
midG
pInvGmidG |
100 | 99 | oveq2d 6666 |
. . . . . . . . . . 11
midG
pInvGmidG |
101 | 96, 100 | eqtrd 2656 |
. . . . . . . . . 10
midG
pInvGmidG |
102 | 1, 2, 3, 14, 15, 35, 37, 44, 36 | israg 25592 |
. . . . . . . . . 10
midG
midG ∟G
pInvGmidG |
103 | 101, 102 | mpbird 247 |
. . . . . . . . 9
midG
midG ∟G |
104 | 1, 2, 3, 14, 35, 46, 73, 76, 66, 77, 78, 90, 103 | ragperp 25612 |
. . . . . . . 8
midG
midGLineG⟂GLineG |
105 | 104 | orcd 407 |
. . . . . . 7
midG
midGLineG⟂GLineG |
106 | 1, 2, 3, 35, 41, 42, 14, 46, 43, 36 | islmib 25679 |
. . . . . . 7
midG
midG midGLineG midGLineG⟂GLineG |
107 | 71, 105, 106 | mpbir2and 957 |
. . . . . 6
midG
|
108 | 107 | oveq1d 6665 |
. . . . 5
midG
|
109 | 1, 2, 3, 35, 41, 42, 14, 46, 43, 38 | lmiiso 25689 |
. . . . 5
midG
|
110 | 22 | oveq2d 6666 |
. . . . . 6
|
111 | 110 | ad2antrr 762 |
. . . . 5
midG
|
112 | 108, 109,
111 | 3eqtrd 2660 |
. . . 4
midG
|
113 | 69, 112 | eqtrd 2656 |
. . 3
midG
|
114 | 33, 113 | pm2.61dane 2881 |
. 2
midG
|
115 | 30, 114 | pm2.61dane 2881 |
1
|