Description: Reflexivity law for three-place congruence. (Contributed by Thierry Arnoux, 28-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tgcgrxfr.p | |- P = ( Base ` G ) |
|
tgcgrxfr.m | |- .- = ( dist ` G ) |
||
tgcgrxfr.i | |- I = ( Itv ` G ) |
||
tgcgrxfr.r | |- .~ = ( cgrG ` G ) |
||
tgcgrxfr.g | |- ( ph -> G e. TarskiG ) |
||
tgbtwnxfr.a | |- ( ph -> A e. P ) |
||
tgbtwnxfr.b | |- ( ph -> B e. P ) |
||
tgbtwnxfr.c | |- ( ph -> C e. P ) |
||
Assertion | cgr3id | |- ( ph -> <" A B C "> .~ <" A B C "> ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgcgrxfr.p | |- P = ( Base ` G ) |
|
2 | tgcgrxfr.m | |- .- = ( dist ` G ) |
|
3 | tgcgrxfr.i | |- I = ( Itv ` G ) |
|
4 | tgcgrxfr.r | |- .~ = ( cgrG ` G ) |
|
5 | tgcgrxfr.g | |- ( ph -> G e. TarskiG ) |
|
6 | tgbtwnxfr.a | |- ( ph -> A e. P ) |
|
7 | tgbtwnxfr.b | |- ( ph -> B e. P ) |
|
8 | tgbtwnxfr.c | |- ( ph -> C e. P ) |
|
9 | eqidd | |- ( ph -> ( A .- B ) = ( A .- B ) ) |
|
10 | eqidd | |- ( ph -> ( B .- C ) = ( B .- C ) ) |
|
11 | eqidd | |- ( ph -> ( C .- A ) = ( C .- A ) ) |
|
12 | 1 2 4 5 6 7 8 6 7 8 9 10 11 | trgcgr | |- ( ph -> <" A B C "> .~ <" A B C "> ) |