Theorem cgrancol

Description: Angle congruence preserves non-colinearity. (Contributed by Thierry Arnoux, 9-Aug-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 "> )
	cgrancol.l	|- L = ( LineG ` G )
	cgrancol.2	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
Assertion	cgrancol	|- ( ph -> -. ( F e. ( D L E ) \/ D = E ) )

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		cgrancol.l	|- L = ( LineG ` G )
13		cgrancol.2	|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
14	4	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> G e. TarskiG )
15	8	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> D e. P )
16	9	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> E e. P )
17	10	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> F e. P )
18	5	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> A e. P )
19	6	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> B e. P )
20	7	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> C e. P )
21		eqid	|- ( hlG ` G ) = ( hlG ` G )
22	11	adantr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
23	1 2 14 21 18 19 20 15 16 17 22	cgracom	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> <" D E F "> ( cgrA ` G ) <" A B C "> )
24		simpr	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> ( F e. ( D L E ) \/ D = E ) )
25	1 2 3 14 15 16 17 18 19 20 23 12 24	cgracol	|- ( ( ph /\ ( F e. ( D L E ) \/ D = E ) ) -> ( C e. ( A L B ) \/ A = B ) )
26	13 25	mtand	|- ( ph -> -. ( F e. ( D L E ) \/ D = E ) )