Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tkgeom.p | |- P = ( Base ` G ) |
|
tkgeom.d | |- .- = ( dist ` G ) |
||
tkgeom.i | |- I = ( Itv ` G ) |
||
tkgeom.g | |- ( ph -> G e. TarskiG ) |
||
tgbtwnintr.1 | |- ( ph -> A e. P ) |
||
tgbtwnintr.2 | |- ( ph -> B e. P ) |
||
tgbtwnintr.3 | |- ( ph -> C e. P ) |
||
tgbtwnintr.4 | |- ( ph -> D e. P ) |
||
tgbtwnexch3.5 | |- ( ph -> B e. ( A I C ) ) |
||
tgbtwnexch3.6 | |- ( ph -> C e. ( A I D ) ) |
||
Assertion | tgbtwnexch3 | |- ( ph -> C e. ( B I D ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tkgeom.p | |- P = ( Base ` G ) |
|
2 | tkgeom.d | |- .- = ( dist ` G ) |
|
3 | tkgeom.i | |- I = ( Itv ` G ) |
|
4 | tkgeom.g | |- ( ph -> G e. TarskiG ) |
|
5 | tgbtwnintr.1 | |- ( ph -> A e. P ) |
|
6 | tgbtwnintr.2 | |- ( ph -> B e. P ) |
|
7 | tgbtwnintr.3 | |- ( ph -> C e. P ) |
|
8 | tgbtwnintr.4 | |- ( ph -> D e. P ) |
|
9 | tgbtwnexch3.5 | |- ( ph -> B e. ( A I C ) ) |
|
10 | tgbtwnexch3.6 | |- ( ph -> C e. ( A I D ) ) |
|
11 | 1 2 3 4 5 6 7 9 | tgbtwncom | |- ( ph -> B e. ( C I A ) ) |
12 | 1 2 3 4 5 7 8 10 | tgbtwncom | |- ( ph -> C e. ( D I A ) ) |
13 | 1 2 3 4 6 7 8 5 11 12 | tgbtwnintr | |- ( ph -> C e. ( B I D ) ) |