cgracol

Description: Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020)

	Ref	Expression
Hypotheses	cgracol.p	$⊢ P = {Base}_{G}$
	cgracol.i	$⊢ I = Itv (G)$
	cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
	cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgracol.a	$⊢ φ \to A \in P$
	cgracol.b	$⊢ φ \to B \in P$
	cgracol.c	$⊢ φ \to C \in P$
	cgracol.d	$⊢ φ \to D \in P$
	cgracol.e	$⊢ φ \to E \in P$
	cgracol.f	$⊢ φ \to F \in P$
	cgracol.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgracol.l	$⊢ L = {Line}_{𝒢} (G)$
	cgracol.2	$⊢ φ \to (C \in (A L B) \lor A = B)$
Assertion	cgracol	$⊢ φ \to (F \in (D L E) \lor D = E)$

Proof

Step	Hyp	Ref	Expression
1		cgracol.p	$⊢ P = {Base}_{G}$
2		cgracol.i	$⊢ I = Itv (G)$
3		cgracol.m	$⊢ \underset{˙}{-} = dist (G)$
4		cgracol.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		cgracol.a	$⊢ φ \to A \in P$
6		cgracol.b	$⊢ φ \to B \in P$
7		cgracol.c	$⊢ φ \to C \in P$
8		cgracol.d	$⊢ φ \to D \in P$
9		cgracol.e	$⊢ φ \to E \in P$
10		cgracol.f	$⊢ φ \to F \in P$
11		cgracol.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
12		cgracol.l	$⊢ L = {Line}_{𝒢} (G)$
13		cgracol.2	$⊢ φ \to (C \in (A L B) \lor A = B)$
14	4	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to G \in 𝒢_{Tarski}$
15	5	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to A \in P$
16	6	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to B \in P$
17	7	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to C \in P$
18	8	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to D \in P$
19	9	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to E \in P$
20	10	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to F \in P$
21	11	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
22		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
23	1 2 22 4 5 6 7 8 9 10 11	cgrane2	$⊢ φ \to B \neq C$
24	23	necomd	$⊢ φ \to C \neq B$
25	24	adantr	$⊢ (φ \land C \in (A I B)) \to C \neq B$
26	1 2 22 4 5 6 7 8 9 10 11	cgrane1	$⊢ φ \to A \neq B$
27	26	adantr	$⊢ (φ \land C \in (A I B)) \to A \neq B$
28	4	adantr	$⊢ (φ \land C \in (A I B)) \to G \in 𝒢_{Tarski}$
29	5	adantr	$⊢ (φ \land C \in (A I B)) \to A \in P$
30	7	adantr	$⊢ (φ \land C \in (A I B)) \to C \in P$
31	6	adantr	$⊢ (φ \land C \in (A I B)) \to B \in P$
32		simpr	$⊢ (φ \land C \in (A I B)) \to C \in (A I B)$
33	1 3 2 28 29 30 31 32	tgbtwncom	$⊢ (φ \land C \in (A I B)) \to C \in (B I A)$
34	33	orcd	$⊢ (φ \land C \in (A I B)) \to (C \in (B I A) \lor A \in (B I C))$
35	25 27 34	3jca	$⊢ (φ \land C \in (A I B)) \to (C \neq B \land A \neq B \land (C \in (B I A) \lor A \in (B I C)))$
36	24	adantr	$⊢ (φ \land A \in (C I B)) \to C \neq B$
37	26	adantr	$⊢ (φ \land A \in (C I B)) \to A \neq B$
38	4	adantr	$⊢ (φ \land A \in (C I B)) \to G \in 𝒢_{Tarski}$
39	7	adantr	$⊢ (φ \land A \in (C I B)) \to C \in P$
40	5	adantr	$⊢ (φ \land A \in (C I B)) \to A \in P$
41	6	adantr	$⊢ (φ \land A \in (C I B)) \to B \in P$
42		simpr	$⊢ (φ \land A \in (C I B)) \to A \in (C I B)$
43	1 3 2 38 39 40 41 42	tgbtwncom	$⊢ (φ \land A \in (C I B)) \to A \in (B I C)$
44	43	olcd	$⊢ (φ \land A \in (C I B)) \to (C \in (B I A) \lor A \in (B I C))$
45	36 37 44	3jca	$⊢ (φ \land A \in (C I B)) \to (C \neq B \land A \neq B \land (C \in (B I A) \lor A \in (B I C)))$
46	35 45	jaodan	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (C \neq B \land A \neq B \land (C \in (B I A) \lor A \in (B I C)))$
47	1 2 22 7 5 6 4	ishlg	$⊢ φ \to (C {hl}_{𝒢} (G) (B) A \leftrightarrow (C \neq B \land A \neq B \land (C \in (B I A) \lor A \in (B I C))))$
48	47	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (C {hl}_{𝒢} (G) (B) A \leftrightarrow (C \neq B \land A \neq B \land (C \in (B I A) \lor A \in (B I C))))$
49	46 48	mpbird	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to C {hl}_{𝒢} (G) (B) A$
50	1 2 22 17 15 16 14 49	hlcomd	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to A {hl}_{𝒢} (G) (B) C$
51	1 2 3 14 15 16 17 18 19 20 21 22 50	cgrahl	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to D {hl}_{𝒢} (G) (E) F$
52	1 2 22 18 20 19 14	ishlg	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (D {hl}_{𝒢} (G) (E) F \leftrightarrow (D \neq E \land F \neq E \land (D \in (E I F) \lor F \in (E I D))))$
53	51 52	mpbid	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (D \neq E \land F \neq E \land (D \in (E I F) \lor F \in (E I D)))$
54	53	simp3d	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (D \in (E I F) \lor F \in (E I D))$
55	4	adantr	$⊢ (φ \land D \in (E I F)) \to G \in 𝒢_{Tarski}$
56	9	adantr	$⊢ (φ \land D \in (E I F)) \to E \in P$
57	8	adantr	$⊢ (φ \land D \in (E I F)) \to D \in P$
58	10	adantr	$⊢ (φ \land D \in (E I F)) \to F \in P$
59		simpr	$⊢ (φ \land D \in (E I F)) \to D \in (E I F)$
60	1 3 2 55 56 57 58 59	tgbtwncom	$⊢ (φ \land D \in (E I F)) \to D \in (F I E)$
61	60	olcd	$⊢ (φ \land D \in (E I F)) \to (F \in (D I E) \lor D \in (F I E))$
62	4	adantr	$⊢ (φ \land F \in (E I D)) \to G \in 𝒢_{Tarski}$
63	9	adantr	$⊢ (φ \land F \in (E I D)) \to E \in P$
64	10	adantr	$⊢ (φ \land F \in (E I D)) \to F \in P$
65	8	adantr	$⊢ (φ \land F \in (E I D)) \to D \in P$
66		simpr	$⊢ (φ \land F \in (E I D)) \to F \in (E I D)$
67	1 3 2 62 63 64 65 66	tgbtwncom	$⊢ (φ \land F \in (E I D)) \to F \in (D I E)$
68	67	orcd	$⊢ (φ \land F \in (E I D)) \to (F \in (D I E) \lor D \in (F I E))$
69	61 68	jaodan	$⊢ (φ \land (D \in (E I F) \lor F \in (E I D))) \to (F \in (D I E) \lor D \in (F I E))$
70	54 69	syldan	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (F \in (D I E) \lor D \in (F I E))$
71	70	orcd	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to ((F \in (D I E) \lor D \in (F I E)) \lor E \in (D I F))$
72		df-3or	$⊢ (F \in (D I E) \lor D \in (F I E) \lor E \in (D I F)) \leftrightarrow ((F \in (D I E) \lor D \in (F I E)) \lor E \in (D I F))$
73	71 72	sylibr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (F \in (D I E) \lor D \in (F I E) \lor E \in (D I F))$
74	1 2 4 22 5 6 7 8 9 10 11	cgracom	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
75	1 2 22 4 8 9 10 5 6 7 74	cgrane1	$⊢ φ \to D \neq E$
76	1 12 2 4 8 9 75 10	tgellng	$⊢ φ \to (F \in (D L E) \leftrightarrow (F \in (D I E) \lor D \in (F I E) \lor E \in (D I F)))$
77	76	adantr	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (F \in (D L E) \leftrightarrow (F \in (D I E) \lor D \in (F I E) \lor E \in (D I F)))$
78	73 77	mpbird	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to F \in (D L E)$
79	78	orcd	$⊢ (φ \land (C \in (A I B) \lor A \in (C I B))) \to (F \in (D L E) \lor D = E)$
80	4	adantr	$⊢ (φ \land B \in (A I C)) \to G \in 𝒢_{Tarski}$
81	8	adantr	$⊢ (φ \land B \in (A I C)) \to D \in P$
82	9	adantr	$⊢ (φ \land B \in (A I C)) \to E \in P$
83	10	adantr	$⊢ (φ \land B \in (A I C)) \to F \in P$
84	5	adantr	$⊢ (φ \land B \in (A I C)) \to A \in P$
85	6	adantr	$⊢ (φ \land B \in (A I C)) \to B \in P$
86	7	adantr	$⊢ (φ \land B \in (A I C)) \to C \in P$
87	11	adantr	$⊢ (φ \land B \in (A I C)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
88		simpr	$⊢ (φ \land B \in (A I C)) \to B \in (A I C)$
89	1 2 3 80 84 85 86 81 82 83 87 88	cgrabtwn	$⊢ (φ \land B \in (A I C)) \to E \in (D I F)$
90	1 12 2 80 81 82 83 89	btwncolg3	$⊢ (φ \land B \in (A I C)) \to (F \in (D L E) \lor D = E)$
91	26	neneqd	$⊢ φ \to \neg A = B$
92	13	orcomd	$⊢ φ \to (A = B \lor C \in (A L B))$
93	92	ord	$⊢ φ \to (\neg A = B \to C \in (A L B))$
94	91 93	mpd	$⊢ φ \to C \in (A L B)$
95	1 12 2 4 5 6 26 7	tgellng	$⊢ φ \to (C \in (A L B) \leftrightarrow (C \in (A I B) \lor A \in (C I B) \lor B \in (A I C)))$
96	94 95	mpbid	$⊢ φ \to (C \in (A I B) \lor A \in (C I B) \lor B \in (A I C))$
97		df-3or	$⊢ (C \in (A I B) \lor A \in (C I B) \lor B \in (A I C)) \leftrightarrow ((C \in (A I B) \lor A \in (C I B)) \lor B \in (A I C))$
98	96 97	sylib	$⊢ φ \to ((C \in (A I B) \lor A \in (C I B)) \lor B \in (A I C))$
99	79 90 98	mpjaodan	$⊢ φ \to (F \in (D L E) \lor D = E)$

Metamath Proof Explorer

Theorem cgracol

Proof