Step |
Hyp |
Ref |
Expression |
1 |
|
cgracol.p |
|- P = ( Base ` G ) |
2 |
|
cgracol.i |
|- I = ( Itv ` G ) |
3 |
|
cgracol.m |
|- .- = ( dist ` G ) |
4 |
|
cgracol.g |
|- ( ph -> G e. TarskiG ) |
5 |
|
cgracol.a |
|- ( ph -> A e. P ) |
6 |
|
cgracol.b |
|- ( ph -> B e. P ) |
7 |
|
cgracol.c |
|- ( ph -> C e. P ) |
8 |
|
cgracol.d |
|- ( ph -> D e. P ) |
9 |
|
cgracol.e |
|- ( ph -> E e. P ) |
10 |
|
cgracol.f |
|- ( ph -> F e. P ) |
11 |
|
flatcgra.1 |
|- ( ph -> B e. ( A I C ) ) |
12 |
|
flatcgra.2 |
|- ( ph -> E e. ( D I F ) ) |
13 |
|
flatcgra.3 |
|- ( ph -> A =/= B ) |
14 |
|
flatcgra.4 |
|- ( ph -> C =/= B ) |
15 |
|
flatcgra.5 |
|- ( ph -> D =/= E ) |
16 |
|
flatcgra.6 |
|- ( ph -> F =/= E ) |
17 |
|
eqid |
|- ( cgrG ` G ) = ( cgrG ` G ) |
18 |
4
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> G e. TarskiG ) |
19 |
5
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> A e. P ) |
20 |
6
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B e. P ) |
21 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> C e. P ) |
22 |
|
simpllr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> x e. P ) |
23 |
9
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. P ) |
24 |
|
simplr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> y e. P ) |
25 |
|
simprlr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( E .- x ) = ( B .- A ) ) |
26 |
1 3 2 18 23 22 20 19 25
|
tgcgrcomlr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x .- E ) = ( A .- B ) ) |
27 |
26
|
eqcomd |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A .- B ) = ( x .- E ) ) |
28 |
|
simprrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( E .- y ) = ( B .- C ) ) |
29 |
28
|
eqcomd |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( B .- C ) = ( E .- y ) ) |
30 |
10
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> F e. P ) |
31 |
8
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> D e. P ) |
32 |
16
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> F =/= E ) |
33 |
15
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> D =/= E ) |
34 |
1 3 2 4 8 9 10 12
|
tgbtwncom |
|- ( ph -> E e. ( F I D ) ) |
35 |
34
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( F I D ) ) |
36 |
|
simprll |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( F I x ) ) |
37 |
|
simprrl |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( D I y ) ) |
38 |
1 2 18 30 23 31 22 24 32 33 35 36 37
|
tgbtwnconn22 |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( x I y ) ) |
39 |
11
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B e. ( A I C ) ) |
40 |
1 3 2 18 22 23 24 19 20 21 38 39 26 28
|
tgcgrextend |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x .- y ) = ( A .- C ) ) |
41 |
40
|
eqcomd |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( A .- C ) = ( x .- y ) ) |
42 |
1 3 2 18 19 21 22 24 41
|
tgcgrcomlr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( C .- A ) = ( y .- x ) ) |
43 |
1 3 17 18 19 20 21 22 23 24 27 29 42
|
trgcgr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> ) |
44 |
25
|
eqcomd |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( B .- A ) = ( E .- x ) ) |
45 |
13
|
necomd |
|- ( ph -> B =/= A ) |
46 |
45
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B =/= A ) |
47 |
1 3 2 18 20 19 23 22 44 46
|
tgcgrneq |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E =/= x ) |
48 |
47
|
necomd |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> x =/= E ) |
49 |
1 2 18 30 23 22 31 32 36 35
|
tgbtwnconn2 |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x e. ( E I D ) \/ D e. ( E I x ) ) ) |
50 |
48 33 49
|
3jca |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x =/= E /\ D =/= E /\ ( x e. ( E I D ) \/ D e. ( E I x ) ) ) ) |
51 |
|
eqid |
|- ( hlG ` G ) = ( hlG ` G ) |
52 |
1 2 51 22 31 23 18
|
ishlg |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( x ( ( hlG ` G ) ` E ) D <-> ( x =/= E /\ D =/= E /\ ( x e. ( E I D ) \/ D e. ( E I x ) ) ) ) ) |
53 |
50 52
|
mpbird |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> x ( ( hlG ` G ) ` E ) D ) |
54 |
14
|
necomd |
|- ( ph -> B =/= C ) |
55 |
54
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> B =/= C ) |
56 |
1 3 2 18 20 21 23 24 29 55
|
tgcgrneq |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E =/= y ) |
57 |
56
|
necomd |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> y =/= E ) |
58 |
12
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> E e. ( D I F ) ) |
59 |
1 2 18 31 23 24 30 33 37 58
|
tgbtwnconn2 |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y e. ( E I F ) \/ F e. ( E I y ) ) ) |
60 |
57 32 59
|
3jca |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y =/= E /\ F =/= E /\ ( y e. ( E I F ) \/ F e. ( E I y ) ) ) ) |
61 |
1 2 51 24 30 23 18
|
ishlg |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( y ( ( hlG ` G ) ` E ) F <-> ( y =/= E /\ F =/= E /\ ( y e. ( E I F ) \/ F e. ( E I y ) ) ) ) ) |
62 |
60 61
|
mpbird |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> y ( ( hlG ` G ) ` E ) F ) |
63 |
43 53 62
|
3jca |
|- ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) -> ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) |
64 |
1 3 2 4 10 9 6 5
|
axtgsegcon |
|- ( ph -> E. x e. P ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) ) |
65 |
1 3 2 4 8 9 6 7
|
axtgsegcon |
|- ( ph -> E. y e. P ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) |
66 |
|
reeanv |
|- ( E. x e. P E. y e. P ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) <-> ( E. x e. P ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ E. y e. P ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) |
67 |
64 65 66
|
sylanbrc |
|- ( ph -> E. x e. P E. y e. P ( ( E e. ( F I x ) /\ ( E .- x ) = ( B .- A ) ) /\ ( E e. ( D I y ) /\ ( E .- y ) = ( B .- C ) ) ) ) |
68 |
63 67
|
reximddv2 |
|- ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) |
69 |
1 2 51 4 5 6 7 8 9 10
|
iscgra |
|- ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( ( hlG ` G ) ` E ) D /\ y ( ( hlG ` G ) ` E ) F ) ) ) |
70 |
68 69
|
mpbird |
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> ) |