Step |
Hyp |
Ref |
Expression |
1 |
|
tg5segofs.p |
|- P = ( Base ` G ) |
2 |
|
tg5segofs.m |
|- .- = ( dist ` G ) |
3 |
|
tg5segofs.s |
|- I = ( Itv ` G ) |
4 |
|
tg5segofs.g |
|- ( ph -> G e. TarskiG ) |
5 |
|
tg5segofs.a |
|- ( ph -> A e. P ) |
6 |
|
tg5segofs.b |
|- ( ph -> B e. P ) |
7 |
|
tg5segofs.c |
|- ( ph -> C e. P ) |
8 |
|
tg5segofs.d |
|- ( ph -> D e. P ) |
9 |
|
tg5segofs.e |
|- ( ph -> E e. P ) |
10 |
|
tg5segofs.f |
|- ( ph -> F e. P ) |
11 |
|
tg5segofs.o |
|- O = ( AFS ` G ) |
12 |
|
tg5segofs.h |
|- ( ph -> H e. P ) |
13 |
|
tg5segofs.i |
|- ( ph -> I e. P ) |
14 |
|
tg5segofs.1 |
|- ( ph -> <. <. A , B >. , <. C , D >. >. O <. <. E , F >. , <. H , I >. >. ) |
15 |
|
tg5segofs.2 |
|- ( ph -> A =/= B ) |
16 |
1 2 3 4 11 5 6 7 8 9 10 12 13
|
brafs |
|- ( ph -> ( <. <. A , B >. , <. C , D >. >. O <. <. E , F >. , <. H , I >. >. <-> ( ( B e. ( A I C ) /\ F e. ( E I H ) ) /\ ( ( A .- B ) = ( E .- F ) /\ ( B .- C ) = ( F .- H ) ) /\ ( ( A .- D ) = ( E .- I ) /\ ( B .- D ) = ( F .- I ) ) ) ) ) |
17 |
14 16
|
mpbid |
|- ( ph -> ( ( B e. ( A I C ) /\ F e. ( E I H ) ) /\ ( ( A .- B ) = ( E .- F ) /\ ( B .- C ) = ( F .- H ) ) /\ ( ( A .- D ) = ( E .- I ) /\ ( B .- D ) = ( F .- I ) ) ) ) |
18 |
17
|
simp1d |
|- ( ph -> ( B e. ( A I C ) /\ F e. ( E I H ) ) ) |
19 |
18
|
simpld |
|- ( ph -> B e. ( A I C ) ) |
20 |
18
|
simprd |
|- ( ph -> F e. ( E I H ) ) |
21 |
17
|
simp2d |
|- ( ph -> ( ( A .- B ) = ( E .- F ) /\ ( B .- C ) = ( F .- H ) ) ) |
22 |
21
|
simpld |
|- ( ph -> ( A .- B ) = ( E .- F ) ) |
23 |
21
|
simprd |
|- ( ph -> ( B .- C ) = ( F .- H ) ) |
24 |
17
|
simp3d |
|- ( ph -> ( ( A .- D ) = ( E .- I ) /\ ( B .- D ) = ( F .- I ) ) ) |
25 |
24
|
simpld |
|- ( ph -> ( A .- D ) = ( E .- I ) ) |
26 |
24
|
simprd |
|- ( ph -> ( B .- D ) = ( F .- I ) ) |
27 |
1 2 3 4 5 6 7 9 10 12 8 13 15 19 20 22 23 25 26
|
axtg5seg |
|- ( ph -> ( C .- D ) = ( H .- I ) ) |