Step | Hyp | Ref
| Expression |
1 | | ishlg.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | ishlg.i |
. . 3
β’ πΌ = (ItvβπΊ) |
3 | | ishlg.k |
. . 3
β’ πΎ = (hlGβπΊ) |
4 | | ishlg.a |
. . 3
β’ (π β π΄ β π) |
5 | | ishlg.b |
. . 3
β’ (π β π΅ β π) |
6 | | ishlg.c |
. . 3
β’ (π β πΆ β π) |
7 | | hlln.1 |
. . 3
β’ (π β πΊ β TarskiG) |
8 | | hltr.d |
. . 3
β’ (π β π· β π) |
9 | | hlcgrex.m |
. . 3
β’ β =
(distβπΊ) |
10 | | hlcgrex.1 |
. . 3
β’ (π β π· β π΄) |
11 | | hlcgrex.2 |
. . 3
β’ (π β π΅ β πΆ) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | hlcgrex 27600 |
. 2
β’ (π β βπ₯ β π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ))) |
13 | 4 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π΄ β π) |
14 | 5 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π΅ β π) |
15 | 6 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β πΆ β π) |
16 | 7 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β πΊ β TarskiG) |
17 | 8 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π· β π) |
18 | 10 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π· β π΄) |
19 | 11 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π΅ β πΆ) |
20 | | simpllr 775 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π₯ β π) |
21 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π¦ β π) |
22 | | simprll 778 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π₯(πΎβπ΄)π·) |
23 | | simprrl 780 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π¦(πΎβπ΄)π·) |
24 | | simprlr 779 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β (π΄ β π₯) = (π΅ β πΆ)) |
25 | | simprrr 781 |
. . . . . 6
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β (π΄ β π¦) = (π΅ β πΆ)) |
26 | 1, 2, 3, 13, 14, 15, 16, 17, 9, 18, 19, 20, 21, 22, 23, 24, 25 | hlcgreulem 27601 |
. . . . 5
β’ ((((π β§ π₯ β π) β§ π¦ β π) β§ ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) β π₯ = π¦) |
27 | 26 | ex 414 |
. . . 4
β’ (((π β§ π₯ β π) β§ π¦ β π) β (((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ))) β π₯ = π¦)) |
28 | 27 | ralrimiva 3140 |
. . 3
β’ ((π β§ π₯ β π) β βπ¦ β π (((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ))) β π₯ = π¦)) |
29 | 28 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β π βπ¦ β π (((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ))) β π₯ = π¦)) |
30 | | breq1 5109 |
. . . 4
β’ (π₯ = π¦ β (π₯(πΎβπ΄)π· β π¦(πΎβπ΄)π·)) |
31 | | oveq2 7366 |
. . . . 5
β’ (π₯ = π¦ β (π΄ β π₯) = (π΄ β π¦)) |
32 | 31 | eqeq1d 2735 |
. . . 4
β’ (π₯ = π¦ β ((π΄ β π₯) = (π΅ β πΆ) β (π΄ β π¦) = (π΅ β πΆ))) |
33 | 30, 32 | anbi12d 632 |
. . 3
β’ (π₯ = π¦ β ((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ)))) |
34 | 33 | reu4 3690 |
. 2
β’
(β!π₯ β
π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β (βπ₯ β π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ βπ₯ β π βπ¦ β π (((π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ)) β§ (π¦(πΎβπ΄)π· β§ (π΄ β π¦) = (π΅ β πΆ))) β π₯ = π¦))) |
35 | 12, 29, 34 | sylanbrc 584 |
1
β’ (π β β!π₯ β π (π₯(πΎβπ΄)π· β§ (π΄ β π₯) = (π΅ β πΆ))) |