Step | Hyp | Ref
| Expression |
1 | | colperpex.p |
. . . 4
|
2 | | colperpex.d |
. . . 4
|
3 | | colperpex.i |
. . . 4
Itv |
4 | | colperpex.l |
. . . 4
LineG |
5 | | eqid 2622 |
. . . 4
pInvG pInvG |
6 | | colperpex.g |
. . . . 5
TarskiG |
7 | 6 | ad2antrr 762 |
. . . 4
⟂G TarskiG |
8 | | eqid 2622 |
. . . 4
pInvG pInvG |
9 | | colperpex.1 |
. . . . . . . 8
|
10 | | colperpex.2 |
. . . . . . . 8
|
11 | | colperpex.4 |
. . . . . . . 8
|
12 | 1, 3, 4, 6, 9, 10,
11 | tgelrnln 25525 |
. . . . . . 7
|
13 | 12 | ad2antrr 762 |
. . . . . 6
⟂G |
14 | | simplr 792 |
. . . . . 6
⟂G |
15 | 1, 4, 3, 7, 13, 14 | tglnpt 25444 |
. . . . 5
⟂G |
16 | | eqid 2622 |
. . . . 5
pInvG pInvG |
17 | | colperpex.3 |
. . . . . 6
|
18 | 17 | ad2antrr 762 |
. . . . 5
⟂G |
19 | 1, 2, 3, 4, 5, 7, 15, 16, 18 | mircl 25556 |
. . . 4
⟂G pInvG |
20 | 9 | ad2antrr 762 |
. . . . 5
⟂G |
21 | | eqid 2622 |
. . . . 5
pInvG pInvG |
22 | 1, 2, 3, 4, 5, 7, 20, 21, 18 | mircl 25556 |
. . . 4
⟂G pInvG |
23 | 1, 2, 3, 4, 5, 7, 20, 21, 18 | mircgr 25552 |
. . . . 5
⟂G pInvG |
24 | 10 | ad2antrr 762 |
. . . . . . 7
⟂G |
25 | | colperpexlem3.1 |
. . . . . . . . . . 11
|
26 | 25 | ad2antrr 762 |
. . . . . . . . . 10
⟂G
|
27 | | nelne2 2891 |
. . . . . . . . . 10
|
28 | 14, 26, 27 | syl2anc 693 |
. . . . . . . . 9
⟂G |
29 | 1, 3, 4, 7, 15, 18, 28 | tgelrnln 25525 |
. . . . . . . 8
⟂G |
30 | 1, 3, 4, 7, 15, 18, 28 | tglinecom 25530 |
. . . . . . . . 9
⟂G |
31 | | simpr 477 |
. . . . . . . . 9
⟂G ⟂G |
32 | 30, 31 | eqbrtrd 4675 |
. . . . . . . 8
⟂G ⟂G |
33 | 1, 2, 3, 4, 7, 29,
13, 32 | perpcom 25608 |
. . . . . . 7
⟂G ⟂G |
34 | 1, 2, 3, 4, 7, 20,
24, 14, 18, 33 | perprag 25618 |
. . . . . 6
⟂G ∟G |
35 | 1, 2, 3, 4, 5, 7, 20, 15, 18 | israg 25592 |
. . . . . 6
⟂G ∟G
pInvG |
36 | 34, 35 | mpbid 222 |
. . . . 5
⟂G pInvG |
37 | 23, 36 | eqtr2d 2657 |
. . . 4
⟂G pInvG pInvG |
38 | 1, 2, 3, 4, 5, 7, 8, 19, 22, 20, 37 | midexlem 25587 |
. . 3
⟂G pInvG pInvGpInvG |
39 | 7 | ad2antrr 762 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
TarskiG |
40 | 22 | ad2antrr 762 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG pInvG |
41 | 20 | ad2antrr 762 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
|
42 | 18 | ad2antrr 762 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
|
43 | 19 | ad2antrr 762 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG pInvG |
44 | 15 | ad2antrr 762 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
|
45 | | simplr 792 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
|
46 | 1, 2, 3, 4, 5, 39,
41, 21, 42 | mirbtwn 25553 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
pInvG |
47 | 1, 2, 3, 4, 5, 39,
44, 16, 42 | mirbtwn 25553 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
pInvG |
48 | 1, 2, 3, 4, 5, 39,
45, 8, 43 | mirbtwn 25553 |
. . . . . . . . 9
⟂G
pInvG pInvGpInvG
pInvGpInvGpInvG |
49 | | simpr 477 |
. . . . . . . . . . 11
⟂G
pInvG pInvGpInvG pInvG pInvGpInvG |
50 | 49 | eqcomd 2628 |
. . . . . . . . . 10
⟂G
pInvG pInvGpInvG pInvGpInvG pInvG |
51 | 50 | oveq1d 6665 |
. . . . . . . . 9
⟂G
pInvG pInvGpInvG pInvGpInvGpInvG pInvGpInvG |
52 | 48, 51 | eleqtrd 2703 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
pInvGpInvG |
53 | 1, 2, 3, 39, 40, 41, 42, 43, 44, 45, 46, 47, 52 | tgtrisegint 25394 |
. . . . . . 7
⟂G
pInvG pInvGpInvG
|
54 | 39 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
TarskiG |
55 | 41 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
56 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
57 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
|
58 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⟂G pInvG pInvGpInvG
|
59 | 58 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
|
60 | 57, 59 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
61 | 1, 2, 3, 54, 55, 56, 60 | axtgbtwnid 25365 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
|
62 | 61 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⟂G pInvG pInvGpInvG
|
63 | 62 | oveq1d 6665 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
64 | 50 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
pInvGpInvG pInvG |
65 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⟂G pInvG pInvGpInvG
pInvG pInvG |
66 | 65 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
pInvG pInvG |
67 | 64, 66 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
pInvGpInvG pInvG |
68 | 45 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
|
69 | 43 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
pInvG |
70 | 1, 2, 3, 4, 5, 54,
68, 8, 69 | mirinv 25561 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
pInvGpInvG pInvG
pInvG |
71 | 67, 70 | mpbid 222 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
pInvG |
72 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
|
73 | 58 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
⟂G pInvG pInvGpInvG
|
74 | 57, 73 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
|
75 | 1, 2, 3, 54, 72, 56, 74 | axtgbtwnid 25365 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
76 | 75 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
|
77 | 71, 76 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⟂G pInvG pInvGpInvG
pInvG |
78 | 34 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⟂G
pInvG pInvGpInvG ∟G |
79 | 1, 2, 3, 4, 5, 39,
45, 8, 43, 50 | mircom 25558 |
. . . . . . . . . . . . . . . . . 18
⟂G
pInvG pInvGpInvG pInvGpInvG pInvG |
80 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⟂G
pInvG pInvGpInvG |
81 | 1, 2, 3, 4, 39, 5,
21, 16, 8, 41, 44, 42, 45, 78, 79, 80 | colperpexlem2 25623 |
. . . . . . . . . . . . . . . . 17
⟂G
pInvG pInvGpInvG |
82 | 81 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
83 | 62, 82 | eqnetrd 2861 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
|
84 | 1, 3, 4, 54, 56, 68, 83 | tglinecom 25530 |
. . . . . . . . . . . . . 14
⟂G pInvG pInvGpInvG
|
85 | 42 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
86 | 80 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
87 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⟂G
pInvG pInvGpInvG
pInvG
TarskiG |
88 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⟂G
pInvG pInvGpInvG
pInvG
|
89 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⟂G
pInvG pInvGpInvG
pInvG
|
90 | 1, 2, 3, 4, 5, 87,
88, 16 | mircinv 25563 |
. . . . . . . . . . . . . . . . . . . 20
⟂G
pInvG pInvGpInvG
pInvG
pInvG |
91 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⟂G
pInvG pInvGpInvG
pInvG
pInvG |
92 | 90, 91 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
⟂G
pInvG pInvGpInvG
pInvG
pInvG pInvG |
93 | 1, 2, 3, 4, 5, 87,
88, 16, 88, 89, 92 | mireq 25560 |
. . . . . . . . . . . . . . . . . 18
⟂G
pInvG pInvGpInvG
pInvG
|
94 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⟂G
pInvG pInvGpInvG
pInvG
|
95 | 94 | neneqd 2799 |
. . . . . . . . . . . . . . . . . 18
⟂G
pInvG pInvGpInvG
pInvG
|
96 | 93, 95 | pm2.65da 600 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
pInvG |
97 | 96 | neqned 2801 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
pInvG |
98 | 47 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⟂G pInvG pInvGpInvG
pInvG |
99 | 1, 3, 4, 54, 72, 85, 69, 86, 98 | btwnlng2 25515 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
pInvG |
100 | 1, 3, 4, 54, 72, 85, 86, 69, 97, 99 | tglineelsb2 25527 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
pInvG |
101 | 28 | necomd 2849 |
. . . . . . . . . . . . . . . . 17
⟂G |
102 | 101 | ad5antr 770 |
. . . . . . . . . . . . . . . 16
⟂G pInvG pInvGpInvG
|
103 | 1, 3, 4, 54, 85, 72, 102 | tglinecom 25530 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
|
104 | 1, 3, 4, 54, 69, 72, 97 | tglinecom 25530 |
. . . . . . . . . . . . . . 15
⟂G pInvG pInvGpInvG
pInvG pInvG |
105 | 100, 103,
104 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
⟂G pInvG pInvGpInvG
pInvG |
106 | 77, 84, 105 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
107 | 63, 106 | eqtr3d 2658 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
108 | 31 | ad5antr 770 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
⟂G |
109 | 107, 108 | eqbrtrd 4675 |
. . . . . . . . . . 11
⟂G pInvG pInvGpInvG
⟂G |
110 | 39 | ad3antrrr 766 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
TarskiG |
111 | 41 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
112 | 45 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
113 | 81 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
114 | 1, 3, 4, 110, 111, 112, 113 | tgelrnln 25525 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
115 | 13 | ad5antr 770 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
116 | 1, 3, 4, 110, 111, 112, 113 | tglinerflx1 25528 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
117 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⟂G |
118 | 1, 3, 4, 7, 20, 24, 117 | tglinerflx1 25528 |
. . . . . . . . . . . . . 14
⟂G |
119 | 118 | ad5antr 770 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
120 | 116, 119 | elind 3798 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
121 | 1, 3, 4, 110, 111, 112, 113 | tglinerflx2 25529 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
122 | 14 | ad5antr 770 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
123 | 113 | necomd 2849 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
124 | | simpr 477 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
125 | 44 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
126 | 1, 2, 3, 4, 39, 5,
21, 16, 8, 41, 44, 42, 45, 78, 79 | colperpexlem1 25622 |
. . . . . . . . . . . . . 14
⟂G
pInvG pInvGpInvG ∟G |
127 | 126 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
∟G |
128 | 1, 2, 3, 4, 5, 110, 125, 111, 112, 127 | ragcom 25593 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
∟G |
129 | 1, 2, 3, 4, 110, 114, 115, 120, 121, 122, 123, 124, 128 | ragperp 25612 |
. . . . . . . . . . 11
⟂G pInvG pInvGpInvG
⟂G |
130 | 109, 129 | pm2.61dane 2881 |
. . . . . . . . . 10
⟂G
pInvG pInvGpInvG
⟂G |
131 | 118 | ad5antr 770 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
132 | 62, 131 | eqeltrd 2701 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
133 | 132 | orcd 407 |
. . . . . . . . . . 11
⟂G pInvG pInvGpInvG
|
134 | 24 | ad5antr 770 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
135 | 117 | ad5antr 770 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
136 | | simpllr 799 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
137 | 124 | necomd 2849 |
. . . . . . . . . . . . . 14
⟂G pInvG pInvGpInvG
|
138 | | simplrr 801 |
. . . . . . . . . . . . . 14
⟂G pInvG pInvGpInvG
|
139 | 1, 3, 4, 110, 111, 125, 136, 137, 138 | btwnlng1 25514 |
. . . . . . . . . . . . 13
⟂G pInvG pInvGpInvG
|
140 | 1, 3, 4, 110, 111, 134, 135, 125, 124, 122, 136, 139 | tglineeltr 25526 |
. . . . . . . . . . . 12
⟂G pInvG pInvGpInvG
|
141 | 140 | orcd 407 |
. . . . . . . . . . 11
⟂G pInvG pInvGpInvG
|
142 | 133, 141 | pm2.61dane 2881 |
. . . . . . . . . 10
⟂G
pInvG pInvGpInvG
|
143 | 39 | ad2antrr 762 |
. . . . . . . . . . 11
⟂G
pInvG pInvGpInvG
TarskiG |
144 | 45 | ad2antrr 762 |
. . . . . . . . . . 11
⟂G
pInvG pInvGpInvG
|
145 | | simplr 792 |
. . . . . . . . . . 11
⟂G
pInvG pInvGpInvG
|
146 | 42 | ad2antrr 762 |
. . . . . . . . . . 11
⟂G
pInvG pInvGpInvG
|
147 | | simprl 794 |
. . . . . . . . . . 11
⟂G
pInvG pInvGpInvG
|
148 | 1, 2, 3, 143, 144, 145, 146, 147 | tgbtwncom 25383 |
. . . . . . . . . 10
⟂G
pInvG pInvGpInvG
|
149 | 130, 142,
148 | jca32 558 |
. . . . . . . . 9
⟂G
pInvG pInvGpInvG
⟂G |
150 | 149 | ex 450 |
. . . . . . . 8
⟂G
pInvG pInvGpInvG
⟂G |
151 | 150 | reximdva 3017 |
. . . . . . 7
⟂G
pInvG pInvGpInvG
⟂G |
152 | 53, 151 | mpd 15 |
. . . . . 6
⟂G
pInvG pInvGpInvG
⟂G |
153 | | r19.42v 3092 |
. . . . . 6
⟂G
⟂G |
154 | 152, 153 | sylib 208 |
. . . . 5
⟂G
pInvG pInvGpInvG ⟂G
|
155 | 154 | ex 450 |
. . . 4
⟂G pInvG pInvGpInvG ⟂G
|
156 | 155 | reximdva 3017 |
. . 3
⟂G
pInvG pInvGpInvG
⟂G
|
157 | 38, 156 | mpd 15 |
. 2
⟂G ⟂G
|
158 | 1, 2, 3, 4, 6, 12,
17, 25 | footex 25613 |
. 2
⟂G |
159 | 157, 158 | r19.29a 3078 |
1
⟂G
|