opphllem6

Description: First part of Lemma 9.4 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 3-Mar-2020)

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	opphl.l	$⊢ L = {Line}_{𝒢} (G)$
	opphl.d	$⊢ φ \to D \in ran L$
	opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	opphl.k	$⊢ K = {hl}_{𝒢} (G)$
	opphllem5.n	$⊢ N = {pInv}_{𝒢} (G) (M)$
	opphllem5.a	$⊢ φ \to A \in P$
	opphllem5.c	$⊢ φ \to C \in P$
	opphllem5.r	$⊢ φ \to R \in D$
	opphllem5.s	$⊢ φ \to S \in D$
	opphllem5.m	$⊢ φ \to M \in P$
	opphllem5.o	$⊢ φ \to A O C$
	opphllem5.p	$⊢ φ \to D ⟂_{𝒢} (G) (A L R)$
	opphllem5.q	$⊢ φ \to D ⟂_{𝒢} (G) (C L S)$
	opphllem5.u	$⊢ φ \to U \in P$
	opphllem6.v	$⊢ φ \to N (R) = S$
Assertion	opphllem6	$⊢ φ \to (U K (R) A \leftrightarrow N (U) K (S) C)$

Proof

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		opphl.l	$⊢ L = {Line}_{𝒢} (G)$
6		opphl.d	$⊢ φ \to D \in ran L$
7		opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		opphl.k	$⊢ K = {hl}_{𝒢} (G)$
9		opphllem5.n	$⊢ N = {pInv}_{𝒢} (G) (M)$
10		opphllem5.a	$⊢ φ \to A \in P$
11		opphllem5.c	$⊢ φ \to C \in P$
12		opphllem5.r	$⊢ φ \to R \in D$
13		opphllem5.s	$⊢ φ \to S \in D$
14		opphllem5.m	$⊢ φ \to M \in P$
15		opphllem5.o	$⊢ φ \to A O C$
16		opphllem5.p	$⊢ φ \to D ⟂_{𝒢} (G) (A L R)$
17		opphllem5.q	$⊢ φ \to D ⟂_{𝒢} (G) (C L S)$
18		opphllem5.u	$⊢ φ \to U \in P$
19		opphllem6.v	$⊢ φ \to N (R) = S$
20		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
21	7	adantr	$⊢ (φ \land R = S) \to G \in 𝒢_{Tarski}$
22	14	adantr	$⊢ (φ \land R = S) \to M \in P$
23	10	adantr	$⊢ (φ \land R = S) \to A \in P$
24	11	adantr	$⊢ (φ \land R = S) \to C \in P$
25	18	adantr	$⊢ (φ \land R = S) \to U \in P$
26	1 5 3 7 6 12	tglnpt	$⊢ φ \to R \in P$
27	5 7 16	perpln2	$⊢ φ \to A L R \in ran L$
28	1 3 5 7 10 26 27	tglnne	$⊢ φ \to A \neq R$
29	28	adantr	$⊢ (φ \land R = S) \to A \neq R$
30	19	adantr	$⊢ (φ \land R = S) \to N (R) = S$
31		simpr	$⊢ (φ \land R = S) \to R = S$
32	30 31	eqtr4d	$⊢ (φ \land R = S) \to N (R) = R$
33	1 2 3 5 20 7 14 9 26	mirinv	$⊢ φ \to (N (R) = R \leftrightarrow M = R)$
34	33	adantr	$⊢ (φ \land R = S) \to (N (R) = R \leftrightarrow M = R)$
35	32 34	mpbid	$⊢ (φ \land R = S) \to M = R$
36	29 35	neeqtrrd	$⊢ (φ \land R = S) \to A \neq M$
37	1 5 3 7 6 13	tglnpt	$⊢ φ \to S \in P$
38	5 7 17	perpln2	$⊢ φ \to C L S \in ran L$
39	1 3 5 7 11 37 38	tglnne	$⊢ φ \to C \neq S$
40	39	adantr	$⊢ (φ \land R = S) \to C \neq S$
41	35 31	eqtrd	$⊢ (φ \land R = S) \to M = S$
42	40 41	neeqtrrd	$⊢ (φ \land R = S) \to C \neq M$
43		simpr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R = t) \to R = t$
44	7	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to G \in 𝒢_{Tarski}$
45	11	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to C \in P$
46	26	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in P$
47	7	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to G \in 𝒢_{Tarski}$
48	6	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to D \in ran L$
49		simplr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in D$
50	1 5 3 47 48 49	tglnpt	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in P$
51	50	adantr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in P$
52	10	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to A \in P$
53	37	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to S \in P$
54		simpllr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R = S$
55	1 3 5 7 11 37 39	tglinerflx2	$⊢ φ \to S \in (C L S)$
56	55	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to S \in (C L S)$
57	54 56	eqeltrd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (C L S)$
58	57	adantr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in (C L S)$
59	1 2 3 5 7 6 38 17	perpcom	$⊢ φ \to (C L S) ⟂_{𝒢} (G) D$
60	59	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to (C L S) ⟂_{𝒢} (G) D$
61		simpr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \neq t$
62	6	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to D \in ran L$
63	12	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in D$
64		simpllr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in D$
65	1 3 5 44 46 51 61 61 62 63 64	tglinethru	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to D = R L t$
66	60 65	breqtrd	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to (C L S) ⟂_{𝒢} (G) (R L t)$
67	1 2 3 5 44 45 53 58 51 66	perprag	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to ⟨“ C R t ”⟩ \in ∟_{𝒢} (G)$
68	1 3 5 7 10 26 28	tglinerflx2	$⊢ φ \to R \in (A L R)$
69	68	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in (A L R)$
70	1 2 3 5 7 6 27 16	perpcom	$⊢ φ \to (A L R) ⟂_{𝒢} (G) D$
71	70	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to (A L R) ⟂_{𝒢} (G) D$
72	71 65	breqtrd	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to (A L R) ⟂_{𝒢} (G) (R L t)$
73	1 2 3 5 44 52 46 69 51 72	perprag	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to ⟨“ A R t ”⟩ \in ∟_{𝒢} (G)$
74		simplr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in (A I C)$
75	1 2 3 44 52 51 45 74	tgbtwncom	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in (C I A)$
76	1 2 3 5 20 44 45 46 51 52 67 73 75	ragflat2	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R = t$
77	43 76	pm2.61dane	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R = t$
78		simpr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in (A I C)$
79	77 78	eqeltrd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (A I C)$
80	1 2 3 4 10 11	islnopp	$⊢ φ \to (A O C \leftrightarrow ((\neg A \in D \land \neg C \in D) \land \exists t \in D t \in (A I C)))$
81	15 80	mpbid	$⊢ φ \to ((\neg A \in D \land \neg C \in D) \land \exists t \in D t \in (A I C))$
82	81	simprd	$⊢ φ \to \exists t \in D t \in (A I C)$
83	82	adantr	$⊢ (φ \land R = S) \to \exists t \in D t \in (A I C)$
84	79 83	r19.29a	$⊢ (φ \land R = S) \to R \in (A I C)$
85	35 84	eqeltrd	$⊢ (φ \land R = S) \to M \in (A I C)$
86	1 2 3 5 20 21 9 8 22 23 24 25 36 42 85	mirbtwnhl	$⊢ (φ \land R = S) \to (U K (M) A \leftrightarrow N (U) K (M) C)$
87	35	fveq2d	$⊢ (φ \land R = S) \to K (M) = K (R)$
88	87	breqd	$⊢ (φ \land R = S) \to (U K (M) A \leftrightarrow U K (R) A)$
89	41	fveq2d	$⊢ (φ \land R = S) \to K (M) = K (S)$
90	89	breqd	$⊢ (φ \land R = S) \to (N (U) K (M) C \leftrightarrow N (U) K (S) C)$
91	86 88 90	3bitr3d	$⊢ (φ \land R = S) \to (U K (R) A \leftrightarrow N (U) K (S) C)$
92	6	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to D \in ran L$
93	7	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
94	10	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to A \in P$
95	11	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to C \in P$
96	12	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to R \in D$
97	13	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to S \in D$
98	14	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to M \in P$
99	15	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to A O C$
100	16	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to D ⟂_{𝒢} (G) (A L R)$
101	17	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to D ⟂_{𝒢} (G) (C L S)$
102		simplr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to R \neq S$
103		simpr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)$
104	18	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to U \in P$
105	19	ad2antrr	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to N (R) = S$
106	1 2 3 4 5 92 93 8 9 94 95 96 97 98 99 100 101 102 103 104 105	opphllem3	$⊢ ((φ \land R \neq S) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to (U K (R) A \leftrightarrow N (U) K (S) C)$
107	6	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to D \in ran L$
108	7	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
109	11	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to C \in P$
110	10	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to A \in P$
111	13	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to S \in D$
112	12	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to R \in D$
113	14	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to M \in P$
114	15	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to A O C$
115	1 2 3 4 5 107 108 110 109 114	oppcom	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to C O A$
116	17	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to D ⟂_{𝒢} (G) (C L S)$
117	16	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to D ⟂_{𝒢} (G) (A L R)$
118		simpr	$⊢ (φ \land R \neq S) \to R \neq S$
119	118	necomd	$⊢ (φ \land R \neq S) \to S \neq R$
120	119	adantr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to S \neq R$
121		simpr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)$
122	18	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to U \in P$
123	1 2 3 5 20 108 113 9 122	mircl	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to N (U) \in P$
124	26	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to R \in P$
125	19	ad2antrr	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to N (R) = S$
126	1 2 3 5 20 108 113 9 124 125	mircom	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to N (S) = R$
127	1 2 3 4 5 107 108 8 9 109 110 111 112 113 115 116 117 120 121 123 126	opphllem3	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to (N (U) K (S) C \leftrightarrow N (N (U)) K (R) A)$
128	1 2 3 5 20 108 113 9 122	mirmir	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to N (N (U)) = U$
129	128	breq1d	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to (N (N (U)) K (R) A \leftrightarrow U K (R) A)$
130	127 129	bitr2d	$⊢ ((φ \land R \neq S) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to (U K (R) A \leftrightarrow N (U) K (S) C)$
131		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
132	1 2 3 131 7 37 11 26 10	legtrid	$⊢ φ \to ((S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A) \lor (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C))$
133	132	adantr	$⊢ (φ \land R \neq S) \to ((S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A) \lor (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C))$
134	106 130 133	mpjaodan	$⊢ (φ \land R \neq S) \to (U K (R) A \leftrightarrow N (U) K (S) C)$
135	91 134	pm2.61dane	$⊢ φ \to (U K (R) A \leftrightarrow N (U) K (S) C)$

Metamath Proof Explorer

Theorem opphllem6

Proof