Step | Hyp | Ref
| Expression |
1 | | colperpex.p |
. . . 4
     |
2 | | colperpex.d |
. . . 4
     |
3 | | colperpex.i |
. . . 4
Itv   |
4 | | colperpex.l |
. . . 4
LineG   |
5 | | eqid 2462 |
. . . 4
pInvG  pInvG   |
6 | | colperpex.g |
. . . . 5

TarskiG |
7 | 6 | ad2antrr 737 |
. . . 4
             ⟂G        TarskiG |
8 | | eqid 2462 |
. . . 4
 pInvG      pInvG      |
9 | | colperpex.1 |
. . . . . . . 8
   |
10 | | colperpex.2 |
. . . . . . . 8
   |
11 | | colperpex.4 |
. . . . . . . 8
   |
12 | 1, 3, 4, 6, 9, 10,
11 | tgelrnln 24731 |
. . . . . . 7
       |
13 | 12 | ad2antrr 737 |
. . . . . 6
             ⟂G              |
14 | | simplr 767 |
. . . . . 6
             ⟂G              |
15 | 1, 4, 3, 7, 13, 14 | tglnpt 24650 |
. . . . 5
             ⟂G          |
16 | | eqid 2462 |
. . . . 5
 pInvG      pInvG      |
17 | | colperpex.3 |
. . . . . 6
   |
18 | 17 | ad2antrr 737 |
. . . . 5
             ⟂G          |
19 | 1, 2, 3, 4, 5, 7, 15, 16, 18 | mircl 24762 |
. . . 4
             ⟂G          pInvG          |
20 | 9 | ad2antrr 737 |
. . . . 5
             ⟂G          |
21 | | eqid 2462 |
. . . . 5
 pInvG      pInvG      |
22 | 1, 2, 3, 4, 5, 7, 20, 21, 18 | mircl 24762 |
. . . 4
             ⟂G          pInvG          |
23 | 1, 2, 3, 4, 5, 7, 20, 21, 18 | mircgr 24758 |
. . . . 5
             ⟂G           pInvG             |
24 | 10 | ad2antrr 737 |
. . . . . . 7
             ⟂G          |
25 | | colperpexlem3.1 |
. . . . . . . . . . 11
       |
26 | 25 | ad2antrr 737 |
. . . . . . . . . 10
             ⟂G       
      |
27 | | nelne2 2733 |
. . . . . . . . . 10
     
       |
28 | 14, 26, 27 | syl2anc 671 |
. . . . . . . . 9
             ⟂G          |
29 | 1, 3, 4, 7, 15, 18, 28 | tgelrnln 24731 |
. . . . . . . 8
             ⟂G              |
30 | 1, 3, 4, 7, 15, 18, 28 | tglinecom 24736 |
. . . . . . . . 9
             ⟂G                  |
31 | | simpr 467 |
. . . . . . . . 9
             ⟂G             ⟂G         |
32 | 30, 31 | eqbrtrd 4439 |
. . . . . . . 8
             ⟂G             ⟂G         |
33 | 1, 2, 3, 4, 7, 29,
13, 32 | perpcom 24814 |
. . . . . . 7
             ⟂G             ⟂G         |
34 | 1, 2, 3, 4, 7, 20,
24, 14, 18, 33 | perprag 24824 |
. . . . . 6
             ⟂G              ∟G    |
35 | 1, 2, 3, 4, 5, 7, 20, 15, 18 | israg 24798 |
. . . . . 6
             ⟂G               ∟G 
     pInvG            |
36 | 34, 35 | mpbid 215 |
. . . . 5
             ⟂G             pInvG           |
37 | 23, 36 | eqtr2d 2497 |
. . . 4
             ⟂G           pInvG            pInvG           |
38 | 1, 2, 3, 4, 5, 7, 8, 19, 22, 20, 37 | midexlem 24793 |
. . 3
             ⟂G           pInvG          pInvG         pInvG           |
39 | 7 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
TarskiG |
40 | 22 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG            pInvG          |
41 | 20 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
  |
42 | 18 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
  |
43 | 19 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG            pInvG          |
44 | 15 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
  |
45 | | simplr 767 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
  |
46 | 1, 2, 3, 4, 5, 39,
41, 21, 42 | mirbtwn 24759 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
   pInvG             |
47 | 1, 2, 3, 4, 5, 39,
44, 16, 42 | mirbtwn 24759 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
   pInvG             |
48 | 1, 2, 3, 4, 5, 39,
45, 8, 43 | mirbtwn 24759 |
. . . . . . . . 9
               ⟂G       
   pInvG          pInvG         pInvG         
   pInvG         pInvG             pInvG           |
49 | | simpr 467 |
. . . . . . . . . . 11
               ⟂G       
   pInvG          pInvG         pInvG            pInvG          pInvG         pInvG           |
50 | 49 | eqcomd 2468 |
. . . . . . . . . 10
               ⟂G       
   pInvG          pInvG         pInvG            pInvG         pInvG           pInvG          |
51 | 50 | oveq1d 6335 |
. . . . . . . . 9
               ⟂G       
   pInvG          pInvG         pInvG             pInvG         pInvG             pInvG            pInvG            pInvG           |
52 | 48, 51 | eleqtrd 2542 |
. . . . . . . 8
               ⟂G       
   pInvG          pInvG         pInvG         
   pInvG            pInvG           |
53 | 1, 2, 3, 39, 40, 41, 42, 43, 44, 45, 46, 47, 52 | tgtrisegint 24599 |
. . . . . . 7
               ⟂G       
   pInvG          pInvG         pInvG          
            |
54 | 39 | ad3antrrr 741 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
       TarskiG |
55 | 41 | ad3antrrr 741 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
56 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
57 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
             |
58 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
       
          ⟂G           pInvG          pInvG         pInvG               
         |
59 | 58 | oveq2d 6336 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
60 | 57, 59 | eleqtrd 2542 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
             |
61 | 1, 2, 3, 54, 55, 56, 60 | axtgbtwnid 24570 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
         |
62 | 61 | eqcomd 2468 |
. . . . . . . . . . . . . 14
       
          ⟂G           pInvG          pInvG         pInvG               
         |
63 | 62 | oveq1d 6335 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
64 | 50 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG         pInvG           pInvG          |
65 | 58 | fveq2d 5896 |
. . . . . . . . . . . . . . . . . 18
       
          ⟂G           pInvG          pInvG         pInvG               
        pInvG      pInvG       |
66 | 65 | fveq1d 5894 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG          pInvG          |
67 | 64, 66 | eqtr4d 2499 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG         pInvG           pInvG          |
68 | 45 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
         |
69 | 43 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG          |
70 | 1, 2, 3, 4, 5, 54,
68, 8, 69 | mirinv 24767 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
          pInvG         pInvG           pInvG       
  pInvG           |
71 | 67, 70 | mpbid 215 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG          |
72 | 44 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
         |
73 | 58 | oveq1d 6335 |
. . . . . . . . . . . . . . . . . 18
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
74 | 57, 73 | eleqtrrd 2543 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
             |
75 | 1, 2, 3, 54, 72, 56, 74 | axtgbtwnid 24570 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
76 | 75 | eqcomd 2468 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
         |
77 | 71, 76 | oveq12d 6338 |
. . . . . . . . . . . . . 14
       
          ⟂G           pInvG          pInvG         pInvG               
              pInvG             |
78 | 34 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
               ⟂G       
   pInvG          pInvG         pInvG                ∟G    |
79 | 1, 2, 3, 4, 5, 39,
45, 8, 43, 50 | mircom 24764 |
. . . . . . . . . . . . . . . . . 18
               ⟂G       
   pInvG          pInvG         pInvG            pInvG         pInvG           pInvG          |
80 | 28 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
               ⟂G       
   pInvG          pInvG         pInvG            |
81 | 1, 2, 3, 4, 39, 5,
21, 16, 8, 41, 44, 42, 45, 78, 79, 80 | colperpexlem2 24829 |
. . . . . . . . . . . . . . . . 17
               ⟂G       
   pInvG          pInvG         pInvG            |
82 | 81 | ad3antrrr 741 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
83 | 62, 82 | eqnetrd 2703 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
         |
84 | 1, 3, 4, 54, 56, 68, 83 | tglinecom 24736 |
. . . . . . . . . . . . . 14
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
85 | 42 | ad3antrrr 741 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
86 | 80 | ad3antrrr 741 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
87 | 54 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
TarskiG |
88 | 72 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  |
89 | 85 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  |
90 | 1, 2, 3, 4, 5, 87,
88, 16 | mircinv 24769 |
. . . . . . . . . . . . . . . . . . . 20
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  pInvG          |
91 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . 20
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  pInvG          |
92 | 90, 91 | eqtr4d 2499 |
. . . . . . . . . . . . . . . . . . 19
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  pInvG          pInvG          |
93 | 1, 2, 3, 4, 5, 87,
88, 16, 88, 89, 92 | mireq 24766 |
. . . . . . . . . . . . . . . . . 18
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  |
94 | 86 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  |
95 | 94 | neneqd 2640 |
. . . . . . . . . . . . . . . . . 18
                   ⟂G       
   pInvG          pInvG         pInvG         
               pInvG        
  |
96 | 93, 95 | pm2.65da 584 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG          |
97 | 96 | neqned 2642 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG          |
98 | 47 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . 17
       
          ⟂G           pInvG          pInvG         pInvG               
          pInvG             |
99 | 1, 3, 4, 54, 72, 85, 69, 86, 98 | btwnlng2 24721 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         pInvG              |
100 | 1, 3, 4, 54, 72, 85, 86, 69, 97, 99 | tglineelsb2 24733 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
                pInvG           |
101 | 28 | necomd 2691 |
. . . . . . . . . . . . . . . . 17
             ⟂G          |
102 | 101 | ad5antr 745 |
. . . . . . . . . . . . . . . 16
       
          ⟂G           pInvG          pInvG         pInvG               
         |
103 | 1, 3, 4, 54, 85, 72, 102 | tglinecom 24736 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
104 | 1, 3, 4, 54, 69, 72, 97 | tglinecom 24736 |
. . . . . . . . . . . . . . 15
       
          ⟂G           pInvG          pInvG         pInvG               
          pInvG                pInvG           |
105 | 100, 103,
104 | 3eqtr4d 2506 |
. . . . . . . . . . . . . 14
       
          ⟂G           pInvG          pInvG         pInvG               
              pInvG             |
106 | 77, 84, 105 | 3eqtr4d 2506 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
107 | 63, 106 | eqtr3d 2498 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
                 |
108 | 31 | ad5antr 745 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
            ⟂G         |
109 | 107, 108 | eqbrtrd 4439 |
. . . . . . . . . . 11
       
          ⟂G           pInvG          pInvG         pInvG               
            ⟂G         |
110 | 39 | ad3antrrr 741 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
       TarskiG |
111 | 41 | ad3antrrr 741 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
112 | 45 | ad3antrrr 741 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
113 | 81 | ad3antrrr 741 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
114 | 1, 3, 4, 110, 111, 112, 113 | tgelrnln 24731 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             |
115 | 13 | ad5antr 745 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             |
116 | 1, 3, 4, 110, 111, 112, 113 | tglinerflx1 24734 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
             |
117 | 11 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
             ⟂G          |
118 | 1, 3, 4, 7, 20, 24, 117 | tglinerflx1 24734 |
. . . . . . . . . . . . . 14
             ⟂G              |
119 | 118 | ad5antr 745 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
             |
120 | 116, 119 | elind 3630 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
                   |
121 | 1, 3, 4, 110, 111, 112, 113 | tglinerflx2 24735 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             |
122 | 14 | ad5antr 745 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             |
123 | 113 | necomd 2691 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
         |
124 | | simpr 467 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
         |
125 | 44 | ad3antrrr 741 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
126 | 1, 2, 3, 4, 39, 5,
21, 16, 8, 41, 44, 42, 45, 78, 79 | colperpexlem1 24828 |
. . . . . . . . . . . . . 14
               ⟂G       
   pInvG          pInvG         pInvG                ∟G    |
127 | 126 | ad3antrrr 741 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
             ∟G    |
128 | 1, 2, 3, 4, 5, 110, 125, 111, 112, 127 | ragcom 24799 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             ∟G    |
129 | 1, 2, 3, 4, 110, 114, 115, 120, 121, 122, 123, 124, 128 | ragperp 24818 |
. . . . . . . . . . 11
       
          ⟂G           pInvG          pInvG         pInvG               
            ⟂G         |
130 | 109, 129 | pm2.61dane 2723 |
. . . . . . . . . 10
                 ⟂G        
  pInvG          pInvG         pInvG          
                ⟂G         |
131 | 118 | ad5antr 745 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
             |
132 | 62, 131 | eqeltrd 2540 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             |
133 | 132 | orcd 398 |
. . . . . . . . . . 11
       
          ⟂G           pInvG          pInvG         pInvG               
               |
134 | 24 | ad5antr 745 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
135 | 117 | ad5antr 745 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
136 | | simpllr 774 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
         |
137 | 124 | necomd 2691 |
. . . . . . . . . . . . . 14
       
          ⟂G           pInvG          pInvG         pInvG               
         |
138 | | simplrr 776 |
. . . . . . . . . . . . . 14
       
          ⟂G           pInvG          pInvG         pInvG               
             |
139 | 1, 3, 4, 110, 111, 125, 136, 137, 138 | btwnlng1 24720 |
. . . . . . . . . . . . 13
       
          ⟂G           pInvG          pInvG         pInvG               
             |
140 | 1, 3, 4, 110, 111, 134, 135, 125, 124, 122, 136, 139 | tglineeltr 24732 |
. . . . . . . . . . . 12
       
          ⟂G           pInvG          pInvG         pInvG               
             |
141 | 140 | orcd 398 |
. . . . . . . . . . 11
       
          ⟂G           pInvG          pInvG         pInvG               
               |
142 | 133, 141 | pm2.61dane 2723 |
. . . . . . . . . 10
                 ⟂G        
  pInvG          pInvG         pInvG          
                   |
143 | 39 | ad2antrr 737 |
. . . . . . . . . . 11
                 ⟂G        
  pInvG          pInvG         pInvG          
          
TarskiG |
144 | 45 | ad2antrr 737 |
. . . . . . . . . . 11
                 ⟂G        
  pInvG          pInvG         pInvG          
          
  |
145 | | simplr 767 |
. . . . . . . . . . 11
                 ⟂G        
  pInvG          pInvG         pInvG          
             |
146 | 42 | ad2antrr 737 |
. . . . . . . . . . 11
                 ⟂G        
  pInvG          pInvG         pInvG          
          
  |
147 | | simprl 769 |
. . . . . . . . . . 11
                 ⟂G        
  pInvG          pInvG         pInvG          
                 |
148 | 1, 2, 3, 143, 144, 145, 146, 147 | tgbtwncom 24588 |
. . . . . . . . . 10
                 ⟂G        
  pInvG          pInvG         pInvG          
                 |
149 | 130, 142,
148 | jca32 542 |
. . . . . . . . 9
                 ⟂G        
  pInvG          pInvG         pInvG          
                 ⟂G                      |
150 | 149 | ex 440 |
. . . . . . . 8
     
          ⟂G        
  pInvG          pInvG         pInvG          
     
           ⟂G                       |
151 | 150 | reximdva 2874 |
. . . . . . 7
               ⟂G       
   pInvG          pInvG         pInvG                      
      ⟂G                       |
152 | 53, 151 | mpd 15 |
. . . . . 6
               ⟂G       
   pInvG          pInvG         pInvG          
      ⟂G                      |
153 | | r19.42v 2957 |
. . . . . 6
        ⟂G                   
      ⟂G                       |
154 | 152, 153 | sylib 201 |
. . . . 5
               ⟂G       
   pInvG          pInvG         pInvG                ⟂G       
               |
155 | 154 | ex 440 |
. . . 4
   
          ⟂G            pInvG          pInvG         pInvG               ⟂G       
                |
156 | 155 | reximdva 2874 |
. . 3
             ⟂G         
  pInvG          pInvG         pInvG         
      ⟂G       
                |
157 | 38, 156 | mpd 15 |
. 2
             ⟂G               ⟂G       
               |
158 | 1, 2, 3, 4, 6, 12,
17, 25 | footex 24819 |
. 2
            ⟂G         |
159 | 157, 158 | r19.29a 2944 |
1
        ⟂G       
               |