morleylemrneab

	Ref	Expression
Hypotheses	morley.s	$⊢ S = {Base}_{G}$
	morley.l	$⊢ L = {Line}_{𝒢} (G)$
	morley.e	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	morley.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	morley.a	$⊢ φ \to A \in S$
	morley.b	$⊢ φ \to B \in S$
	morley.c	$⊢ φ \to C \in S$
	morley.p	$⊢ φ \to P \in S$
	morley.q	$⊢ φ \to Q \in S$
	morley.r	$⊢ φ \to R \in S$
	morley.0	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
	morley.1	$⊢ φ \to ⟨“ C A Q ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩$
	morley.2	$⊢ φ \to ⟨“ R A B ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩$
	morley.3	$⊢ φ \to ⟨“ A B R ”⟩ \underset{˙}{\sim} ⟨“ R B P ”⟩$
	morley.4	$⊢ φ \to ⟨“ P B C ”⟩ \underset{˙}{\sim} ⟨“ R B P ”⟩$
	morley.5	$⊢ φ \to ⟨“ B C P ”⟩ \underset{˙}{\sim} ⟨“ P C Q ”⟩$
	morley.6	$⊢ φ \to ⟨“ Q C A ”⟩ \underset{˙}{\sim} ⟨“ P C Q ”⟩$
Assertion	morleylemrneab	$⊢ φ \to \neg R \in (A L B)$

Proof

Step	Hyp	Ref	Expression
1		morley.s	$⊢ S = {Base}_{G}$
2		morley.l	$⊢ L = {Line}_{𝒢} (G)$
3		morley.e	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
4		morley.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		morley.a	$⊢ φ \to A \in S$
6		morley.b	$⊢ φ \to B \in S$
7		morley.c	$⊢ φ \to C \in S$
8		morley.p	$⊢ φ \to P \in S$
9		morley.q	$⊢ φ \to Q \in S$
10		morley.r	$⊢ φ \to R \in S$
11		morley.0	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
12		morley.1	$⊢ φ \to ⟨“ C A Q ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩$
13		morley.2	$⊢ φ \to ⟨“ R A B ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩$
14		morley.3	$⊢ φ \to ⟨“ A B R ”⟩ \underset{˙}{\sim} ⟨“ R B P ”⟩$
15		morley.4	$⊢ φ \to ⟨“ P B C ”⟩ \underset{˙}{\sim} ⟨“ R B P ”⟩$
16		morley.5	$⊢ φ \to ⟨“ B C P ”⟩ \underset{˙}{\sim} ⟨“ P C Q ”⟩$
17		morley.6	$⊢ φ \to ⟨“ Q C A ”⟩ \underset{˙}{\sim} ⟨“ P C Q ”⟩$
18		ioran	$⊢ \neg (C \in (A L B) \lor A = B) \leftrightarrow (\neg C \in (A L B) \land \neg A = B)$
19	11 18	sylib	$⊢ φ \to (\neg C \in (A L B) \land \neg A = B)$
20	19	simpld	$⊢ φ \to \neg C \in (A L B)$
21		eqid	$⊢ Itv (G) = Itv (G)$
22	4	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to G \in 𝒢_{Tarski}$
23	5	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to A \in S$
24	6	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to B \in S$
25	19	simprd	$⊢ φ \to \neg A = B$
26	25	adantr	$⊢ (φ \land R \in (A L B)) \to \neg A = B$
27	26	neqned	$⊢ (φ \land R \in (A L B)) \to A \neq B$
28	27	adantr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to A \neq B$
29	9	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to Q \in S$
30		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
31	10	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to R \in S$
32	13	adantr	$⊢ (φ \land R \in (A L B)) \to ⟨“ R A B ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩$
33	3	breqi	$⊢ ⟨“ R A B ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩ \leftrightarrow ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
34	32 33	sylib	$⊢ (φ \land R \in (A L B)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
35	34	adantr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
36	1 21 30 22 31 23 24 29 23 31 35	cgrane3	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to A \neq Q$
37	36	necomd	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to Q \neq A$
38	1 21 30 22 31 23 24 29 23 31 35	cgrane4	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to A \neq R$
39		simpr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to R \in (A Itv (G) B)$
40	1 21 22 31 23 24 29 23 31 35 39	cgranbtwn	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to (Q \in (A Itv (G) R) \lor R \in (A Itv (G) Q))$
41	1 21 2 22 23 31 29 38 40	btwnlng13	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to Q \in (A L R)$
42	28	necomd	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to B \neq A$
43	1 21 2 22 23 31 24 38 39	btwnlng3	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to B \in (A L R)$
44	1 21 2 22 23 31 38 24 42 43	tglineelsb2	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to A L R = A L B$
45	41 44	eleqtrd	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to Q \in (A L B)$
46	7	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to C \in S$
47	4	adantr	$⊢ (φ \land R \in (A L B)) \to G \in 𝒢_{Tarski}$
48	7	adantr	$⊢ (φ \land R \in (A L B)) \to C \in S$
49	5	adantr	$⊢ (φ \land R \in (A L B)) \to A \in S$
50	9	adantr	$⊢ (φ \land R \in (A L B)) \to Q \in S$
51	10	adantr	$⊢ (φ \land R \in (A L B)) \to R \in S$
52	6	adantr	$⊢ (φ \land R \in (A L B)) \to B \in S$
53	12	adantr	$⊢ (φ \land R \in (A L B)) \to ⟨“ C A Q ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩$
54	3	breqi	$⊢ ⟨“ C A Q ”⟩ \underset{˙}{\sim} ⟨“ Q A R ”⟩ \leftrightarrow ⟨“ C A Q ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
55	53 54	sylib	$⊢ (φ \land R \in (A L B)) \to ⟨“ C A Q ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
56	1 21 47 30 51 49 52 50 49 51 34	cgracom	$⊢ (φ \land R \in (A L B)) \to ⟨“ Q A R ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ R A B ”⟩$
57	1 21 47 30 48 49 50 50 49 51 55 51 49 52 56	cgratr	$⊢ (φ \land R \in (A L B)) \to ⟨“ C A Q ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ R A B ”⟩$
58	1 21 47 30 48 49 50 51 49 52 57	cgracom	$⊢ (φ \land R \in (A L B)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ C A Q ”⟩$
59	58	adantr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ C A Q ”⟩$
60	1 21 22 31 23 24 46 23 29 59 39	cgranbtwn	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to (C \in (A Itv (G) Q) \lor Q \in (A Itv (G) C))$
61	1 21 2 22 23 29 46 36 60	btwnlng13	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to C \in (A L Q)$
62	1 21 2 22 23 24 28 29 37 45 46 61	tglineeltr	$⊢ ((φ \land R \in (A L B)) \land R \in (A Itv (G) B)) \to C \in (A L B)$
63	4	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to G \in 𝒢_{Tarski}$
64	5	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \in S$
65	6	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to B \in S$
66	27	adantr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \neq B$
67	9	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to Q \in S$
68	1 21 30 47 48 49 50 50 49 51 55	cgrane2	$⊢ (φ \land R \in (A L B)) \to A \neq Q$
69	68	adantr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \neq Q$
70	69	necomd	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to Q \neq A$
71	10	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to R \in S$
72	1 21 30 47 51 49 52 50 49 51 34	cgrane4	$⊢ (φ \land R \in (A L B)) \to A \neq R$
73	72	adantr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \neq R$
74		eqid	$⊢ dist (G) = dist (G)$
75	34	adantr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
76		simpr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \in (R Itv (G) B)$
77	1 21 74 63 71 64 65 67 64 71 75 76	cgrabtwn	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \in (Q Itv (G) R)$
78	1 21 2 63 64 71 67 73 77	btwnlng2	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to Q \in (A L R)$
79	72	necomd	$⊢ (φ \land R \in (A L B)) \to R \neq A$
80		simpr	$⊢ (φ \land R \in (A L B)) \to R \in (A L B)$
81	1 21 2 47 49 52 27 51 79 80	tglineelsb2	$⊢ (φ \land R \in (A L B)) \to A L B = A L R$
82	81	adantr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A L B = A L R$
83	78 82	eleqtrrd	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to Q \in (A L B)$
84	7	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to C \in S$
85	58	adantr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ C A Q ”⟩$
86	1 21 74 63 71 64 65 84 64 67 85 76	cgrabtwn	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to A \in (C Itv (G) Q)$
87	1 21 2 63 64 67 84 69 86	btwnlng2	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to C \in (A L Q)$
88	1 21 2 63 64 65 66 67 70 83 84 87	tglineeltr	$⊢ ((φ \land R \in (A L B)) \land A \in (R Itv (G) B)) \to C \in (A L B)$
89	4	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to G \in 𝒢_{Tarski}$
90	5	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to A \in S$
91	6	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to B \in S$
92	27	adantr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to A \neq B$
93	9	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to Q \in S$
94	68	adantr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to A \neq Q$
95	94	necomd	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to Q \neq A$
96	10	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to R \in S$
97	72	adantr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to A \neq R$
98	92	necomd	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to B \neq A$
99	1 21 89 30 91 90 96 98 97	cgraswap	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to ⟨“ B A R ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ R A B ”⟩$
100	34	adantr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
101	1 21 89 30 91 90 96 96 90 91 99 93 90 96 100	cgratr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to ⟨“ B A R ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Q A R ”⟩$
102		simpr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to B \in (A Itv (G) R)$
103	1 21 89 91 90 96 93 90 96 101 102	cgranbtwn	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to (Q \in (A Itv (G) R) \lor R \in (A Itv (G) Q))$
104	1 21 2 89 90 96 93 97 103	btwnlng13	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to Q \in (A L R)$
105	81	adantr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to A L B = A L R$
106	104 105	eleqtrrd	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to Q \in (A L B)$
107	7	ad2antrr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to C \in S$
108	58	adantr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to ⟨“ R A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ C A Q ”⟩$
109	1 21 89 30 91 90 96 96 90 91 99 107 90 93 108	cgratr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to ⟨“ B A R ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ C A Q ”⟩$
110	1 21 89 91 90 96 107 90 93 109 102	cgranbtwn	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to (C \in (A Itv (G) Q) \lor Q \in (A Itv (G) C))$
111	1 21 2 89 90 93 107 94 110	btwnlng13	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to C \in (A L Q)$
112	1 21 2 89 90 91 92 93 95 106 107 111	tglineeltr	$⊢ ((φ \land R \in (A L B)) \land B \in (A Itv (G) R)) \to C \in (A L B)$
113	1 2 21 47 49 52 27 51	tgellng	$⊢ (φ \land R \in (A L B)) \to (R \in (A L B) \leftrightarrow (R \in (A Itv (G) B) \lor A \in (R Itv (G) B) \lor B \in (A Itv (G) R)))$
114	80 113	mpbid	$⊢ (φ \land R \in (A L B)) \to (R \in (A Itv (G) B) \lor A \in (R Itv (G) B) \lor B \in (A Itv (G) R))$
115	62 88 112 114	mpjao3dan	$⊢ (φ \land R \in (A L B)) \to C \in (A L B)$
116	20 115	mtand	$⊢ φ \to \neg R \in (A L B)$

Metamath Proof Explorer

Theorem morleylemrneab

Proof