Step | Hyp | Ref
| Expression |
1 | | isperp.p |
. . . . . . . . 9
     |
2 | | isperp.d |
. . . . . . . . 9
     |
3 | | isperp.i |
. . . . . . . . 9
Itv   |
4 | | isperp.l |
. . . . . . . . 9
LineG   |
5 | | eqid 2451 |
. . . . . . . . 9
pInvG  pInvG   |
6 | | isperp.g |
. . . . . . . . . . . . . . 15

TarskiG |
7 | 6 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
   


      
TarskiG |
8 | 7 | ad2antrr 732 |
. . . . . . . . . . . . 13
     
  
      
          
TarskiG |
9 | 8 | ad2antrr 732 |
. . . . . . . . . . . 12
       


      
               pInvG        
TarskiG |
10 | 9 | ad2antrr 732 |
. . . . . . . . . . 11
         
  
      
          

  pInvG        
            TarskiG |
11 | 10 | ad2antrr 732 |
. . . . . . . . . 10
           


      
               pInvG        
                       
TarskiG |
12 | 11 | ad2antrr 732 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                
TarskiG |
13 | | eqid 2451 |
. . . . . . . . 9
 pInvG      pInvG      |
14 | | foot.x |
. . . . . . . . . . . . 13
   |
15 | 14 | ad3antrrr 736 |
. . . . . . . . . . . 12
   


      
  |
16 | 15 | ad2antrr 732 |
. . . . . . . . . . 11
     
  
      
          
  |
17 | 16 | ad6antr 742 |
. . . . . . . . . 10
           


      
               pInvG        
                       
  |
18 | 17 | ad2antrr 732 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                
  |
19 | | simplr 762 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                   |
20 | | simp-4r 777 |
. . . . . . . . . . . 12
       


      
               pInvG        
  |
21 | 20 | ad2antrr 732 |
. . . . . . . . . . 11
         
  
      
          

  pInvG        
              |
22 | 21 | ad2antrr 732 |
. . . . . . . . . 10
           


      
               pInvG        
                       
  |
23 | 22 | ad2antrr 732 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                   |
24 | | simprr 766 |
. . . . . . . . . 10
             
  
      
          

  pInvG        
                             pInvG                       |
25 | 24 | eqcomd 2457 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                       |
26 | 1, 2, 3, 4, 5, 12,
13, 18, 19, 23, 25 | midexlem 24737 |
. . . . . . . 8
             
  
      
          

  pInvG        
                             pInvG                 
  pInvG          |
27 | 12 | adantr 467 |
. . . . . . . . . . . . 13
                 
      
          

  pInvG        
                             pInvG                 
  pInvG          TarskiG |
28 | 23 | adantr 467 |
. . . . . . . . . . . . 13
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
29 | | simp-6r 781 |
. . . . . . . . . . . . . 14
             
  
      
          

  pInvG        
                             pInvG                   |
30 | 29 | adantr 467 |
. . . . . . . . . . . . 13
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
31 | | simprl 764 |
. . . . . . . . . . . . 13
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
32 | | simp-4r 777 |
. . . . . . . . . . . . . . . 16
         
  
      
          

  pInvG        
              |
33 | 32 | ad4antr 738 |
. . . . . . . . . . . . . . 15
             
  
      
          

  pInvG        
                             pInvG                
  |
34 | 33 | adantr 467 |
. . . . . . . . . . . . . 14
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
35 | | simp-5r 779 |
. . . . . . . . . . . . . . . . 17
             
  
      
          

  pInvG        
                             pInvG                             |
36 | 35 | simprd 465 |
. . . . . . . . . . . . . . . 16
             
  
      
          

  pInvG        
                             pInvG                       |
37 | 36 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
             
  
      
          

  pInvG        
                             pInvG                       |
38 | 37 | adantr 467 |
. . . . . . . . . . . . . 14
                 
      
          

  pInvG        
                             pInvG                 
  pInvG                |
39 | | simp-7r 783 |
. . . . . . . . . . . . . . . . . 18
             
  
      
          

  pInvG        
                             pInvG                
  pInvG          |
40 | 39 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            pInvG          |
41 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


         |
42 | 41 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
  
      
             |
43 | 42 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       


      
               pInvG        
  |
44 | 43 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
  
      
          

  pInvG        
              |
45 | 44 | ad4antr 738 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                   |
46 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


         |
47 | 46 | ad10antr 750 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                   |
48 | | simp-11r 791 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
  
      
          

  pInvG        
                             pInvG                         |
49 | 48 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                   |
50 | 49 | necomd 2679 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
  
      
          

  pInvG        
                             pInvG                   |
51 | | simp-9r 787 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
  
      
          

  pInvG        
                             pInvG                             |
52 | 51 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
  
      
          

  pInvG        
                             pInvG                       |
53 | 1, 3, 4, 12, 47, 45, 23, 50, 52 | btwnlng3 24666 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                       |
54 | 1, 3, 4, 12, 45, 47, 23, 49, 53 | lncom 24667 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

  pInvG        
                             pInvG                       |
55 | 48 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

  pInvG        
                             pInvG                
      |
56 | 54, 55 | eleqtrrd 2532 |
. . . . . . . . . . . . . . . . . . . 20
             
  
      
          

  pInvG        
                             pInvG                   |
57 | 56 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
58 | | foot.y |
. . . . . . . . . . . . . . . . . . . . . 22
   |
59 | 58 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . 21
   


      
  |
60 | 59 | ad10antr 750 |
. . . . . . . . . . . . . . . . . . . 20
             
  
      
          

  pInvG        
                             pInvG                
  |
61 | 60 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
                 
      
          

  pInvG        
                             pInvG                 
  pInvG         
  |
62 | | nelne2 2721 |
. . . . . . . . . . . . . . . . . . 19
 

  |
63 | 57, 61, 62 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
64 | 63 | necomd 2679 |
. . . . . . . . . . . . . . . . 17
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
65 | 40, 64 | eqnetrrd 2692 |
. . . . . . . . . . . . . . . 16
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            pInvG          |
66 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
 pInvG      pInvG      |
67 | 1, 2, 3, 4, 5, 27,
34, 66, 28 | mirinv 24711 |
. . . . . . . . . . . . . . . . 17
                 
      
          

  pInvG        
                             pInvG                 
  pInvG             pInvG       
   |
68 | 67 | necon3bid 2668 |
. . . . . . . . . . . . . . . 16
                 
      
          

  pInvG        
                             pInvG                 
  pInvG             pInvG       
   |
69 | 65, 68 | mpbid 214 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
70 | 69 | necomd 2679 |
. . . . . . . . . . . . . 14
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
71 | 1, 2, 3, 27, 28, 34, 28, 30, 38, 70 | tgcgrneq 24527 |
. . . . . . . . . . . . 13
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
72 | 71 | necomd 2679 |
. . . . . . . . . . . . . 14
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
73 | | eqid 2451 |
. . . . . . . . . . . . . . 15
 pInvG      pInvG      |
74 | | simp-4r 777 |
. . . . . . . . . . . . . . . 16
             
  
      
          

  pInvG        
                             pInvG                   |
75 | 74 | adantr 467 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
76 | | simp-4r 777 |
. . . . . . . . . . . . . . . . 17
           


      
               pInvG        
                       
  |
77 | | simplr 762 |
. . . . . . . . . . . . . . . . 17
           


      
               pInvG        
                       
  |
78 | 1, 2, 3, 4, 5, 11,
76, 73, 77 | mircl 24706 |
. . . . . . . . . . . . . . . 16
           


      
               pInvG        
                       
  pInvG          |
79 | 78 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            pInvG          |
80 | 18 | adantr 467 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
81 | | simpllr 769 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
82 | 1, 2, 3, 4, 5, 27,
34, 66, 28 | mirbtwn 24703 |
. . . . . . . . . . . . . . . . . 18
                 
      
          

  pInvG        
                             pInvG                 
  pInvG             pInvG             |
83 | 40 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . 18
                 
      
          

  pInvG        
                             pInvG                 
  pInvG                 pInvG             |
84 | 82, 83 | eleqtrrd 2532 |
. . . . . . . . . . . . . . . . 17
                 
      
          

  pInvG        
                             pInvG                 
  pInvG                |
85 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . 19
             
  
      
          

  pInvG        
                             pInvG                             |
86 | 85 | simpld 461 |
. . . . . . . . . . . . . . . . . 18
             
  
      
          

  pInvG        
                             pInvG                       |
87 | 86 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                 
      
          

  pInvG        
                             pInvG                 
  pInvG                |
88 | 1, 2, 3, 27, 80, 34, 28, 75, 69, 84, 87 | tgbtwnouttr2 24539 |
. . . . . . . . . . . . . . . 16
                 
      
          

  pInvG        
                             pInvG                 
  pInvG                |
89 | 1, 2, 3, 27, 80, 28, 75, 88 | tgbtwncom 24532 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG                |
90 | | simplrl 770 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG             pInvG             |
91 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
cgrG  cgrG   |
92 | 51 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

  pInvG        
                             pInvG                       |
93 | 39 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

  pInvG        
                             pInvG                      pInvG           |
94 | 92, 93 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . 20
             
  
      
          

  pInvG        
                             pInvG                      pInvG           |
95 | 1, 2, 3, 4, 5, 12,
45, 33, 23 | israg 24742 |
. . . . . . . . . . . . . . . . . . . 20
             
  
      
          

  pInvG        
                             pInvG                        ∟G 
     pInvG            |
96 | 94, 95 | mpbird 236 |
. . . . . . . . . . . . . . . . . . 19
             
  
      
          

  pInvG        
                             pInvG                       ∟G    |
97 | 85 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
  
      
          

  pInvG        
                             pInvG                       |
98 | 1, 2, 3, 12, 45, 23, 45, 18, 92 | tgcgrcomlr 24524 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
  
      
          

  pInvG        
                             pInvG                       |
99 | 97, 98 | eqtr2d 2486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
  
      
          

  pInvG        
                             pInvG                       |
100 | 1, 3, 4, 12, 45, 47, 49 | tglinerflx1 24678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             
  
      
          

  pInvG        
                             pInvG                       |
101 | 100, 55 | eleqtrrd 2532 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
  
      
          

  pInvG        
                             pInvG                   |
102 | | nelne2 2721 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

  |
103 | 101, 60, 102 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
  
      
          

  pInvG        
                             pInvG                   |
104 | 103 | necomd 2679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
  
      
          

  pInvG        
                             pInvG                   |
105 | 1, 2, 3, 12, 18, 45, 23, 74, 99, 104 | tgcgrneq 24527 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
  
      
          

  pInvG        
                             pInvG                   |
106 | 105 | necomd 2679 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                   |
107 | 1, 2, 3, 12, 33, 23, 74, 86 | tgbtwncom 24532 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                       |
108 | 35 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                       |
109 | 1, 2, 3, 12, 23, 74, 23, 45, 97 | tgcgrcomlr 24524 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                       |
110 | 1, 2, 3, 12, 74, 45 | axtgcgrrflx 24510 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                   |