Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ ((π β§ πΆ = π΅) β πΆ = π΅) |
2 | | ishlg.p |
. . . . . 6
β’ π = (BaseβπΊ) |
3 | | eqid 2733 |
. . . . . 6
β’
(distβπΊ) =
(distβπΊ) |
4 | | ishlg.i |
. . . . . 6
β’ πΌ = (ItvβπΊ) |
5 | | hlln.1 |
. . . . . 6
β’ (π β πΊ β TarskiG) |
6 | | ishlg.a |
. . . . . 6
β’ (π β π΄ β π) |
7 | | ishlg.c |
. . . . . 6
β’ (π β πΆ β π) |
8 | 2, 3, 4, 5, 6, 7 | tgbtwntriv2 27738 |
. . . . 5
β’ (π β πΆ β (π΄πΌπΆ)) |
9 | 8 | adantr 482 |
. . . 4
β’ ((π β§ πΆ = π΅) β πΆ β (π΄πΌπΆ)) |
10 | 1, 9 | eqeltrrd 2835 |
. . 3
β’ ((π β§ πΆ = π΅) β π΅ β (π΄πΌπΆ)) |
11 | 10 | olcd 873 |
. 2
β’ ((π β§ πΆ = π΅) β (πΆ(πΎβπ΅)π΄ β¨ π΅ β (π΄πΌπΆ))) |
12 | | lnhl.1 |
. . . . . 6
β’ (π β πΆ β (π΄πΏπ΅)) |
13 | | lnhl.l |
. . . . . . 7
β’ πΏ = (LineGβπΊ) |
14 | | ishlg.b |
. . . . . . 7
β’ (π β π΅ β π) |
15 | 2, 13, 4, 5, 6, 14,
12 | tglngne 27801 |
. . . . . . 7
β’ (π β π΄ β π΅) |
16 | 2, 13, 4, 5, 6, 14,
15, 7 | tgellng 27804 |
. . . . . 6
β’ (π β (πΆ β (π΄πΏπ΅) β (πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅) β¨ π΅ β (π΄πΌπΆ)))) |
17 | 12, 16 | mpbid 231 |
. . . . 5
β’ (π β (πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅) β¨ π΅ β (π΄πΌπΆ))) |
18 | | df-3or 1089 |
. . . . 5
β’ ((πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅) β¨ π΅ β (π΄πΌπΆ)) β ((πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅)) β¨ π΅ β (π΄πΌπΆ))) |
19 | 17, 18 | sylib 217 |
. . . 4
β’ (π β ((πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅)) β¨ π΅ β (π΄πΌπΆ))) |
20 | 19 | adantr 482 |
. . 3
β’ ((π β§ πΆ β π΅) β ((πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅)) β¨ π΅ β (π΄πΌπΆ))) |
21 | | ishlg.k |
. . . . . . . 8
β’ πΎ = (hlGβπΊ) |
22 | 2, 4, 21, 7, 6, 14, 5 | ishlg 27853 |
. . . . . . 7
β’ (π β (πΆ(πΎβπ΅)π΄ β (πΆ β π΅ β§ π΄ β π΅ β§ (πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ))))) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ πΆ β π΅) β (πΆ(πΎβπ΅)π΄ β (πΆ β π΅ β§ π΄ β π΅ β§ (πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ))))) |
24 | | df-3an 1090 |
. . . . . 6
β’ ((πΆ β π΅ β§ π΄ β π΅ β§ (πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ))) β ((πΆ β π΅ β§ π΄ β π΅) β§ (πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ)))) |
25 | 23, 24 | bitrdi 287 |
. . . . 5
β’ ((π β§ πΆ β π΅) β (πΆ(πΎβπ΅)π΄ β ((πΆ β π΅ β§ π΄ β π΅) β§ (πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ))))) |
26 | 15 | anim1ci 617 |
. . . . . 6
β’ ((π β§ πΆ β π΅) β (πΆ β π΅ β§ π΄ β π΅)) |
27 | 26 | biantrurd 534 |
. . . . 5
β’ ((π β§ πΆ β π΅) β ((πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ)) β ((πΆ β π΅ β§ π΄ β π΅) β§ (πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ))))) |
28 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ β π΅) β πΊ β TarskiG) |
29 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ β π΅) β π΅ β π) |
30 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ β π΅) β πΆ β π) |
31 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ β π΅) β π΄ β π) |
32 | 2, 3, 4, 28, 29, 30, 31 | tgbtwncomb 27740 |
. . . . . 6
β’ ((π β§ πΆ β π΅) β (πΆ β (π΅πΌπ΄) β πΆ β (π΄πΌπ΅))) |
33 | 2, 3, 4, 28, 29, 31, 30 | tgbtwncomb 27740 |
. . . . . 6
β’ ((π β§ πΆ β π΅) β (π΄ β (π΅πΌπΆ) β π΄ β (πΆπΌπ΅))) |
34 | 32, 33 | orbi12d 918 |
. . . . 5
β’ ((π β§ πΆ β π΅) β ((πΆ β (π΅πΌπ΄) β¨ π΄ β (π΅πΌπΆ)) β (πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅)))) |
35 | 25, 27, 34 | 3bitr2d 307 |
. . . 4
β’ ((π β§ πΆ β π΅) β (πΆ(πΎβπ΅)π΄ β (πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅)))) |
36 | 35 | orbi1d 916 |
. . 3
β’ ((π β§ πΆ β π΅) β ((πΆ(πΎβπ΅)π΄ β¨ π΅ β (π΄πΌπΆ)) β ((πΆ β (π΄πΌπ΅) β¨ π΄ β (πΆπΌπ΅)) β¨ π΅ β (π΄πΌπΆ)))) |
37 | 20, 36 | mpbird 257 |
. 2
β’ ((π β§ πΆ β π΅) β (πΆ(πΎβπ΅)π΄ β¨ π΅ β (π΄πΌπΆ))) |
38 | 11, 37 | pm2.61dane 3030 |
1
β’ (π β (πΆ(πΎβπ΅)π΄ β¨ π΅ β (π΄πΌπΆ))) |