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

TarskiG |
7 | 6 | ad3antrrr 744 |
. . . . . . . . . . . . . 14
   


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


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

  pInvG        
            TarskiG |
11 | 10 | ad2antrr 740 |
. . . . . . . . . 10
           


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

  pInvG        
                             pInvG                
TarskiG |
13 | | eqid 2471 |
. . . . . . . . 9
 pInvG      pInvG      |
14 | | foot.x |
. . . . . . . . . . . . 13
   |
15 | 14 | ad3antrrr 744 |
. . . . . . . . . . . 12
   


      
  |
16 | 15 | ad2antrr 740 |
. . . . . . . . . . 11
     
  
      
          
  |
17 | 16 | ad6antr 750 |
. . . . . . . . . 10
           


      
               pInvG        
                       
  |
18 | 17 | ad2antrr 740 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                
  |
19 | | simplr 770 |
. . . . . . . . 9
             
  
      
          

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


      
               pInvG        
  |
21 | 20 | ad2antrr 740 |
. . . . . . . . . . 11
         
  
      
          

  pInvG        
              |
22 | 21 | ad2antrr 740 |
. . . . . . . . . 10
           


      
               pInvG        
                       
  |
23 | 22 | ad2antrr 740 |
. . . . . . . . 9
             
  
      
          

  pInvG        
                             pInvG                   |
24 | | simprr 774 |
. . . . . . . . . 10
             
  
      
          

  pInvG        
                             pInvG                       |
25 | 24 | eqcomd 2477 |
. . . . . . . . 9
             
  
      
          

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

  pInvG        
                             pInvG                 
  pInvG          |
27 | 12 | adantr 472 |
. . . . . . . . . . . . 13
                 
      
          

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

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

  pInvG        
                             pInvG                   |
30 | 29 | adantr 472 |
. . . . . . . . . . . . 13
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
31 | | simprl 772 |
. . . . . . . . . . . . 13
                 
      
          

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

  pInvG        
              |
33 | 32 | ad4antr 746 |
. . . . . . . . . . . . . . 15
             
  
      
          

  pInvG        
                             pInvG                
  |
34 | 33 | adantr 472 |
. . . . . . . . . . . . . 14
                 
      
          

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

  pInvG        
                             pInvG                             |
36 | 35 | simprd 470 |
. . . . . . . . . . . . . . . 16
             
  
      
          

  pInvG        
                             pInvG                       |
37 | 36 | eqcomd 2477 |
. . . . . . . . . . . . . . 15
             
  
      
          

  pInvG        
                             pInvG                       |
38 | 37 | adantr 472 |
. . . . . . . . . . . . . 14
                 
      
          

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

  pInvG        
                             pInvG                
  pInvG          |
40 | 39 | adantr 472 |
. . . . . . . . . . . . . . . . 17
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            pInvG          |
41 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


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


      
               pInvG        
  |
44 | 43 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
  
      
          

  pInvG        
              |
45 | 44 | ad4antr 746 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                   |
46 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
   


         |
47 | 46 | ad10antr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

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

  pInvG        
                             pInvG                         |
49 | 48 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

  pInvG        
                             pInvG                   |
50 | 49 | necomd 2698 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
  
      
          

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

  pInvG        
                             pInvG                             |
52 | 51 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
             
  
      
          

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

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

  pInvG        
                             pInvG                       |
55 | 48 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

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

  pInvG        
                             pInvG                   |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
                 
      
          

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


      
  |
60 | 59 | ad10antr 758 |
. . . . . . . . . . . . . . . . . . . 20
             
  
      
          

  pInvG        
                             pInvG                
  |
61 | 60 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
                 
      
          

  pInvG        
                             pInvG                 
  pInvG         
  |
62 | | nelne2 2740 |
. . . . . . . . . . . . . . . . . . 19
 

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

  pInvG        
                             pInvG                 
  pInvG            |
64 | 63 | necomd 2698 |
. . . . . . . . . . . . . . . . 17
                 
      
          

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

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

  pInvG        
                             pInvG                 
  pInvG             pInvG       
   |
68 | 67 | necon3bid 2687 |
. . . . . . . . . . . . . . . 16
                 
      
          

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

  pInvG        
                             pInvG                 
  pInvG            |
70 | 69 | necomd 2698 |
. . . . . . . . . . . . . 14
                 
      
          

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

  pInvG        
                             pInvG                 
  pInvG            |
72 | 71 | necomd 2698 |
. . . . . . . . . . . . . 14
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
73 | | eqid 2471 |
. . . . . . . . . . . . . . 15
 pInvG      pInvG      |
74 | | simp-4r 785 |
. . . . . . . . . . . . . . . 16
             
  
      
          

  pInvG        
                             pInvG                   |
75 | 74 | adantr 472 |
. . . . . . . . . . . . . . 15
                 
      
          

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


      
               pInvG        
                       
  |
77 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
           


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


      
               pInvG        
                       
  pInvG          |
79 | 78 | ad3antrrr 744 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            pInvG          |
80 | 18 | adantr 472 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG            |
81 | | simpllr 777 |
. . . . . . . . . . . . . . 15
                 
      
          

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

  pInvG        
                             pInvG                 
  pInvG             pInvG             |
83 | 40 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
                 
      
          

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

  pInvG        
                             pInvG                 
  pInvG                |
85 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . 19
             
  
      
          

  pInvG        
                             pInvG                             |
86 | 85 | simpld 466 |
. . . . . . . . . . . . . . . . . 18
             
  
      
          

  pInvG        
                             pInvG                       |
87 | 86 | adantr 472 |
. . . . . . . . . . . . . . . . 17
                 
      
          

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

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

  pInvG        
                             pInvG                 
  pInvG                |
90 | | simplrl 778 |
. . . . . . . . . . . . . . 15
                 
      
          

  pInvG        
                             pInvG                 
  pInvG             pInvG             |
91 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
cgrG  cgrG   |
92 | 51 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

  pInvG        
                             pInvG                       |
93 | 39 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . 21
             
  
      
          

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

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

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

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

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

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

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

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

  pInvG        
                             pInvG                   |
102 | | nelne2 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

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

  pInvG        
                             pInvG                   |
104 | 103 | necomd 2698 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
  
      
          

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

  pInvG        
                             pInvG                   |
106 | 105 | necomd 2698 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

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

  pInvG        
                             pInvG                       |
108 | 35 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . 22
             
  
      
          

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

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

  pInvG        
                   |