Step | Hyp | Ref
| Expression |
1 | | mideu.1 |
. . . 4
|
2 | 1 | adantr 481 |
. . 3
|
3 | | colperpex.p |
. . . . 5
|
4 | | colperpex.d |
. . . . 5
|
5 | | colperpex.i |
. . . . 5
Itv |
6 | | colperpex.l |
. . . . 5
LineG |
7 | | mideu.s |
. . . . 5
pInvG |
8 | | colperpex.g |
. . . . . 6
TarskiG |
9 | 8 | adantr 481 |
. . . . 5
TarskiG |
10 | | eqid 2622 |
. . . . 5
|
11 | 3, 4, 5, 6, 7, 9, 2, 10 | mircinv 25563 |
. . . 4
|
12 | | simpr 477 |
. . . 4
|
13 | 11, 12 | eqtr2d 2657 |
. . 3
|
14 | | fveq2 6191 |
. . . . . 6
|
15 | 14 | fveq1d 6193 |
. . . . 5
|
16 | 15 | eqeq2d 2632 |
. . . 4
|
17 | 16 | rspcev 3309 |
. . 3
|
18 | 2, 13, 17 | syl2anc 693 |
. 2
|
19 | 8 | adantr 481 |
. . . . . . . 8
TarskiG |
20 | 19 | ad2antrr 762 |
. . . . . . 7
⟂G
TarskiG |
21 | 20 | ad4antr 768 |
. . . . . 6
⟂G
⟂G ≤G TarskiG |
22 | 1 | adantr 481 |
. . . . . . . 8
|
23 | 22 | ad2antrr 762 |
. . . . . . 7
⟂G
|
24 | 23 | ad4antr 768 |
. . . . . 6
⟂G
⟂G ≤G |
25 | | mideu.2 |
. . . . . . . . 9
|
26 | 25 | adantr 481 |
. . . . . . . 8
|
27 | 26 | ad2antrr 762 |
. . . . . . 7
⟂G
|
28 | 27 | ad4antr 768 |
. . . . . 6
⟂G
⟂G ≤G |
29 | | simpr 477 |
. . . . . . . 8
|
30 | 29 | ad2antrr 762 |
. . . . . . 7
⟂G |
31 | 30 | ad4antr 768 |
. . . . . 6
⟂G
⟂G ≤G |
32 | | simplr 792 |
. . . . . . 7
⟂G |
33 | 32 | ad4antr 768 |
. . . . . 6
⟂G
⟂G ≤G |
34 | | simp-4r 807 |
. . . . . 6
⟂G
⟂G ≤G |
35 | | simpllr 799 |
. . . . . 6
⟂G
⟂G ≤G |
36 | | simp-5r 809 |
. . . . . . . . 9
⟂G
⟂G ≤G ⟂G |
37 | 6, 21, 36 | perpln1 25605 |
. . . . . . . 8
⟂G
⟂G ≤G |
38 | 3, 5, 6, 21, 24, 28, 31 | tgelrnln 25525 |
. . . . . . . 8
⟂G
⟂G ≤G |
39 | 3, 4, 5, 6, 21, 37, 38, 36 | perpcom 25608 |
. . . . . . 7
⟂G
⟂G ≤G ⟂G |
40 | 3, 5, 6, 21, 28, 33, 37 | tglnne 25523 |
. . . . . . . 8
⟂G
⟂G ≤G |
41 | 3, 5, 6, 21, 28, 33, 40 | tglinecom 25530 |
. . . . . . 7
⟂G
⟂G ≤G |
42 | 39, 41 | breqtrd 4679 |
. . . . . 6
⟂G
⟂G ≤G ⟂G |
43 | | simplr 792 |
. . . . . . . . 9
⟂G
⟂G ≤G ⟂G |
44 | 43 | simpld 475 |
. . . . . . . 8
⟂G
⟂G ≤G ⟂G |
45 | 6, 21, 44 | perpln1 25605 |
. . . . . . 7
⟂G
⟂G ≤G |
46 | 3, 4, 5, 6, 21, 45, 38, 44 | perpcom 25608 |
. . . . . 6
⟂G
⟂G ≤G ⟂G |
47 | 31 | neneqd 2799 |
. . . . . . 7
⟂G
⟂G ≤G
|
48 | 43 | simprd 479 |
. . . . . . . . . 10
⟂G
⟂G ≤G |
49 | 48 | simpld 475 |
. . . . . . . . 9
⟂G
⟂G ≤G |
50 | 49 | orcomd 403 |
. . . . . . . 8
⟂G
⟂G ≤G |
51 | 50 | ord 392 |
. . . . . . 7
⟂G
⟂G ≤G
|
52 | 47, 51 | mpd 15 |
. . . . . 6
⟂G
⟂G ≤G |
53 | 48 | simprd 479 |
. . . . . 6
⟂G
⟂G ≤G |
54 | | simpr 477 |
. . . . . 6
⟂G
⟂G ≤G ≤G |
55 | 3, 4, 5, 6, 21, 7,
24, 28, 31, 33, 34, 35, 42, 46, 52, 53, 54 | mideulem 25628 |
. . . . 5
⟂G
⟂G ≤G
|
56 | 20 | ad4antr 768 |
. . . . . . . . 9
⟂G
⟂G ≤G TarskiG |
57 | 56 | adantr 481 |
. . . . . . . 8
⟂G
⟂G ≤G
TarskiG |
58 | | simprl 794 |
. . . . . . . 8
⟂G
⟂G ≤G
|
59 | | eqid 2622 |
. . . . . . . 8
|
60 | 27 | ad4antr 768 |
. . . . . . . . 9
⟂G
⟂G ≤G |
61 | 60 | adantr 481 |
. . . . . . . 8
⟂G
⟂G ≤G
|
62 | | simprr 796 |
. . . . . . . . 9
⟂G
⟂G ≤G
|
63 | 62 | eqcomd 2628 |
. . . . . . . 8
⟂G
⟂G ≤G |
64 | 3, 4, 5, 6, 7, 57,
58, 59, 61, 63 | mircom 25558 |
. . . . . . 7
⟂G
⟂G ≤G |
65 | 64 | eqcomd 2628 |
. . . . . 6
⟂G
⟂G ≤G
|
66 | 23 | ad4antr 768 |
. . . . . . 7
⟂G
⟂G ≤G |
67 | 30 | ad4antr 768 |
. . . . . . . 8
⟂G
⟂G ≤G |
68 | 67 | necomd 2849 |
. . . . . . 7
⟂G
⟂G ≤G |
69 | | simp-4r 807 |
. . . . . . 7
⟂G
⟂G ≤G |
70 | 32 | ad4antr 768 |
. . . . . . 7
⟂G
⟂G ≤G |
71 | | simpllr 799 |
. . . . . . 7
⟂G
⟂G ≤G |
72 | | simplr 792 |
. . . . . . . . . . . . . 14
⟂G
⟂G ≤G ⟂G |
73 | 72 | simpld 475 |
. . . . . . . . . . . . 13
⟂G
⟂G ≤G ⟂G |
74 | 6, 56, 73 | perpln1 25605 |
. . . . . . . . . . . 12
⟂G
⟂G ≤G |
75 | 3, 5, 6, 56, 66, 69, 74 | tglnne 25523 |
. . . . . . . . . . 11
⟂G
⟂G ≤G |
76 | 3, 5, 6, 56, 66, 69, 75 | tglinecom 25530 |
. . . . . . . . . 10
⟂G
⟂G ≤G |
77 | 76 | eqcomd 2628 |
. . . . . . . . 9
⟂G
⟂G ≤G |
78 | 77, 74 | eqeltrd 2701 |
. . . . . . . 8
⟂G
⟂G ≤G |
79 | 3, 5, 6, 56, 60, 66, 68 | tgelrnln 25525 |
. . . . . . . 8
⟂G
⟂G ≤G |
80 | 3, 5, 6, 56, 66, 60, 67 | tglinecom 25530 |
. . . . . . . . 9
⟂G
⟂G ≤G |
81 | 73, 76, 80 | 3brtr3d 4684 |
. . . . . . . 8
⟂G
⟂G ≤G ⟂G |
82 | 3, 4, 5, 6, 56, 78, 79, 81 | perpcom 25608 |
. . . . . . 7
⟂G
⟂G ≤G ⟂G |
83 | | simp-5r 809 |
. . . . . . . . 9
⟂G
⟂G ≤G ⟂G |
84 | 6, 56, 83 | perpln1 25605 |
. . . . . . . 8
⟂G
⟂G ≤G |
85 | 83, 80 | breqtrd 4679 |
. . . . . . . 8
⟂G
⟂G ≤G ⟂G |
86 | 3, 4, 5, 6, 56, 84, 79, 85 | perpcom 25608 |
. . . . . . 7
⟂G
⟂G ≤G ⟂G |
87 | 67 | neneqd 2799 |
. . . . . . . . 9
⟂G
⟂G ≤G
|
88 | 72 | simprd 479 |
. . . . . . . . . . . 12
⟂G
⟂G ≤G |
89 | 88 | simpld 475 |
. . . . . . . . . . 11
⟂G
⟂G ≤G |
90 | 89 | orcomd 403 |
. . . . . . . . . 10
⟂G
⟂G ≤G |
91 | 90 | ord 392 |
. . . . . . . . 9
⟂G
⟂G ≤G
|
92 | 87, 91 | mpd 15 |
. . . . . . . 8
⟂G
⟂G ≤G |
93 | 92, 80 | eleqtrd 2703 |
. . . . . . 7
⟂G
⟂G ≤G |
94 | 88 | simprd 479 |
. . . . . . . 8
⟂G
⟂G ≤G |
95 | 3, 4, 5, 56, 70, 71, 69, 94 | tgbtwncom 25383 |
. . . . . . 7
⟂G
⟂G ≤G |
96 | | simpr 477 |
. . . . . . 7
⟂G
⟂G ≤G ≤G |
97 | 3, 4, 5, 6, 56, 7,
60, 66, 68, 69, 70, 71, 82, 86, 93, 95, 96 | mideulem 25628 |
. . . . . 6
⟂G
⟂G ≤G
|
98 | 65, 97 | reximddv 3018 |
. . . . 5
⟂G
⟂G ≤G
|
99 | | eqid 2622 |
. . . . . 6
≤G ≤G |
100 | 20 | ad3antrrr 766 |
. . . . . 6
⟂G
⟂G TarskiG |
101 | 23 | ad3antrrr 766 |
. . . . . 6
⟂G
⟂G |
102 | | simpllr 799 |
. . . . . 6
⟂G
⟂G |
103 | 27 | ad3antrrr 766 |
. . . . . 6
⟂G
⟂G |
104 | 32 | ad3antrrr 766 |
. . . . . 6
⟂G
⟂G |
105 | 3, 4, 5, 99, 100, 101, 102, 103, 104 | legtrid 25486 |
. . . . 5
⟂G
⟂G ≤G ≤G |
106 | 55, 98, 105 | mpjaodan 827 |
. . . 4
⟂G
⟂G
|
107 | | mideu.3 |
. . . . . . . 8
DimTarskiG≥ |
108 | 107 | adantr 481 |
. . . . . . 7
DimTarskiG≥ |
109 | 108 | ad2antrr 762 |
. . . . . 6
⟂G DimTarskiG≥ |
110 | 3, 4, 5, 6, 20, 23, 27, 32, 30, 109 | colperpex 25625 |
. . . . 5
⟂G
⟂G
|
111 | | r19.42v 3092 |
. . . . . 6
⟂G
⟂G |
112 | 111 | rexbii 3041 |
. . . . 5
⟂G
⟂G |
113 | 110, 112 | sylibr 224 |
. . . 4
⟂G
⟂G |
114 | 106, 113 | r19.29vva 3081 |
. . 3
⟂G
|
115 | 29 | necomd 2849 |
. . . . 5
|
116 | 3, 4, 5, 6, 19, 26, 22, 22, 115, 108 | colperpex 25625 |
. . . 4
⟂G |
117 | | simprl 794 |
. . . . . . 7
⟂G
⟂G |
118 | 3, 5, 6, 19, 22, 26, 29 | tglinecom 25530 |
. . . . . . . 8
|
119 | 118 | adantr 481 |
. . . . . . 7
⟂G
|
120 | 117, 119 | breqtrrd 4681 |
. . . . . 6
⟂G
⟂G |
121 | 120 | ex 450 |
. . . . 5
⟂G
⟂G |
122 | 121 | reximdv 3016 |
. . . 4
⟂G
⟂G |
123 | 116, 122 | mpd 15 |
. . 3
⟂G |
124 | 114, 123 | r19.29a 3078 |
. 2
|
125 | 18, 124 | pm2.61dane 2881 |
1
|