![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-trkgc | Structured version Visualization version Unicode version |
Description: Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2480, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.) |
Ref | Expression |
---|---|
df-trkgc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cstrkgc 24527 |
. 2
![]() | |
2 | vx |
. . . . . . . . . . 11
![]() ![]() | |
3 | 2 | cv 1453 |
. . . . . . . . . 10
![]() ![]() |
4 | vy |
. . . . . . . . . . 11
![]() ![]() | |
5 | 4 | cv 1453 |
. . . . . . . . . 10
![]() ![]() |
6 | vd |
. . . . . . . . . . 11
![]() ![]() | |
7 | 6 | cv 1453 |
. . . . . . . . . 10
![]() ![]() |
8 | 3, 5, 7 | co 6314 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 3, 7 | co 6314 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 8, 9 | wceq 1454 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | vp |
. . . . . . . . 9
![]() ![]() | |
12 | 11 | cv 1453 |
. . . . . . . 8
![]() ![]() |
13 | 10, 4, 12 | wral 2748 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13, 2, 12 | wral 2748 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | vz |
. . . . . . . . . . . . 13
![]() ![]() | |
16 | 15 | cv 1453 |
. . . . . . . . . . . 12
![]() ![]() |
17 | 16, 16, 7 | co 6314 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() |
18 | 8, 17 | wceq 1454 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 2, 4 | weq 1801 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() |
20 | 18, 19 | wi 4 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 20, 15, 12 | wral 2748 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | 21, 4, 12 | wral 2748 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
23 | 22, 2, 12 | wral 2748 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 14, 23 | wa 375 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | vf |
. . . . . . 7
![]() ![]() | |
26 | 25 | cv 1453 |
. . . . . 6
![]() ![]() |
27 | cds 15247 |
. . . . . 6
![]() ![]() | |
28 | 26, 27 | cfv 5600 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
29 | 24, 6, 28 | wsbc 3278 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | cbs 15169 |
. . . . 5
![]() ![]() | |
31 | 26, 30 | cfv 5600 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
32 | 29, 11, 31 | wsbc 3278 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32, 25 | cab 2447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 1, 33 | wceq 1454 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: istrkgc 24550 |
Copyright terms: Public domain | W3C validator |