Description: Identity law for points on lines. Theorem 4.18 of Schwabhauser p. 38. (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 ) |
||
lnid.1 | |- ( ph -> X =/= Y ) |
||
lnid.2 | |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) ) |
||
lnid.3 | |- ( ph -> ( X .- Z ) = ( X .- A ) ) |
||
lnid.4 | |- ( ph -> ( Y .- Z ) = ( Y .- A ) ) |
||
Assertion | lnid | |- ( ph -> Z = A ) |
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 | lnid.1 | |- ( ph -> X =/= Y ) |
|
13 | lnid.2 | |- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) ) |
|
14 | lnid.3 | |- ( ph -> ( X .- Z ) = ( X .- A ) ) |
|
15 | lnid.4 | |- ( ph -> ( Y .- Z ) = ( Y .- A ) ) |
|
16 | 1 2 3 4 5 6 7 8 7 9 11 12 13 14 15 | lncgr | |- ( ph -> ( Z .- Z ) = ( Z .- A ) ) |
17 | 16 | eqcomd | |- ( ph -> ( Z .- A ) = ( Z .- Z ) ) |
18 | 1 11 3 4 7 9 7 17 | axtgcgrid | |- ( ph -> Z = A ) |