Step | Hyp | Ref
| Expression |
1 | | ishlg.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | | eqid 2732 |
. . . . 5
β’
(distβπΊ) =
(distβπΊ) |
3 | | ishlg.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
4 | | hlln.1 |
. . . . . 6
β’ (π β πΊ β TarskiG) |
5 | 4 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ β (πΆπΌπ΅)) β πΊ β TarskiG) |
6 | | ishlg.c |
. . . . . 6
β’ (π β πΆ β π) |
7 | 6 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ β (πΆπΌπ΅)) β πΆ β π) |
8 | | ishlg.a |
. . . . . 6
β’ (π β π΄ β π) |
9 | 8 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ β (πΆπΌπ΅)) β π΄ β π) |
10 | | ishlg.b |
. . . . . 6
β’ (π β π΅ β π) |
11 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ β (πΆπΌπ΅)) β π΅ β π) |
12 | | simpr 485 |
. . . . 5
β’ ((π β§ π΄ β (πΆπΌπ΅)) β π΄ β (πΆπΌπ΅)) |
13 | 1, 2, 3, 5, 7, 9, 11, 12 | tgbtwncom 27728 |
. . . 4
β’ ((π β§ π΄ β (πΆπΌπ΅)) β π΄ β (π΅πΌπΆ)) |
14 | 13 | 3mix1d 1336 |
. . 3
β’ ((π β§ π΄ β (πΆπΌπ΅)) β (π΄ β (π΅πΌπΆ) β¨ π΅ β (π΄πΌπΆ) β¨ πΆ β (π΅πΌπ΄))) |
15 | 4 | adantr 481 |
. . . . 5
β’ ((π β§ π΅ β (πΆπΌπ΄)) β πΊ β TarskiG) |
16 | 6 | adantr 481 |
. . . . 5
β’ ((π β§ π΅ β (πΆπΌπ΄)) β πΆ β π) |
17 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ π΅ β (πΆπΌπ΄)) β π΅ β π) |
18 | 8 | adantr 481 |
. . . . 5
β’ ((π β§ π΅ β (πΆπΌπ΄)) β π΄ β π) |
19 | | simpr 485 |
. . . . 5
β’ ((π β§ π΅ β (πΆπΌπ΄)) β π΅ β (πΆπΌπ΄)) |
20 | 1, 2, 3, 15, 16, 17, 18, 19 | tgbtwncom 27728 |
. . . 4
β’ ((π β§ π΅ β (πΆπΌπ΄)) β π΅ β (π΄πΌπΆ)) |
21 | 20 | 3mix2d 1337 |
. . 3
β’ ((π β§ π΅ β (πΆπΌπ΄)) β (π΄ β (π΅πΌπΆ) β¨ π΅ β (π΄πΌπΆ) β¨ πΆ β (π΅πΌπ΄))) |
22 | | hlln.2 |
. . . . 5
β’ (π β π΄(πΎβπΆ)π΅) |
23 | | ishlg.k |
. . . . . 6
β’ πΎ = (hlGβπΊ) |
24 | 1, 3, 23, 8, 10, 6, 4 | ishlg 27842 |
. . . . 5
β’ (π β (π΄(πΎβπΆ)π΅ β (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄))))) |
25 | 22, 24 | mpbid 231 |
. . . 4
β’ (π β (π΄ β πΆ β§ π΅ β πΆ β§ (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄)))) |
26 | 25 | simp3d 1144 |
. . 3
β’ (π β (π΄ β (πΆπΌπ΅) β¨ π΅ β (πΆπΌπ΄))) |
27 | 14, 21, 26 | mpjaodan 957 |
. 2
β’ (π β (π΄ β (π΅πΌπΆ) β¨ π΅ β (π΄πΌπΆ) β¨ πΆ β (π΅πΌπ΄))) |
28 | | hlln.l |
. . 3
β’ πΏ = (LineGβπΊ) |
29 | 25 | simp2d 1143 |
. . 3
β’ (π β π΅ β πΆ) |
30 | 1, 28, 3, 4, 10, 6,
29, 8 | tgellng 27793 |
. 2
β’ (π β (π΄ β (π΅πΏπΆ) β (π΄ β (π΅πΌπΆ) β¨ π΅ β (π΄πΌπΆ) β¨ πΆ β (π΅πΌπ΄)))) |
31 | 27, 30 | mpbird 256 |
1
β’ (π β π΄ β (π΅πΏπΆ)) |