Step | Hyp | Ref
| Expression |
1 | | isleag.p |
. . . . 5
|
2 | | cgrg3col4.l |
. . . . 5
LineG |
3 | | eqid 2622 |
. . . . 5
Itv Itv |
4 | | isleag.g |
. . . . . 6
TarskiG |
5 | 4 | ad2antrr 762 |
. . . . 5
TarskiG |
6 | | isleag.a |
. . . . . 6
|
7 | 6 | ad2antrr 762 |
. . . . 5
|
8 | | isleag.b |
. . . . . 6
|
9 | 8 | ad2antrr 762 |
. . . . 5
|
10 | | cgrg3col4.x |
. . . . . 6
|
11 | 10 | ad2antrr 762 |
. . . . 5
|
12 | | eqid 2622 |
. . . . 5
cgrG cgrG |
13 | | isleag.d |
. . . . . 6
|
14 | 13 | ad2antrr 762 |
. . . . 5
|
15 | | isleag.e |
. . . . . 6
|
16 | 15 | ad2antrr 762 |
. . . . 5
|
17 | | eqid 2622 |
. . . . 5
|
18 | | simpr 477 |
. . . . 5
|
19 | | isleag.c |
. . . . . . 7
|
20 | | isleag.f |
. . . . . . 7
|
21 | | cgrg3col4.1 |
. . . . . . 7
cgrG |
22 | 1, 17, 3, 12, 4, 6,
8, 19, 13, 15, 20, 21 | cgr3simp1 25415 |
. . . . . 6
|
23 | 22 | ad2antrr 762 |
. . . . 5
|
24 | 1, 2, 3, 5, 7, 9, 11, 12, 14, 16, 17, 18, 23 | lnext 25462 |
. . . 4
cgrG |
25 | 21 | ad4antr 768 |
. . . . . . . 8
cgrG cgrG |
26 | 5 | ad2antrr 762 |
. . . . . . . . . 10
cgrG TarskiG |
27 | 11 | ad2antrr 762 |
. . . . . . . . . 10
cgrG |
28 | 7 | ad2antrr 762 |
. . . . . . . . . 10
cgrG |
29 | | simplr 792 |
. . . . . . . . . 10
cgrG |
30 | 14 | ad2antrr 762 |
. . . . . . . . . 10
cgrG |
31 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
cgrG |
32 | 16 | ad2antrr 762 |
. . . . . . . . . . 11
cgrG |
33 | | simpr 477 |
. . . . . . . . . . 11
cgrG cgrG |
34 | 1, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33 | cgr3simp3 25417 |
. . . . . . . . . 10
cgrG |
35 | 1, 17, 3, 26, 27, 28, 29, 30, 34 | tgcgrcomlr 25375 |
. . . . . . . . 9
cgrG |
36 | 1, 17, 3, 12, 26, 28, 31, 27, 30, 32, 29, 33 | cgr3simp2 25416 |
. . . . . . . . 9
cgrG |
37 | 19 | ad4antr 768 |
. . . . . . . . . 10
cgrG |
38 | 20 | ad4antr 768 |
. . . . . . . . . 10
cgrG |
39 | | simpr 477 |
. . . . . . . . . . . . 13
|
40 | 39 | ad3antrrr 766 |
. . . . . . . . . . . 12
cgrG |
41 | 40 | oveq2d 6666 |
. . . . . . . . . . 11
cgrG |
42 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
TarskiG |
43 | 6 | adantr 481 |
. . . . . . . . . . . . . 14
|
44 | 19 | adantr 481 |
. . . . . . . . . . . . . 14
|
45 | 13 | adantr 481 |
. . . . . . . . . . . . . 14
|
46 | 20 | adantr 481 |
. . . . . . . . . . . . . 14
|
47 | 1, 17, 3, 12, 4, 6,
8, 19, 13, 15, 20, 21 | cgr3simp3 25417 |
. . . . . . . . . . . . . . . 16
|
48 | 1, 17, 3, 4, 19, 6,
20, 13, 47 | tgcgrcomlr 25375 |
. . . . . . . . . . . . . . 15
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . . 14
|
50 | 1, 17, 3, 42, 43, 44, 45, 46, 49, 39 | tgcgreq 25377 |
. . . . . . . . . . . . 13
|
51 | 50 | ad3antrrr 766 |
. . . . . . . . . . . 12
cgrG |
52 | 51 | oveq2d 6666 |
. . . . . . . . . . 11
cgrG |
53 | 34, 41, 52 | 3eqtr3d 2664 |
. . . . . . . . . 10
cgrG |
54 | 1, 17, 3, 26, 27, 37, 29, 38, 53 | tgcgrcomlr 25375 |
. . . . . . . . 9
cgrG |
55 | 35, 36, 54 | 3jca 1242 |
. . . . . . . 8
cgrG |
56 | 25, 55 | jca 554 |
. . . . . . 7
cgrG cgrG |
57 | 1, 17, 3, 12, 26, 28, 31, 37, 27, 30, 32, 38, 29 | tgcgr4 25426 |
. . . . . . 7
cgrG cgrG
cgrG |
58 | 56, 57 | mpbird 247 |
. . . . . 6
cgrG cgrG |
59 | 58 | ex 450 |
. . . . 5
cgrG cgrG |
60 | 59 | reximdva 3017 |
. . . 4
cgrG cgrG |
61 | 24, 60 | mpd 15 |
. . 3
cgrG |
62 | | eqid 2622 |
. . . . . 6
hlG hlG |
63 | 42 | adantr 481 |
. . . . . . 7
TarskiG |
64 | 63 | ad2antrr 762 |
. . . . . 6
TarskiG |
65 | 8 | ad2antrr 762 |
. . . . . . 7
|
66 | 65 | ad2antrr 762 |
. . . . . 6
|
67 | 43 | adantr 481 |
. . . . . . 7
|
68 | 67 | ad2antrr 762 |
. . . . . 6
|
69 | 10 | ad2antrr 762 |
. . . . . . 7
|
70 | 69 | ad2antrr 762 |
. . . . . 6
|
71 | 15 | ad2antrr 762 |
. . . . . . 7
|
72 | 71 | ad2antrr 762 |
. . . . . 6
|
73 | 45 | adantr 481 |
. . . . . . 7
|
74 | 73 | ad2antrr 762 |
. . . . . 6
|
75 | | simplr 792 |
. . . . . 6
|
76 | | simpr 477 |
. . . . . . 7
|
77 | 76 | ad2antrr 762 |
. . . . . 6
|
78 | | simpr 477 |
. . . . . . . . . 10
|
79 | 22 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
80 | 1, 3, 2, 63, 65, 67, 69, 76 | ncolne1 25520 |
. . . . . . . . . . . . . 14
|
81 | 80 | necomd 2849 |
. . . . . . . . . . . . 13
|
82 | 1, 17, 3, 63, 67, 65, 73, 71, 79, 81 | tgcgrneq 25378 |
. . . . . . . . . . . 12
|
83 | 82 | ad2antrr 762 |
. . . . . . . . . . 11
|
84 | 83 | neneqd 2799 |
. . . . . . . . . 10
|
85 | 78, 84 | jca 554 |
. . . . . . . . 9
|
86 | | ioran 511 |
. . . . . . . . 9
|
87 | 85, 86 | sylibr 224 |
. . . . . . . 8
|
88 | 1, 2, 3, 64, 74, 72, 75, 87 | ncolcom 25456 |
. . . . . . 7
|
89 | 1, 2, 3, 64, 72, 74, 75, 88 | ncolrot1 25457 |
. . . . . 6
|
90 | 1, 17, 3, 4, 6, 8, 13, 15, 22 | tgcgrcomlr 25375 |
. . . . . . 7
|
91 | 90 | ad4antr 768 |
. . . . . 6
|
92 | 1, 17, 3, 2, 62, 64, 66, 68, 70, 72, 74, 75, 77, 89, 91 | trgcopy 25696 |
. . . . 5
cgrG hpG |
93 | 21 | ad6antr 772 |
. . . . . . . . . 10
cgrG cgrG |
94 | 64 | ad2antrr 762 |
. . . . . . . . . . . 12
cgrG TarskiG |
95 | 66 | ad2antrr 762 |
. . . . . . . . . . . 12
cgrG |
96 | 68 | ad2antrr 762 |
. . . . . . . . . . . 12
cgrG |
97 | 70 | ad2antrr 762 |
. . . . . . . . . . . 12
cgrG |
98 | 72 | ad2antrr 762 |
. . . . . . . . . . . 12
cgrG |
99 | 74 | ad2antrr 762 |
. . . . . . . . . . . 12
cgrG |
100 | | simplr 792 |
. . . . . . . . . . . 12
cgrG |
101 | | simpr 477 |
. . . . . . . . . . . 12
cgrG cgrG |
102 | 1, 17, 3, 12, 94, 95, 96, 97, 98, 99, 100, 101 | cgr3simp2 25416 |
. . . . . . . . . . 11
cgrG |
103 | 1, 17, 3, 12, 94, 95, 96, 97, 98, 99, 100, 101 | cgr3simp3 25417 |
. . . . . . . . . . . 12
cgrG |
104 | 1, 17, 3, 94, 97, 95, 100, 98, 103 | tgcgrcomlr 25375 |
. . . . . . . . . . 11
cgrG |
105 | 44 | ad5antr 770 |
. . . . . . . . . . . 12
cgrG |
106 | 46 | ad5antr 770 |
. . . . . . . . . . . 12
cgrG |
107 | 1, 17, 3, 94, 96, 97, 99, 100, 102 | tgcgrcomlr 25375 |
. . . . . . . . . . . . 13
cgrG |
108 | | simp-6r 811 |
. . . . . . . . . . . . . 14
cgrG |
109 | 108 | oveq2d 6666 |
. . . . . . . . . . . . 13
cgrG |
110 | 50 | ad5antr 770 |
. . . . . . . . . . . . . 14
cgrG |
111 | 110 | oveq2d 6666 |
. . . . . . . . . . . . 13
cgrG |
112 | 107, 109,
111 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
cgrG |
113 | 1, 17, 3, 94, 97, 105, 100, 106, 112 | tgcgrcomlr 25375 |
. . . . . . . . . . 11
cgrG |
114 | 102, 104,
113 | 3jca 1242 |
. . . . . . . . . 10
cgrG |
115 | 93, 114 | jca 554 |
. . . . . . . . 9
cgrG cgrG |
116 | 1, 17, 3, 12, 94, 96, 95, 105, 97, 99, 98, 106, 100 | tgcgr4 25426 |
. . . . . . . . 9
cgrG cgrG
cgrG |
117 | 115, 116 | mpbird 247 |
. . . . . . . 8
cgrG cgrG |
118 | 117 | ex 450 |
. . . . . . 7
cgrG cgrG |
119 | 118 | adantrd 484 |
. . . . . 6
cgrG hpG cgrG |
120 | 119 | reximdva 3017 |
. . . . 5
cgrG hpG
cgrG |
121 | 92, 120 | mpd 15 |
. . . 4
cgrG |
122 | 1, 2, 3, 63, 67, 69, 65, 76 | ncoltgdim2 25460 |
. . . . 5
DimTarskiG≥ |
123 | 1, 3, 2, 63, 122, 73, 71, 82 | tglowdim2ln 25546 |
. . . 4
|
124 | 121, 123 | r19.29a 3078 |
. . 3
cgrG |
125 | 61, 124 | pm2.61dan 832 |
. 2
cgrG |
126 | | cgrg3col4.2 |
. . . . . . 7
|
127 | 1, 2, 3, 4, 6, 19,
10, 126 | colcom 25453 |
. . . . . 6
|
128 | 1, 2, 3, 4, 19, 6,
10, 127 | colrot1 25454 |
. . . . 5
|
129 | 1, 2, 3, 4, 6, 19,
10, 12, 13, 20, 17, 128, 48 | lnext 25462 |
. . . 4
cgrG |
130 | 129 | adantr 481 |
. . 3
cgrG |
131 | 21 | ad3antrrr 766 |
. . . . . . 7
cgrG cgrG |
132 | 4 | ad3antrrr 766 |
. . . . . . . . 9
cgrG TarskiG |
133 | 10 | ad3antrrr 766 |
. . . . . . . . 9
cgrG |
134 | 6 | ad3antrrr 766 |
. . . . . . . . 9
cgrG |
135 | | simplr 792 |
. . . . . . . . 9
cgrG |
136 | 13 | ad3antrrr 766 |
. . . . . . . . 9
cgrG |
137 | 19 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
138 | 20 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
139 | | simpr 477 |
. . . . . . . . . 10
cgrG cgrG |
140 | 1, 17, 3, 12, 132, 134, 137, 133, 136, 138, 135, 139 | cgr3simp3 25417 |
. . . . . . . . 9
cgrG |
141 | 1, 17, 3, 132, 133, 134, 135, 136, 140 | tgcgrcomlr 25375 |
. . . . . . . 8
cgrG |
142 | 8 | ad3antrrr 766 |
. . . . . . . . 9
cgrG |
143 | 15 | ad3antrrr 766 |
. . . . . . . . 9
cgrG |
144 | 128 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
145 | 22 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
146 | 1, 17, 3, 12, 4, 6,
8, 19, 13, 15, 20, 21 | cgr3simp2 25416 |
. . . . . . . . . . . 12
|
147 | 1, 17, 3, 4, 8, 19,
15, 20, 146 | tgcgrcomlr 25375 |
. . . . . . . . . . 11
|
148 | 147 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
149 | | simpllr 799 |
. . . . . . . . . 10
cgrG |
150 | 1, 2, 3, 132, 134, 137, 133, 12, 136, 138, 17, 142, 135, 143, 144, 139, 145, 148, 149 | tgfscgr 25463 |
. . . . . . . . 9
cgrG |
151 | 1, 17, 3, 132, 133, 142, 135, 143, 150 | tgcgrcomlr 25375 |
. . . . . . . 8
cgrG |
152 | 1, 17, 3, 12, 132, 134, 137, 133, 136, 138, 135, 139 | cgr3simp2 25416 |
. . . . . . . 8
cgrG |
153 | 141, 151,
152 | 3jca 1242 |
. . . . . . 7
cgrG |
154 | 131, 153 | jca 554 |
. . . . . 6
cgrG cgrG |
155 | 1, 17, 3, 12, 132, 134, 142, 137, 133, 136, 143, 138, 135 | tgcgr4 25426 |
. . . . . 6
cgrG cgrG
cgrG |
156 | 154, 155 | mpbird 247 |
. . . . 5
cgrG cgrG |
157 | 156 | ex 450 |
. . . 4
cgrG cgrG |
158 | 157 | reximdva 3017 |
. . 3
cgrG
cgrG |
159 | 130, 158 | mpd 15 |
. 2
cgrG |
160 | 125, 159 | pm2.61dane 2881 |
1
cgrG |