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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	dfcgra2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	dfcgra2.m	⊢ − = ( dist ‘ 𝐺 )
	dfcgra2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	dfcgra2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	dfcgra2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	dfcgra2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	dfcgra2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	dfcgra2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	dfcgra2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	oacgr.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
	oacgr.2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 𝐼 𝐹 ) )
	oacgr.3	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
	oacgr.4	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	oacgr.5	⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
	oacgr.6	⊢ ( 𝜑 → 𝐵 ≠ 𝐹 )
Assertion	oacgr	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝐹 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		dfcgra2.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		dfcgra2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		dfcgra2.m	⊢ − = ( dist ‘ 𝐺 )
4		dfcgra2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		dfcgra2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		dfcgra2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		dfcgra2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		dfcgra2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		dfcgra2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		dfcgra2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		oacgr.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
12		oacgr.2	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐶 𝐼 𝐹 ) )
13		oacgr.3	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
14		oacgr.4	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
15		oacgr.5	⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
16		oacgr.6	⊢ ( 𝜑 → 𝐵 ≠ 𝐹 )
17		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
18	13	necomd	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
19	1 2 4 17 5 6 7 18 14	cgraswap	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )
20	16	necomd	⊢ ( 𝜑 → 𝐹 ≠ 𝐵 )
21	1 2 4 17 10 6 5 20 13	cgraswap	⊢ ( 𝜑 → ⟨“ 𝐹 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐹 ”⟩ )
22	1 3 2 4 7 6 10 12	tgbtwncom	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐹 𝐼 𝐶 ) )
23	1 2 3 4 10 6 5 5 6 10 7 8 21 22 11 14 15	sacgr	⊢ ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝐹 ”⟩ )
24	1 2 4 17 5 6 7 7 6 5 19 8 6 10 23	cgratr	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝐹 ”⟩ )