Step | Hyp | Ref
| Expression |
1 | | tkgeom.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | tkgeom.d |
. . 3
β’ β =
(distβπΊ) |
3 | | tkgeom.i |
. . 3
β’ πΌ = (ItvβπΊ) |
4 | | tkgeom.g |
. . . 4
β’ (π β πΊ β TarskiG) |
5 | 4 | adantr 481 |
. . 3
β’ ((π β§ π΄ = π΅) β πΊ β TarskiG) |
6 | | tgcgrcomlr.c |
. . . 4
β’ (π β πΆ β π) |
7 | 6 | adantr 481 |
. . 3
β’ ((π β§ π΄ = π΅) β πΆ β π) |
8 | | tgcgrcomlr.d |
. . . 4
β’ (π β π· β π) |
9 | 8 | adantr 481 |
. . 3
β’ ((π β§ π΄ = π΅) β π· β π) |
10 | | tgcgrcomlr.b |
. . . 4
β’ (π β π΅ β π) |
11 | 10 | adantr 481 |
. . 3
β’ ((π β§ π΄ = π΅) β π΅ β π) |
12 | | tgcgrcomlr.6 |
. . . . 5
β’ (π β (π΄ β π΅) = (πΆ β π·)) |
13 | 12 | adantr 481 |
. . . 4
β’ ((π β§ π΄ = π΅) β (π΄ β π΅) = (πΆ β π·)) |
14 | | simpr 485 |
. . . . 5
β’ ((π β§ π΄ = π΅) β π΄ = π΅) |
15 | 14 | oveq1d 7426 |
. . . 4
β’ ((π β§ π΄ = π΅) β (π΄ β π΅) = (π΅ β π΅)) |
16 | 13, 15 | eqtr3d 2774 |
. . 3
β’ ((π β§ π΄ = π΅) β (πΆ β π·) = (π΅ β π΅)) |
17 | 1, 2, 3, 5, 7, 9, 11, 16 | axtgcgrid 27969 |
. 2
β’ ((π β§ π΄ = π΅) β πΆ = π·) |
18 | 4 | adantr 481 |
. . 3
β’ ((π β§ πΆ = π·) β πΊ β TarskiG) |
19 | | tgcgrcomlr.a |
. . . 4
β’ (π β π΄ β π) |
20 | 19 | adantr 481 |
. . 3
β’ ((π β§ πΆ = π·) β π΄ β π) |
21 | 10 | adantr 481 |
. . 3
β’ ((π β§ πΆ = π·) β π΅ β π) |
22 | 8 | adantr 481 |
. . 3
β’ ((π β§ πΆ = π·) β π· β π) |
23 | 12 | adantr 481 |
. . . 4
β’ ((π β§ πΆ = π·) β (π΄ β π΅) = (πΆ β π·)) |
24 | | simpr 485 |
. . . . 5
β’ ((π β§ πΆ = π·) β πΆ = π·) |
25 | 24 | oveq1d 7426 |
. . . 4
β’ ((π β§ πΆ = π·) β (πΆ β π·) = (π· β π·)) |
26 | 23, 25 | eqtrd 2772 |
. . 3
β’ ((π β§ πΆ = π·) β (π΄ β π΅) = (π· β π·)) |
27 | 1, 2, 3, 18, 20, 21, 22, 26 | axtgcgrid 27969 |
. 2
β’ ((π β§ πΆ = π·) β π΄ = π΅) |
28 | 17, 27 | impbida 799 |
1
β’ (π β (π΄ = π΅ β πΆ = π·)) |