Theorem cgraswaplr

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

	Ref	Expression
Hypotheses	cgracol.p	|- P = ( Base ` G )
	cgracol.i	|- I = ( Itv ` G )
	cgracol.m	|- .- = ( dist ` G )
	cgracol.g	|- ( ph -> G e. TarskiG )
	cgracol.a	|- ( ph -> A e. P )
	cgracol.b	|- ( ph -> B e. P )
	cgracol.c	|- ( ph -> C e. P )
	cgracol.d	|- ( ph -> D e. P )
	cgracol.e	|- ( ph -> E e. P )
	cgracol.f	|- ( ph -> F e. P )
	cgracol.1	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
Assertion	cgraswaplr	|- ( ph -> <" C B A "> ( cgrA ` G ) <" F E D "> )

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	|- P = ( Base ` G )
2		cgracol.i	|- I = ( Itv ` G )
3		cgracol.m	|- .- = ( dist ` G )
4		cgracol.g	|- ( ph -> G e. TarskiG )
5		cgracol.a	|- ( ph -> A e. P )
6		cgracol.b	|- ( ph -> B e. P )
7		cgracol.c	|- ( ph -> C e. P )
8		cgracol.d	|- ( ph -> D e. P )
9		cgracol.e	|- ( ph -> E e. P )
10		cgracol.f	|- ( ph -> F e. P )
11		cgracol.1	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12		eqid	|- ( hlG ` G ) = ( hlG ` G )
13	1 2 12 4 5 6 7 8 9 10 11	cgrane2	|- ( ph -> B =/= C )
14	13	necomd	|- ( ph -> C =/= B )
15	1 2 12 4 5 6 7 8 9 10 11	cgrane1	|- ( ph -> A =/= B )
16	15	necomd	|- ( ph -> B =/= A )
17	1 2 4 12 7 6 5 14 16	cgraswap	|- ( ph -> <" C B A "> ( cgrA ` G ) <" A B C "> )
18	1 2 4 12 7 6 5 5 6 7 17 8 9 10 11	cgratr	|- ( ph -> <" C B A "> ( cgrA ` G ) <" D E F "> )
19	1 2 12 4 5 6 7 8 9 10 11	cgrane3	|- ( ph -> E =/= D )
20	19	necomd	|- ( ph -> D =/= E )
21	1 2 12 4 5 6 7 8 9 10 11	cgrane4	|- ( ph -> E =/= F )
22	1 2 4 12 8 9 10 20 21	cgraswap	|- ( ph -> <" D E F "> ( cgrA ` G ) <" F E D "> )
23	1 2 4 12 7 6 5 8 9 10 18 10 9 8 22	cgratr	|- ( ph -> <" C B A "> ( cgrA ` G ) <" F E D "> )