Description: Vertical angle theorem. Vertical, or opposite angles are the facing pair of angles formed when two lines intersect. Eudemus of Rhodes attributed the proof to Thales of Miletus. The proposition showed that since both of a pair of vertical angles are supplementary to both of the adjacent angles, the vertical angles are equal in measure. We follow the same path. Theorem 11.14 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 27-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dfcgra2.p | |- P = ( Base ` G ) |
|
| dfcgra2.i | |- I = ( Itv ` G ) |
||
| dfcgra2.m | |- .- = ( dist ` G ) |
||
| dfcgra2.g | |- ( ph -> G e. TarskiG ) |
||
| dfcgra2.a | |- ( ph -> A e. P ) |
||
| dfcgra2.b | |- ( ph -> B e. P ) |
||
| dfcgra2.c | |- ( ph -> C e. P ) |
||
| dfcgra2.d | |- ( ph -> D e. P ) |
||
| dfcgra2.e | |- ( ph -> E e. P ) |
||
| dfcgra2.f | |- ( ph -> F e. P ) |
||
| oacgr.1 | |- ( ph -> B e. ( A I D ) ) |
||
| oacgr.2 | |- ( ph -> B e. ( C I F ) ) |
||
| oacgr.3 | |- ( ph -> B =/= A ) |
||
| oacgr.4 | |- ( ph -> B =/= C ) |
||
| oacgr.5 | |- ( ph -> B =/= D ) |
||
| oacgr.6 | |- ( ph -> B =/= F ) |
||
| Assertion | oacgr | |- ( ph -> <" A B C "> ( cgrA ` G ) <" D B F "> ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcgra2.p | |- P = ( Base ` G ) |
|
| 2 | dfcgra2.i | |- I = ( Itv ` G ) |
|
| 3 | dfcgra2.m | |- .- = ( dist ` G ) |
|
| 4 | dfcgra2.g | |- ( ph -> G e. TarskiG ) |
|
| 5 | dfcgra2.a | |- ( ph -> A e. P ) |
|
| 6 | dfcgra2.b | |- ( ph -> B e. P ) |
|
| 7 | dfcgra2.c | |- ( ph -> C e. P ) |
|
| 8 | dfcgra2.d | |- ( ph -> D e. P ) |
|
| 9 | dfcgra2.e | |- ( ph -> E e. P ) |
|
| 10 | dfcgra2.f | |- ( ph -> F e. P ) |
|
| 11 | oacgr.1 | |- ( ph -> B e. ( A I D ) ) |
|
| 12 | oacgr.2 | |- ( ph -> B e. ( C I F ) ) |
|
| 13 | oacgr.3 | |- ( ph -> B =/= A ) |
|
| 14 | oacgr.4 | |- ( ph -> B =/= C ) |
|
| 15 | oacgr.5 | |- ( ph -> B =/= D ) |
|
| 16 | oacgr.6 | |- ( ph -> B =/= F ) |
|
| 17 | eqid | |- ( hlG ` G ) = ( hlG ` G ) |
|
| 18 | 13 | necomd | |- ( ph -> A =/= B ) |
| 19 | 1 2 4 17 5 6 7 18 14 | cgraswap | |- ( ph -> <" A B C "> ( cgrA ` G ) <" C B A "> ) |
| 20 | 16 | necomd | |- ( ph -> F =/= B ) |
| 21 | 1 2 4 17 10 6 5 20 13 | cgraswap | |- ( ph -> <" F B A "> ( cgrA ` G ) <" A B F "> ) |
| 22 | 1 3 2 4 7 6 10 12 | tgbtwncom | |- ( ph -> B e. ( F I C ) ) |
| 23 | 1 2 3 4 10 6 5 5 6 10 7 8 21 22 11 14 15 | sacgr | |- ( ph -> <" C B A "> ( cgrA ` G ) <" D B F "> ) |
| 24 | 1 2 4 17 5 6 7 7 6 5 19 8 6 10 23 | cgratr | |- ( ph -> <" A B C "> ( cgrA ` G ) <" D B F "> ) |