Step | Hyp | Ref
| Expression |
1 | | ishlg.p |
. . . 4
β’ π = (BaseβπΊ) |
2 | | hlcgrex.m |
. . . 4
β’ β =
(distβπΊ) |
3 | | ishlg.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
4 | | hlln.1 |
. . . . 5
β’ (π β πΊ β TarskiG) |
5 | 4 | ad2antrr 724 |
. . . 4
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β πΊ β TarskiG) |
6 | | simplr 767 |
. . . 4
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β π¦ β π) |
7 | | ishlg.a |
. . . . 5
β’ (π β π΄ β π) |
8 | 7 | ad2antrr 724 |
. . . 4
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β π΄ β π) |
9 | | ishlg.b |
. . . . 5
β’ (π β π΅ β π) |
10 | 9 | ad2antrr 724 |
. . . 4
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β π΅ β π) |
11 | | ishlg.c |
. . . . 5
β’ (π β πΆ β π) |
12 | 11 | ad2antrr 724 |
. . . 4
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β πΆ β π) |
13 | 1, 2, 3, 5, 6, 8, 10, 12 | axtgsegcon 26870 |
. . 3
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β βπ₯ β π (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) |
14 | 5 | ad2antrr 724 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β πΊ β TarskiG) |
15 | 10 | ad2antrr 724 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΅ β π) |
16 | 12 | ad2antrr 724 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β πΆ β π) |
17 | | simplr 767 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π₯ β π) |
18 | 8 | ad2antrr 724 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΄ β π) |
19 | | simprr 771 |
. . . . . . . . . 10
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π΄ β π₯) = (π΅ β πΆ)) |
20 | 1, 2, 3, 14, 18, 17, 15, 16, 19 | tgcgrcoml 26885 |
. . . . . . . . 9
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π₯ β π΄) = (π΅ β πΆ)) |
21 | 20 | eqcomd 2742 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π΅ β πΆ) = (π₯ β π΄)) |
22 | | hlcgrex.2 |
. . . . . . . . 9
β’ (π β π΅ β πΆ) |
23 | 22 | ad4antr 730 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΅ β πΆ) |
24 | 1, 2, 3, 14, 15, 16, 17, 18, 21, 23 | tgcgrneq 26889 |
. . . . . . 7
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π₯ β π΄) |
25 | | hlcgrex.1 |
. . . . . . . 8
β’ (π β π· β π΄) |
26 | 25 | ad4antr 730 |
. . . . . . 7
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π· β π΄) |
27 | 6 | ad2antrr 724 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π¦ β π) |
28 | | hltr.d |
. . . . . . . . 9
β’ (π β π· β π) |
29 | 28 | ad4antr 730 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π· β π) |
30 | | simpllr 774 |
. . . . . . . . . 10
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) |
31 | 30 | simprd 497 |
. . . . . . . . 9
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΄ β π¦) |
32 | 31 | necomd 2997 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π¦ β π΄) |
33 | | simprl 769 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΄ β (π¦πΌπ₯)) |
34 | 30 | simpld 496 |
. . . . . . . . 9
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΄ β (π·πΌπ¦)) |
35 | 1, 2, 3, 14, 29, 18, 27, 34 | tgbtwncom 26894 |
. . . . . . . 8
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π΄ β (π¦πΌπ·)) |
36 | 1, 3, 14, 27, 18, 17, 29, 32, 33, 35 | tgbtwnconn2 26982 |
. . . . . . 7
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π₯ β (π΄πΌπ·) β¨ π· β (π΄πΌπ₯))) |
37 | | ishlg.k |
. . . . . . . 8
β’ πΎ = (hlGβπΊ) |
38 | 1, 3, 37, 17, 29, 18, 14 | ishlg 27008 |
. . . . . . 7
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π₯(πΎβπ΄)π· β (π₯ β π΄ β§ π· β π΄ β§ (π₯ β (π΄πΌπ·) β¨ π· β (π΄πΌπ₯))))) |
39 | 24, 26, 36, 38 | mpbir3and 1342 |
. . . . . 6
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β π₯(πΎβπ΄)π·) |
40 | 39, 19 | jca 513 |
. . . . 5
β’
(((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β§ (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ))) β (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ))) |
41 | 40 | ex 414 |
. . . 4
β’ ((((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β§ π₯ β π) β ((π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ)) β (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)))) |
42 | 41 | reximdva 3162 |
. . 3
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β (βπ₯ β π (π΄ β (π¦πΌπ₯) β§ (π΄ β π₯) = (π΅ β πΆ)) β βπ₯ β π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)))) |
43 | 13, 42 | mpd 15 |
. 2
β’ (((π β§ π¦ β π) β§ (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) β βπ₯ β π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ))) |
44 | 1 | fvexi 6818 |
. . . . 5
β’ π β V |
45 | 44 | a1i 11 |
. . . 4
β’ (π β π β V) |
46 | 45, 9, 11, 22 | nehash2 14233 |
. . 3
β’ (π β 2 β€
(β―βπ)) |
47 | 1, 2, 3, 4, 28, 7,
46 | tgbtwndiff 26912 |
. 2
β’ (π β βπ¦ β π (π΄ β (π·πΌπ¦) β§ π΄ β π¦)) |
48 | 43, 47 | r19.29a 3156 |
1
β’ (π β βπ₯ β π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ))) |