Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 28-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tglngval.p | |- P = ( Base ` G ) |
|
tglngval.l | |- L = ( LineG ` G ) |
||
tglngval.i | |- I = ( Itv ` G ) |
||
tglngval.g | |- ( ph -> G e. TarskiG ) |
||
tglngval.x | |- ( ph -> X e. P ) |
||
tglngval.y | |- ( ph -> Y e. P ) |
||
tgcolg.z | |- ( ph -> Z e. P ) |
||
lnxfr.r | |- .~ = ( cgrG ` G ) |
||
lnxfr.a | |- ( ph -> A e. P ) |
||
lnxfr.b | |- ( ph -> B e. P ) |
||
lnxfr.d | |- .- = ( dist ` G ) |
||
lncgr.1 | |- ( ph -> X =/= Y ) |
||
lncgr.2 | |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) ) |
||
lncgr.3 | |- ( ph -> ( X .- A ) = ( X .- B ) ) |
||
lncgr.4 | |- ( ph -> ( Y .- A ) = ( Y .- B ) ) |
||
Assertion | lncgr | |- ( ph -> ( Z .- A ) = ( Z .- B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglngval.p | |- P = ( Base ` G ) |
|
2 | tglngval.l | |- L = ( LineG ` G ) |
|
3 | tglngval.i | |- I = ( Itv ` G ) |
|
4 | tglngval.g | |- ( ph -> G e. TarskiG ) |
|
5 | tglngval.x | |- ( ph -> X e. P ) |
|
6 | tglngval.y | |- ( ph -> Y e. P ) |
|
7 | tgcolg.z | |- ( ph -> Z e. P ) |
|
8 | lnxfr.r | |- .~ = ( cgrG ` G ) |
|
9 | lnxfr.a | |- ( ph -> A e. P ) |
|
10 | lnxfr.b | |- ( ph -> B e. P ) |
|
11 | lnxfr.d | |- .- = ( dist ` G ) |
|
12 | lncgr.1 | |- ( ph -> X =/= Y ) |
|
13 | lncgr.2 | |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) ) |
|
14 | lncgr.3 | |- ( ph -> ( X .- A ) = ( X .- B ) ) |
|
15 | lncgr.4 | |- ( ph -> ( Y .- A ) = ( Y .- B ) ) |
|
16 | 1 11 3 8 4 5 6 7 | cgr3id | |- ( ph -> <" X Y Z "> .~ <" X Y Z "> ) |
17 | 1 2 3 4 5 6 7 8 5 6 11 9 7 10 13 16 14 15 12 | tgfscgr | |- ( ph -> ( Z .- A ) = ( Z .- B ) ) |