Step |
Hyp |
Ref |
Expression |
1 |
|
isoas.p |
|- P = ( Base ` G ) |
2 |
|
isoas.m |
|- .- = ( dist ` G ) |
3 |
|
isoas.i |
|- I = ( Itv ` G ) |
4 |
|
isoas.l |
|- L = ( LineG ` G ) |
5 |
|
isoas.g |
|- ( ph -> G e. TarskiG ) |
6 |
|
isoas.a |
|- ( ph -> A e. P ) |
7 |
|
isoas.b |
|- ( ph -> B e. P ) |
8 |
|
isoas.c |
|- ( ph -> C e. P ) |
9 |
|
isoas.1 |
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) ) |
10 |
|
isoas.2 |
|- ( ph -> <" A B C "> ( cgrA ` G ) <" A C B "> ) |
11 |
|
eqid |
|- ( cgrG ` G ) = ( cgrG ` G ) |
12 |
1 4 3 5 6 7 8 9
|
ncolrot1 |
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) ) |
13 |
1 2 3 5 7 8
|
axtgcgrrflx |
|- ( ph -> ( B .- C ) = ( C .- B ) ) |
14 |
|
eqid |
|- ( hlG ` G ) = ( hlG ` G ) |
15 |
1 3 5 14 6 7 8 6 8 7 10
|
cgracom |
|- ( ph -> <" A C B "> ( cgrA ` G ) <" A B C "> ) |
16 |
1 3 2 5 6 8 7 6 7 8 15
|
cgraswaplr |
|- ( ph -> <" B C A "> ( cgrA ` G ) <" C B A "> ) |
17 |
1 2 3 5 7 8 6 8 7 6 4 12 13 16 10
|
tgasa |
|- ( ph -> <" B C A "> ( cgrG ` G ) <" C B A "> ) |
18 |
1 2 3 11 5 7 8 6 8 7 6 17
|
cgr3simp3 |
|- ( ph -> ( A .- B ) = ( A .- C ) ) |