Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . . . 6
|
2 | | hpg.d |
. . . . . 6
|
3 | | hpg.i |
. . . . . 6
Itv |
4 | | hpg.o |
. . . . . 6
|
5 | | opphl.l |
. . . . . 6
LineG |
6 | | opphl.d |
. . . . . . 7
|
7 | 6 | ad8antr 776 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G
|
8 | | opphl.g |
. . . . . . 7
TarskiG |
9 | 8 | ad8antr 776 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G
TarskiG |
10 | | opphl.k |
. . . . . 6
hlG |
11 | | eqid 2622 |
. . . . . 6
pInvG pInvG |
12 | | opphl.b |
. . . . . . 7
|
13 | 12 | ad8antr 776 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G
|
14 | | eqid 2622 |
. . . . . . 7
pInvG pInvG |
15 | | simp-4r 807 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G
|
16 | | opphl.a |
. . . . . . . 8
|
17 | 16 | ad8antr 776 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G
|
18 | 1, 2, 3, 5, 14, 9,
15, 11, 17 | mircl 25556 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G pInvG |
19 | | simplr 792 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G |
20 | | simp-6r 811 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G |
21 | | opphl.2 |
. . . . . . . 8
|
22 | 21 | ad8antr 776 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G
|
23 | | opphl.c |
. . . . . . . . 9
|
24 | 23 | ad8antr 776 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G
|
25 | | simp-8r 815 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G
|
26 | | opphl.1 |
. . . . . . . . 9
|
27 | 26 | ad8antr 776 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G |
28 | | simp-7r 813 |
. . . . . . . . . 10
⟂G
⟂G
pInvG
⟂G ⟂G |
29 | 5, 9, 28 | perpln1 25605 |
. . . . . . . . 9
⟂G
⟂G
pInvG
⟂G |
30 | 1, 2, 3, 5, 9, 29,
7, 28 | perpcom 25608 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G ⟂G |
31 | | simp-5r 809 |
. . . . . . . . . 10
⟂G
⟂G
pInvG
⟂G ⟂G |
32 | 5, 9, 31 | perpln1 25605 |
. . . . . . . . 9
⟂G
⟂G
pInvG
⟂G |
33 | 1, 2, 3, 5, 9, 32,
7, 31 | perpcom 25608 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G ⟂G |
34 | 1, 5, 3, 9, 7, 25 | tglnpt 25444 |
. . . . . . . . 9
⟂G
⟂G
pInvG
⟂G
|
35 | 1, 3, 5, 9, 17, 34, 29 | tglnne 25523 |
. . . . . . . . 9
⟂G
⟂G
pInvG
⟂G |
36 | 1, 3, 10, 17, 17, 34, 9, 35 | hlid 25504 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G |
37 | | simpllr 799 |
. . . . . . . . . . 11
⟂G
⟂G
pInvG
⟂G pInvG |
38 | 37 | eqcomd 2628 |
. . . . . . . . . 10
⟂G
⟂G
pInvG
⟂G pInvG |
39 | 1, 2, 3, 4, 5, 7, 9, 10, 11, 17, 24, 25, 20, 15, 27, 30, 33, 17, 38 | opphllem6 25644 |
. . . . . . . . 9
⟂G
⟂G
pInvG
⟂G pInvG |
40 | 36, 39 | mpbid 222 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G pInvG |
41 | 1, 2, 3, 4, 5, 7, 9, 10, 11, 17, 24, 25, 20, 15, 27, 30, 33, 17, 18, 36, 40 | opphllem5 25643 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G pInvG |
42 | 38, 20 | eqeltrd 2701 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G pInvG |
43 | 1, 2, 3, 5, 14, 9,
11, 7, 15, 25, 42 | mirln2 25572 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G
|
44 | 1, 2, 3, 5, 14, 9,
15, 11, 17 | mirmir 25557 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G pInvGpInvG |
45 | 44 | eqcomd 2628 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G
pInvGpInvG |
46 | 1, 5, 3, 8, 6, 21 | tglnpt 25444 |
. . . . . . . . 9
|
47 | | opphl.3 |
. . . . . . . . 9
|
48 | 1, 3, 10, 16, 12, 46, 8, 47 | hlne1 25500 |
. . . . . . . 8
|
49 | 48 | ad8antr 776 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G |
50 | 1, 3, 10, 16, 12, 46, 8, 5, 47 | hlln 25502 |
. . . . . . . . 9
|
51 | 1, 5, 3, 8, 12, 46, 50 | tglngne 25445 |
. . . . . . . 8
|
52 | 51 | ad8antr 776 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G |
53 | 1, 3, 10, 16, 12, 46, 8 | ishlg 25497 |
. . . . . . . . . 10
|
54 | 47, 53 | mpbid 222 |
. . . . . . . . 9
|
55 | 54 | simp3d 1075 |
. . . . . . . 8
|
56 | 55 | ad8antr 776 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G |
57 | 1, 2, 3, 4, 5, 7, 9, 11, 17, 13, 18, 22, 41, 43, 45, 49, 52, 56 | opphllem2 25640 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G pInvG |
58 | | simpr 477 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G ⟂G |
59 | 5, 9, 58 | perpln1 25605 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G |
60 | 1, 2, 3, 5, 9, 59,
7, 58 | perpcom 25608 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G ⟂G |
61 | 1, 5, 3, 9, 7, 20 | tglnpt 25444 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G |
62 | 1, 3, 10, 18, 24, 61, 9, 40 | hlne1 25500 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G pInvG |
63 | 1, 3, 10, 18, 24, 61, 9, 5, 40 | hlln 25502 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G pInvG |
64 | 1, 5, 3, 9, 24, 61, 63 | tglngne 25445 |
. . . . . . . . 9
⟂G
⟂G
pInvG
⟂G |
65 | 1, 3, 5, 9, 24, 61, 64 | tglinerflx2 25529 |
. . . . . . . 8
⟂G
⟂G
pInvG
⟂G |
66 | 1, 3, 5, 9, 18, 61, 62, 62, 32, 63, 65 | tglinethru 25531 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G pInvG |
67 | 33, 66 | breqtrd 4679 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G ⟂GpInvG |
68 | 1, 5, 3, 9, 7, 19 | tglnpt 25444 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G |
69 | 1, 3, 5, 9, 13, 68, 59 | tglnne 25523 |
. . . . . . 7
⟂G
⟂G
pInvG
⟂G |
70 | 1, 3, 10, 13, 17, 68, 9, 69 | hlid 25504 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G |
71 | 1, 3, 10, 18, 24, 61, 9, 40 | hlcomd 25499 |
. . . . . 6
⟂G
⟂G
pInvG
⟂G pInvG |
72 | 1, 2, 3, 4, 5, 7, 9, 10, 11, 13, 18, 19, 20, 15, 57, 60, 67, 13, 24, 70, 71 | opphllem5 25643 |
. . . . 5
⟂G
⟂G
pInvG
⟂G |
73 | 1, 2, 3, 4, 5, 6, 8, 16, 23, 26 | oppne1 25633 |
. . . . . . . 8
|
74 | 50 | adantr 481 |
. . . . . . . . 9
|
75 | 8 | adantr 481 |
. . . . . . . . . 10
TarskiG |
76 | 12 | adantr 481 |
. . . . . . . . . 10
|
77 | 46 | adantr 481 |
. . . . . . . . . 10
|
78 | 51 | adantr 481 |
. . . . . . . . . 10
|
79 | 6 | adantr 481 |
. . . . . . . . . 10
|
80 | | simpr 477 |
. . . . . . . . . 10
|
81 | 21 | adantr 481 |
. . . . . . . . . 10
|
82 | 1, 3, 5, 75, 76, 77, 78, 78, 79, 80, 81 | tglinethru 25531 |
. . . . . . . . 9
|
83 | 74, 82 | eleqtrrd 2704 |
. . . . . . . 8
|
84 | 73, 83 | mtand 691 |
. . . . . . 7
|
85 | 1, 2, 3, 5, 8, 6, 12, 84 | footex 25613 |
. . . . . 6
⟂G |
86 | 85 | ad6antr 772 |
. . . . 5
⟂G
⟂G
pInvG
⟂G |
87 | 72, 86 | r19.29a 3078 |
. . . 4
⟂G
⟂G
pInvG
|
88 | 8 | ad4antr 768 |
. . . . 5
⟂G
⟂G
TarskiG |
89 | 6 | ad4antr 768 |
. . . . . 6
⟂G
⟂G
|
90 | | simp-4r 807 |
. . . . . 6
⟂G
⟂G
|
91 | 1, 5, 3, 88, 89, 90 | tglnpt 25444 |
. . . . 5
⟂G
⟂G
|
92 | | simplr 792 |
. . . . . 6
⟂G
⟂G |
93 | 1, 5, 3, 88, 89, 92 | tglnpt 25444 |
. . . . 5
⟂G
⟂G |
94 | 1, 2, 3, 4, 5, 6, 8, 16, 23, 26 | opptgdim2 25637 |
. . . . . 6
DimTarskiG≥ |
95 | 94 | ad4antr 768 |
. . . . 5
⟂G
⟂G DimTarskiG≥ |
96 | 1, 2, 3, 5, 88, 14, 91, 93, 95 | midex 25629 |
. . . 4
⟂G
⟂G
pInvG |
97 | 87, 96 | r19.29a 3078 |
. . 3
⟂G
⟂G |
98 | 1, 2, 3, 4, 5, 6, 8, 16, 23, 26 | oppne2 25634 |
. . . . 5
|
99 | 1, 2, 3, 5, 8, 6, 23, 98 | footex 25613 |
. . . 4
⟂G |
100 | 99 | ad2antrr 762 |
. . 3
⟂G ⟂G |
101 | 97, 100 | r19.29a 3078 |
. 2
⟂G |
102 | 1, 2, 3, 5, 8, 6, 16, 73 | footex 25613 |
. 2
⟂G |
103 | 101, 102 | r19.29a 3078 |
1
|