Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . . 5
     |
2 | | hpg.i |
. . . . 5
Itv   |
3 | | opphl.k |
. . . . 5
hlG   |
4 | | opphllem3.u |
. . . . . 6
   |
5 | 4 | ad4antr 738 |
. . . . 5
                 
       |
6 | | opphllem5.a |
. . . . . 6
   |
7 | 6 | ad4antr 738 |
. . . . 5
                 
       |
8 | | opphl.l |
. . . . . . 7
LineG   |
9 | | opphl.g |
. . . . . . 7

TarskiG |
10 | | opphl.d |
. . . . . . 7
   |
11 | | opphllem5.r |
. . . . . . 7
   |
12 | 1, 8, 2, 9, 10, 11 | tglnpt 24594 |
. . . . . 6
   |
13 | 12 | ad4antr 738 |
. . . . 5
                 
       |
14 | 9 | ad4antr 738 |
. . . . 5
                 
     TarskiG |
15 | | simplr 762 |
. . . . 5
                 
       |
16 | | simprl 764 |
. . . . 5
                 
           |
17 | | opphllem5.p |
. . . . . . . 8
  ⟂G         |
18 | 8, 9, 17 | perpln2 24756 |
. . . . . . 7
       |
19 | 1, 2, 8, 9, 6, 12,
18 | tglnne 24673 |
. . . . . 6
   |
20 | 19 | ad4antr 738 |
. . . . 5
                 
       |
21 | | hpg.d |
. . . . . 6
     |
22 | | opphllem5.c |
. . . . . . 7
   |
23 | 22 | ad4antr 738 |
. . . . . 6
                 
       |
24 | | opphllem5.s |
. . . . . . . 8
   |
25 | 1, 8, 2, 9, 10, 24 | tglnpt 24594 |
. . . . . . 7
   |
26 | 25 | ad4antr 738 |
. . . . . 6
                 
       |
27 | | simprr 766 |
. . . . . . 7
                 
           |
28 | 1, 21, 2, 14, 26, 23, 13, 15, 27 | tgcgrcomlr 24524 |
. . . . . 6
                 
           |
29 | | opphllem5.q |
. . . . . . . . 9
  ⟂G         |
30 | 29 | ad4antr 738 |
. . . . . . . 8
                 
      ⟂G         |
31 | 8, 14, 30 | perpln2 24756 |
. . . . . . 7
                 
           |
32 | 1, 2, 8, 14, 23, 26, 31 | tglnne 24673 |
. . . . . 6
                 
       |
33 | 1, 21, 2, 14, 23, 26, 15, 13, 28, 32 | tgcgrneq 24527 |
. . . . 5
                 
       |
34 | 1, 2, 3, 5, 7, 13,
14, 15, 16, 20, 33 | hlbtwn 24656 |
. . . 4
                 
                     |
35 | | eqid 2451 |
. . . . . . 7
pInvG  pInvG   |
36 | 14 | adantr 467 |
. . . . . . 7
     
            
           
TarskiG |
37 | | opphllem5.n |
. . . . . . 7
 pInvG      |
38 | | opphllem5.m |
. . . . . . . 8
   |
39 | 38 | ad5antr 740 |
. . . . . . 7
     
            
           
  |
40 | 5 | adantr 467 |
. . . . . . 7
     
            
           
  |
41 | 15 | adantr 467 |
. . . . . . 7
     
            
           
  |
42 | 13 | adantr 467 |
. . . . . . 7
     
            
           
  |
43 | | simpr 463 |
. . . . . . 7
     
            
           
        |
44 | 1, 21, 2, 8, 35, 36, 37, 3, 39, 40, 41, 42, 43 | mirhl 24724 |
. . . . . 6
     
            
           
                    |
45 | | eqidd 2452 |
. . . . . . 7
     
            
           
          |
46 | | opphllem3.v |
. . . . . . . . 9
       |
47 | 46 | ad5antr 740 |
. . . . . . . 8
     
            
           
      |
48 | 47 | fveq2d 5869 |
. . . . . . 7
     
            
           
              |
49 | | simprr 766 |
. . . . . . . . . 10
                   
     
   pInvG       
  pInvG            pInvG          |
50 | 14 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG          TarskiG |
51 | | simplr 762 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG            |
52 | 38 | ad6antr 742 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG            |
53 | 26 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG            |
54 | 13 | ad2antrr 732 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG            |
55 | | simprl 764 |
. . . . . . . . . . . . . . 15
                   
     
   pInvG       
  pInvG            pInvG          |
56 | 55 | eqcomd 2457 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG            pInvG          |
57 | 37 | fveq1i 5866 |
. . . . . . . . . . . . . . . 16
      pInvG         |
58 | 1, 21, 2, 8, 35, 9,
38, 37, 12, 46 | mircom 24708 |
. . . . . . . . . . . . . . . 16
       |
59 | 57, 58 | syl5eqr 2499 |
. . . . . . . . . . . . . . 15
   pInvG          |
60 | 59 | ad6antr 742 |
. . . . . . . . . . . . . 14
                   
     
   pInvG       
  pInvG            pInvG          |
61 | 1, 21, 2, 8, 35, 50, 51, 52, 53, 54, 56, 60 | miduniq 24730 |
. . . . . . . . . . . . 13
                   
     
   pInvG       
  pInvG            |
62 | 61 | fveq2d 5869 |
. . . . . . . . . . . 12
                   
     
   pInvG       
  pInvG           pInvG      pInvG       |
63 | 62, 37 | syl6eqr 2503 |
. . . . . . . . . . 11
                   
     
   pInvG       
  pInvG           pInvG       |
64 | 63 | fveq1d 5867 |
. . . . . . . . . 10
                   
     
   pInvG       
  pInvG            pInvG              |
65 | 49, 64 | eqtr2d 2486 |
. . . . . . . . 9
                   
     
   pInvG       
  pInvG                |
66 | | opphllem3.t |
. . . . . . . . . . . 12
   |
67 | 66 | ad4antr 738 |
. . . . . . . . . . 11
                 
       |
68 | 67 | necomd 2679 |
. . . . . . . . . 10
                 
       |
69 | 10 | ad4antr 738 |
. . . . . . . . . . 11
                 
       |
70 | | simp-4r 777 |
. . . . . . . . . . 11
                 
       |
71 | 1, 8, 2, 14, 69, 70 | tglnpt 24594 |
. . . . . . . . . 10
                 
       |
72 | 24 | ad4antr 738 |
. . . . . . . . . . . 12
                 
       |
73 | 11 | ad4antr 738 |
. . . . . . . . . . . 12
                 
       |
74 | 1, 2, 8, 14, 26, 13, 68, 68, 69, 72, 73 | tglinethru 24681 |
. . . . . . . . . . 11
                 
           |
75 | 17 | ad4antr 738 |
. . . . . . . . . . 11
                 
      ⟂G         |
76 | 74, 75 | eqbrtrrd 4425 |
. . . . . . . . . 10
                 
          ⟂G         |
77 | 1, 2, 8, 14, 23, 26, 32 | tglinecom 24680 |
. . . . . . . . . . 11
                 
               |
78 | 30, 74, 77 | 3brtr3d 4432 |
. . . . . . . . . 10
                 
          ⟂G         |
79 | 70, 74 | eleqtrd 2531 |
. . . . . . . . . 10
                 
           |
80 | | simpllr 769 |
. . . . . . . . . 10
                 
           |
81 | 1, 21, 2, 8, 14, 35, 26, 13, 68, 7, 23, 71, 76, 78, 79, 80, 15, 16, 27 | opphllem 24777 |
. . . . . . . . 9
                 
      
  pInvG          pInvG           |
82 | 65, 81 | r19.29a 2932 |
. . . . . . . 8
                 
           |
83 | 82 | adantr 467 |
. . . . . . 7
     
            
           
      |
84 | 45, 48, 83 | breq123d 4416 |
. . . . . 6
     
            
           
                  
             |
85 | 44, 84 | mpbid 214 |
. . . . 5
     
            
           
            |
86 | 14 | adantr 467 |
. . . . . . 7
     
            
               
TarskiG |
87 | 38 | ad5antr 740 |
. . . . . . 7
     
            
               
  |
88 | 1, 21, 2, 8, 35, 9,
38, 37, 4 | mircl 24706 |
. . . . . . . 8
       |
89 | 88 | ad5antr 740 |
. . . . . . 7
     
            
               
      |
90 | 23 | adantr 467 |
. . . . . . 7
     
            
               
  |
91 | 26 | adantr 467 |
. . . . . . 7
     
            
               
  |
92 | | simpr 463 |
. . . . . . 7
     
            
               
            |
93 | 1, 21, 2, 8, 35, 86, 37, 3, 87, 89, 90, 91, 92 | mirhl 24724 |
. . . . . 6
     
            
               
                        |
94 | 5 | adantr 467 |
. . . . . . . 8
     
            
               
  |
95 | 1, 21, 2, 8, 35, 86, 87, 37, 94 | mirmir 24707 |
. . . . . . 7
     
            
               
          |
96 | 13 | adantr 467 |
. . . . . . . . 9
     
            
               
  |
97 | 46 | ad5antr 740 |
. . . . . . . . 9
     
            
               
      |
98 | 1, 21, 2, 8, 35, 86, 87, 37, 96, 97 | mircom 24708 |
. . . . . . . 8
     
            
               
      |
99 | 98 | fveq2d 5869 |
. . . . . . 7
     
            
               
              |
100 | 15 | adantr 467 |
. . . . . . . 8
     
            
               
  |
101 | 82 | adantr 467 |
. . . . . . . 8
     
            
               
      |
102 | 1, 21, 2, 8, 35, 86, 87, 37, 100, 101 | mircom 24708 |
. . . . . . 7
     
            
               
      |
103 | 95, 99, 102 | breq123d 4416 |
. . . . . 6
     
            
               
                                |
104 | 93, 103 | mpbid 214 |
. . . . 5
     
            
               
        |
105 | 85, 104 | impbida 843 |
. . . 4
                 
                         |
106 | 34, 105 | bitrd 257 |
. . 3
                 
                         |
107 | | opphllem3.l |
. . . . 5
    ≤G       |
108 | | eqid 2451 |
. . . . . 6
≤G  ≤G   |
109 | 1, 21, 2, 108, 9, 25, 22, 12, 6 | legov 24630 |
. . . . 5
     ≤G    

             |
110 | 107, 109 | mpbid 214 |
. . . 4
  
           |
111 | 110 | ad2antrr 732 |
. . 3
         
            |
112 | 106, 111 | r19.29a 2932 |
. 2
               
             |
113 | | opphllem5.o |
. . . 4
     |
114 | | hpg.o |
. . . . 5
   
   
           |
115 | 1, 21, 2, 114, 6, 22 | islnopp 24781 |
. . . 4
     
 
        |
116 | 113, 115 | mpbid 214 |
. . 3
  
 
       |
117 | 116 | simprd 465 |
. 2
 
      |
118 | 112, 117 | r19.29a 2932 |
1
                     |