Step | Hyp | Ref
| Expression |
1 | | isperp.p |
. . . 4
β’ π = (BaseβπΊ) |
2 | | isperp.d |
. . . 4
β’ β =
(distβπΊ) |
3 | | isperp.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
4 | | isperp.l |
. . . 4
β’ πΏ = (LineGβπΊ) |
5 | | eqid 2733 |
. . . 4
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
6 | | isperp.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β πΊ β TarskiG) |
8 | | ragperp.b |
. . . . . 6
β’ (π β π΅ β ran πΏ) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π΅ β ran πΏ) |
10 | | simprr 772 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π£ β π΅) |
11 | 1, 4, 3, 7, 9, 10 | tglnpt 27780 |
. . . 4
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π£ β π) |
12 | | isperp.a |
. . . . . 6
β’ (π β π΄ β ran πΏ) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π΄ β ran πΏ) |
14 | | ragperp.x |
. . . . . . 7
β’ (π β π β (π΄ β© π΅)) |
15 | 14 | elin1d 4197 |
. . . . . 6
β’ (π β π β π΄) |
16 | 15 | adantr 482 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π΄) |
17 | 1, 4, 3, 7, 13, 16 | tglnpt 27780 |
. . . 4
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π) |
18 | | simprl 770 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π’ β π΄) |
19 | 1, 4, 3, 7, 13, 18 | tglnpt 27780 |
. . . 4
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π’ β π) |
20 | | ragperp.v |
. . . . . . 7
β’ (π β π β π΅) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π΅) |
22 | 1, 4, 3, 7, 9, 21 | tglnpt 27780 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π) |
23 | | ragperp.u |
. . . . . . . . 9
β’ (π β π β π΄) |
24 | 23 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π΄) |
25 | 1, 4, 3, 7, 13, 24 | tglnpt 27780 |
. . . . . . 7
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π) |
26 | | ragperp.r |
. . . . . . . 8
β’ (π β β¨βπππββ© β (βGβπΊ)) |
27 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β β¨βπππββ© β (βGβπΊ)) |
28 | | ragperp.1 |
. . . . . . . 8
β’ (π β π β π) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π) |
30 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π β π΄) |
31 | 6 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β πΊ β TarskiG) |
32 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π β π) |
33 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π’ β π) |
34 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β Β¬ π = π’) |
35 | 34 | neqned 2948 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π β π’) |
36 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π΄ β ran πΏ) |
37 | 15 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π β π΄) |
38 | 18 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π’ β π΄) |
39 | 1, 3, 4, 31, 32, 33, 35, 35, 36, 37, 38 | tglinethru 27867 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π΄ = (ππΏπ’)) |
40 | 30, 39 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π’) β π β (ππΏπ’)) |
41 | 40 | ex 414 |
. . . . . . . . 9
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β (Β¬ π = π’ β π β (ππΏπ’))) |
42 | 41 | orrd 862 |
. . . . . . . 8
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β (π = π’ β¨ π β (ππΏπ’))) |
43 | 42 | orcomd 870 |
. . . . . . 7
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β (π β (ππΏπ’) β¨ π = π’)) |
44 | 1, 2, 3, 4, 5, 7, 25, 17, 22, 19, 27, 29, 43 | ragcol 27930 |
. . . . . 6
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β β¨βπ’ππββ© β (βGβπΊ)) |
45 | 1, 2, 3, 4, 5, 7, 19, 17, 22, 44 | ragcom 27929 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β β¨βπππ’ββ© β (βGβπΊ)) |
46 | | ragperp.2 |
. . . . . 6
β’ (π β π β π) |
47 | 46 | adantr 482 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β π β π) |
48 | 20 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π β π΅) |
49 | 6 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β πΊ β TarskiG) |
50 | 17 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π β π) |
51 | 11 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π£ β π) |
52 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β Β¬ π = π£) |
53 | 52 | neqned 2948 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π β π£) |
54 | 8 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π΅ β ran πΏ) |
55 | 14 | elin2d 4198 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π β π΅) |
57 | 10 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π£ β π΅) |
58 | 1, 3, 4, 49, 50, 51, 53, 53, 54, 56, 57 | tglinethru 27867 |
. . . . . . . . 9
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π΅ = (ππΏπ£)) |
59 | 48, 58 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ (π’ β π΄ β§ π£ β π΅)) β§ Β¬ π = π£) β π β (ππΏπ£)) |
60 | 59 | ex 414 |
. . . . . . 7
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β (Β¬ π = π£ β π β (ππΏπ£))) |
61 | 60 | orrd 862 |
. . . . . 6
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β (π = π£ β¨ π β (ππΏπ£))) |
62 | 61 | orcomd 870 |
. . . . 5
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β (π β (ππΏπ£) β¨ π = π£)) |
63 | 1, 2, 3, 4, 5, 7, 22, 17, 19, 11, 45, 47, 62 | ragcol 27930 |
. . . 4
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β β¨βπ£ππ’ββ© β (βGβπΊ)) |
64 | 1, 2, 3, 4, 5, 7, 11, 17, 19, 63 | ragcom 27929 |
. . 3
β’ ((π β§ (π’ β π΄ β§ π£ β π΅)) β β¨βπ’ππ£ββ© β (βGβπΊ)) |
65 | 64 | ralrimivva 3201 |
. 2
β’ (π β βπ’ β π΄ βπ£ β π΅ β¨βπ’ππ£ββ© β (βGβπΊ)) |
66 | 1, 2, 3, 4, 6, 12,
8, 14 | isperp2 27946 |
. 2
β’ (π β (π΄(βGβπΊ)π΅ β βπ’ β π΄ βπ£ β π΅ β¨βπ’ππ£ββ© β (βGβπΊ))) |
67 | 65, 66 | mpbird 257 |
1
β’ (π β π΄(βGβπΊ)π΅) |