Theorem cgraswaplr

Description: Swap both side of angle congruence. (Contributed by Thierry Arnoux, 5-Oct-2020)

	Ref	Expression
Hypotheses	cgracol.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	cgracol.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	cgracol.m	⊢ − = ( dist ‘ 𝐺 )
	cgracol.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	cgracol.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	cgracol.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	cgracol.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	cgracol.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	cgracol.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	cgracol.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	cgracol.1	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion	cgraswaplr	⊢ ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐸 𝐷 ”⟩ )

Proof

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