Metamath Proof Explorer


Theorem oacgr

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 "> )

Proof

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 "> )