Step | Hyp | Ref
| Expression |
1 | | tgcgrextend.4 |
. . . 4
β’ (π β (π΅ β πΆ) = (πΈ β πΉ)) |
2 | 1 | adantr 481 |
. . 3
β’ ((π β§ π΄ = π΅) β (π΅ β πΆ) = (πΈ β πΉ)) |
3 | | simpr 485 |
. . . 4
β’ ((π β§ π΄ = π΅) β π΄ = π΅) |
4 | 3 | oveq1d 7426 |
. . 3
β’ ((π β§ π΄ = π΅) β (π΄ β πΆ) = (π΅ β πΆ)) |
5 | | tkgeom.p |
. . . . 5
β’ π = (BaseβπΊ) |
6 | | tkgeom.d |
. . . . 5
β’ β =
(distβπΊ) |
7 | | tkgeom.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
8 | | tkgeom.g |
. . . . . 6
β’ (π β πΊ β TarskiG) |
9 | 8 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ = π΅) β πΊ β TarskiG) |
10 | | tgcgrextend.a |
. . . . . 6
β’ (π β π΄ β π) |
11 | 10 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ = π΅) β π΄ β π) |
12 | | tgcgrextend.b |
. . . . . 6
β’ (π β π΅ β π) |
13 | 12 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ = π΅) β π΅ β π) |
14 | | tgcgrextend.d |
. . . . . 6
β’ (π β π· β π) |
15 | 14 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ = π΅) β π· β π) |
16 | | tgcgrextend.e |
. . . . . 6
β’ (π β πΈ β π) |
17 | 16 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ = π΅) β πΈ β π) |
18 | | tgcgrextend.3 |
. . . . . 6
β’ (π β (π΄ β π΅) = (π· β πΈ)) |
19 | 18 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ = π΅) β (π΄ β π΅) = (π· β πΈ)) |
20 | 5, 6, 7, 9, 11, 13, 15, 17, 19, 3 | tgcgreq 27771 |
. . . 4
β’ ((π β§ π΄ = π΅) β π· = πΈ) |
21 | 20 | oveq1d 7426 |
. . 3
β’ ((π β§ π΄ = π΅) β (π· β πΉ) = (πΈ β πΉ)) |
22 | 2, 4, 21 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π΄ = π΅) β (π΄ β πΆ) = (π· β πΉ)) |
23 | 8 | adantr 481 |
. . 3
β’ ((π β§ π΄ β π΅) β πΊ β TarskiG) |
24 | | tgcgrextend.c |
. . . 4
β’ (π β πΆ β π) |
25 | 24 | adantr 481 |
. . 3
β’ ((π β§ π΄ β π΅) β πΆ β π) |
26 | 10 | adantr 481 |
. . 3
β’ ((π β§ π΄ β π΅) β π΄ β π) |
27 | | tgcgrextend.f |
. . . 4
β’ (π β πΉ β π) |
28 | 27 | adantr 481 |
. . 3
β’ ((π β§ π΄ β π΅) β πΉ β π) |
29 | 14 | adantr 481 |
. . 3
β’ ((π β§ π΄ β π΅) β π· β π) |
30 | 12 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π΅) β π΅ β π) |
31 | 16 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π΅) β πΈ β π) |
32 | | simpr 485 |
. . . 4
β’ ((π β§ π΄ β π΅) β π΄ β π΅) |
33 | | tgcgrextend.1 |
. . . . 5
β’ (π β π΅ β (π΄πΌπΆ)) |
34 | 33 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π΅) β π΅ β (π΄πΌπΆ)) |
35 | | tgcgrextend.2 |
. . . . 5
β’ (π β πΈ β (π·πΌπΉ)) |
36 | 35 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π΅) β πΈ β (π·πΌπΉ)) |
37 | 18 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π΅) β (π΄ β π΅) = (π· β πΈ)) |
38 | 1 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π΅) β (π΅ β πΆ) = (πΈ β πΉ)) |
39 | 5, 6, 7, 23, 26, 29 | tgcgrtriv 27773 |
. . . 4
β’ ((π β§ π΄ β π΅) β (π΄ β π΄) = (π· β π·)) |
40 | 5, 6, 7, 23, 26, 30, 29, 31, 37 | tgcgrcomlr 27769 |
. . . 4
β’ ((π β§ π΄ β π΅) β (π΅ β π΄) = (πΈ β π·)) |
41 | 5, 6, 7, 23, 26, 30, 25, 29, 31, 28, 26, 29, 32, 34, 36, 37, 38, 39, 40 | axtg5seg 27754 |
. . 3
β’ ((π β§ π΄ β π΅) β (πΆ β π΄) = (πΉ β π·)) |
42 | 5, 6, 7, 23, 25, 26, 28, 29, 41 | tgcgrcomlr 27769 |
. 2
β’ ((π β§ π΄ β π΅) β (π΄ β πΆ) = (π· β πΉ)) |
43 | 22, 42 | pm2.61dane 3029 |
1
β’ (π β (π΄ β πΆ) = (π· β πΉ)) |