opphllem5

Description: Second part of Lemma 9.4 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 2-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$
	opphllem5.v	$⊢ φ \to V \in P$
	opphllem5.1	$⊢ φ \to U K (R) A$
	opphllem5.2	$⊢ φ \to V K (S) C$
Assertion	opphllem5	$⊢ φ \to U O V$

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		opphllem5.v	$⊢ φ \to V \in P$
20		opphllem5.1	$⊢ φ \to U K (R) A$
21		opphllem5.2	$⊢ φ \to V K (S) C$
22	1 5 3 7 6 12	tglnpt	$⊢ φ \to R \in P$
23	1 3 8 18 10 22 7 20	hlne2	$⊢ φ \to A \neq R$
24	1 3 5 7 10 22 23	tglinecom	$⊢ φ \to A L R = R L A$
25	16 24	breqtrd	$⊢ φ \to D ⟂_{𝒢} (G) (R L A)$
26	1 3 8 18 10 22 7 20	hlcomd	$⊢ φ \to A K (R) U$
27	1 2 3 5 7 6 8 12 10 18 25 26	hlperpnel	$⊢ φ \to \neg U \in D$
28	27	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to \neg U \in D$
29	1 5 3 7 6 13	tglnpt	$⊢ φ \to S \in P$
30	1 3 8 19 11 29 7 21	hlne2	$⊢ φ \to C \neq S$
31	1 3 5 7 11 29 30	tglinecom	$⊢ φ \to C L S = S L C$
32	17 31	breqtrd	$⊢ φ \to D ⟂_{𝒢} (G) (S L C)$
33	1 3 8 19 11 29 7 21	hlcomd	$⊢ φ \to C K (S) V$
34	1 2 3 5 7 6 8 13 11 19 32 33	hlperpnel	$⊢ φ \to \neg V \in D$
35	34	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to \neg V \in D$
36		simplr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in D$
37		simpr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R = t) \to R = t$
38		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
39	7	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to G \in 𝒢_{Tarski}$
40	11	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to C \in P$
41	22	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in P$
42	7	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to G \in 𝒢_{Tarski}$
43	6	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to D \in ran L$
44	1 5 3 42 43 36	tglnpt	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in P$
45	44	adantr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in P$
46	10	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to A \in P$
47	29	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to S \in P$
48		simpllr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R = S$
49	1 3 5 7 11 29 30	tglinerflx2	$⊢ φ \to S \in (C L S)$
50	49	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to S \in (C L S)$
51	48 50	eqeltrd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (C L S)$
52	51	adantr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in (C L S)$
53	5 7 17	perpln2	$⊢ φ \to C L S \in ran L$
54	1 2 3 5 7 6 53 17	perpcom	$⊢ φ \to (C L S) ⟂_{𝒢} (G) D$
55	54	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to (C L S) ⟂_{𝒢} (G) D$
56		simpr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \neq t$
57	6	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to D \in ran L$
58	12	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in D$
59		simpllr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in D$
60	1 3 5 39 41 45 56 56 57 58 59	tglinethru	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to D = R L t$
61	55 60	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)$
62	1 2 3 5 39 40 47 52 45 61	perprag	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to ⟨“ C R t ”⟩ \in ∟_{𝒢} (G)$
63	1 3 5 7 10 22 23	tglinerflx2	$⊢ φ \to R \in (A L R)$
64	63	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R \in (A L R)$
65	5 7 16	perpln2	$⊢ φ \to A L R \in ran L$
66	1 2 3 5 7 6 65 16	perpcom	$⊢ φ \to (A L R) ⟂_{𝒢} (G) D$
67	66	ad4antr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to (A L R) ⟂_{𝒢} (G) D$
68	67 60	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)$
69	1 2 3 5 39 46 41 64 45 68	perprag	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to ⟨“ A R t ”⟩ \in ∟_{𝒢} (G)$
70		simplr	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in (A I C)$
71	1 2 3 39 46 45 40 70	tgbtwncom	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to t \in (C I A)$
72	1 2 3 5 38 39 40 41 45 46 62 69 71	ragflat2	$⊢ ((((φ \land R = S) \land t \in D) \land t \in (A I C)) \land R \neq t) \to R = t$
73	37 72	pm2.61dane	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R = t$
74	10	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to A \in P$
75	18	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to U \in P$
76	19	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to V \in P$
77	22	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in P$
78	26	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to A K (R) U$
79	11	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to C \in P$
80	21	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to V K (S) C$
81	48	fveq2d	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to K (R) = K (S)$
82	81	breqd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to (V K (R) C \leftrightarrow V K (S) C)$
83	80 82	mpbird	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to V K (R) C$
84	1 3 8 76 79 77 42 83	hlcomd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to C K (R) V$
85		simpr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in (A I C)$
86	73 85	eqeltrd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (A I C)$
87	1 2 3 42 74 77 79 86	tgbtwncom	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (C I A)$
88	1 3 8 79 76 74 42 77 84 87	btwnhl	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (V I A)$
89	1 2 3 42 76 77 74 88	tgbtwncom	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (A I V)$
90	1 3 8 74 75 76 42 77 78 89	btwnhl	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to R \in (U I V)$
91	73 90	eqeltrrd	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to t \in (U I V)$
92		rspe	$⊢ (t \in D \land t \in (U I V)) \to \exists t \in D t \in (U I V)$
93	36 91 92	syl2anc	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to \exists t \in D t \in (U I V)$
94	28 35 93	jca31	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to ((\neg U \in D \land \neg V \in D) \land \exists t \in D t \in (U I V))$
95	1 2 3 4 18 19	islnopp	$⊢ φ \to (U O V \leftrightarrow ((\neg U \in D \land \neg V \in D) \land \exists t \in D t \in (U I V)))$
96	95	ad3antrrr	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to (U O V \leftrightarrow ((\neg U \in D \land \neg V \in D) \land \exists t \in D t \in (U I V)))$
97	94 96	mpbird	$⊢ (((φ \land R = S) \land t \in D) \land t \in (A I C)) \to U O V$
98	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)))$
99	15 98	mpbid	$⊢ φ \to ((\neg A \in D \land \neg C \in D) \land \exists t \in D t \in (A I C))$
100	99	simprd	$⊢ φ \to \exists t \in D t \in (A I C)$
101	100	adantr	$⊢ (φ \land R = S) \to \exists t \in D t \in (A I C)$
102	97 101	r19.29a	$⊢ (φ \land R = S) \to U O V$
103	6	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to D \in ran L$
104	7	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
105		eqid	$⊢ {pInv}_{𝒢} (G) (m) = {pInv}_{𝒢} (G) (m)$
106	10	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to A \in P$
107	11	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to C \in P$
108	12	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to R \in D$
109	13	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to S \in D$
110		simpllr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to m \in P$
111	15	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to A O C$
112	16	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to D ⟂_{𝒢} (G) (A L R)$
113	17	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to D ⟂_{𝒢} (G) (C L S)$
114		simpr	$⊢ (φ \land R \neq S) \to R \neq S$
115	114	ad3antrrr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to R \neq S$
116		simpr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)$
117	18	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to U \in P$
118		simplr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to S = {pInv}_{𝒢} (G) (m) (R)$
119	118	eqcomd	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to {pInv}_{𝒢} (G) (m) (R) = S$
120	19	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to V \in P$
121	20	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to U K (R) A$
122	21	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to V K (S) C$
123	1 2 3 4 5 103 104 8 105 106 107 108 109 110 111 112 113 115 116 117 119 120 121 122	opphllem4	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A)) \to U O V$
124	6	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to D \in ran L$
125	7	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
126	19	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to V \in P$
127	18	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to U \in P$
128	11	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to C \in P$
129	10	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to A \in P$
130	13	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to S \in D$
131	12	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to R \in D$
132		simpllr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to m \in P$
133	15	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to A O C$
134	1 2 3 4 5 124 125 129 128 133	oppcom	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to C O A$
135	17	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to D ⟂_{𝒢} (G) (C L S)$
136	16	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to D ⟂_{𝒢} (G) (A L R)$
137	114	necomd	$⊢ (φ \land R \neq S) \to S \neq R$
138	137	ad3antrrr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to S \neq R$
139		simpr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)$
140	22	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to R \in P$
141		simplr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to S = {pInv}_{𝒢} (G) (m) (R)$
142	141	eqcomd	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to {pInv}_{𝒢} (G) (m) (R) = S$
143	1 2 3 5 38 125 132 105 140 142	mircom	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to {pInv}_{𝒢} (G) (m) (S) = R$
144	21	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to V K (S) C$
145	20	ad4antr	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to U K (R) A$
146	1 2 3 4 5 124 125 8 105 128 129 130 131 132 134 135 136 138 139 126 143 127 144 145	opphllem4	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to V O U$
147	1 2 3 4 5 124 125 126 127 146	oppcom	$⊢ ((((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \land (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C)) \to U O V$
148		eqid	$⊢ \leq_{𝒢} (G) = \leq_{𝒢} (G)$
149	1 2 3 148 7 29 11 22 10	legtrid	$⊢ φ \to ((S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A) \lor (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C))$
150	149	ad3antrrr	$⊢ (((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \to ((S \underset{˙}{-} C) \leq_{𝒢} (G) (R \underset{˙}{-} A) \lor (R \underset{˙}{-} A) \leq_{𝒢} (G) (S \underset{˙}{-} C))$
151	123 147 150	mpjaodan	$⊢ (((φ \land R \neq S) \land m \in P) \land S = {pInv}_{𝒢} (G) (m) (R)) \to U O V$
152	7	adantr	$⊢ (φ \land R \neq S) \to G \in 𝒢_{Tarski}$
153	22	adantr	$⊢ (φ \land R \neq S) \to R \in P$
154	29	adantr	$⊢ (φ \land R \neq S) \to S \in P$
155	1 2 3 4 5 6 7 10 11 15	opptgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
156	155	adantr	$⊢ (φ \land R \neq S) \to G {Dim}_{𝒢} \geq 2$
157	1 2 3 5 152 38 153 154 156	midex	$⊢ (φ \land R \neq S) \to \exists m \in P S = {pInv}_{𝒢} (G) (m) (R)$
158	151 157	r19.29a	$⊢ (φ \land R \neq S) \to U O V$
159	102 158	pm2.61dane	$⊢ φ \to U O V$

Metamath Proof Explorer

Theorem opphllem5

Proof