opphllem

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
	mideu.1	$⊢ φ \to A \in P$
	mideu.2	$⊢ φ \to B \in P$
	mideulem.1	$⊢ φ \to A \neq B$
	mideulem.2	$⊢ φ \to Q \in P$
	mideulem.3	$⊢ φ \to O \in P$
	mideulem.4	$⊢ φ \to T \in P$
	mideulem.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (Q L B)$
	mideulem.6	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (A L O)$
	mideulem.7	$⊢ φ \to T \in (A L B)$
	mideulem.8	$⊢ φ \to T \in (Q I O)$
	opphllem.1	$⊢ φ \to R \in P$
	opphllem.2	$⊢ φ \to R \in (B I Q)$
	opphllem.3	$⊢ φ \to A \underset{˙}{-} O = B \underset{˙}{-} R$
Assertion	opphllem	$⊢ φ \to \exists x \in P (B = S (x) (A) \land O = S (x) (R))$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		mideu.s	$⊢ S = {pInv}_{𝒢} (G)$
7		mideu.1	$⊢ φ \to A \in P$
8		mideu.2	$⊢ φ \to B \in P$
9		mideulem.1	$⊢ φ \to A \neq B$
10		mideulem.2	$⊢ φ \to Q \in P$
11		mideulem.3	$⊢ φ \to O \in P$
12		mideulem.4	$⊢ φ \to T \in P$
13		mideulem.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (Q L B)$
14		mideulem.6	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (A L O)$
15		mideulem.7	$⊢ φ \to T \in (A L B)$
16		mideulem.8	$⊢ φ \to T \in (Q I O)$
17		opphllem.1	$⊢ φ \to R \in P$
18		opphllem.2	$⊢ φ \to R \in (B I Q)$
19		opphllem.3	$⊢ φ \to A \underset{˙}{-} O = B \underset{˙}{-} R$
20	5	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to G \in 𝒢_{Tarski}$
21		eqid	$⊢ S (x) = S (x)$
22	8	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to B \in P$
23	11	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to O \in P$
24	7	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to A \in P$
25	17	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to R \in P$
26		simprl	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in P$
27	9	necomd	$⊢ φ \to B \neq A$
28	27	neneqd	$⊢ φ \to \neg B = A$
29	28	adantr	$⊢ (φ \land O \in (B L A)) \to \neg B = A$
30	4 5 14	perpln2	$⊢ φ \to A L O \in ran L$
31	1 3 4 5 7 11 30	tglnne	$⊢ φ \to A \neq O$
32	31	necomd	$⊢ φ \to O \neq A$
33	32	neneqd	$⊢ φ \to \neg O = A$
34	33	adantr	$⊢ (φ \land O \in (B L A)) \to \neg O = A$
35	29 34	jca	$⊢ (φ \land O \in (B L A)) \to (\neg B = A \land \neg O = A)$
36	5	adantr	$⊢ (φ \land O \in (B L A)) \to G \in 𝒢_{Tarski}$
37	8	adantr	$⊢ (φ \land O \in (B L A)) \to B \in P$
38	7	adantr	$⊢ (φ \land O \in (B L A)) \to A \in P$
39	11	adantr	$⊢ (φ \land O \in (B L A)) \to O \in P$
40	1 3 4 5 8 7 27	tglinerflx2	$⊢ φ \to A \in (B L A)$
41	1 3 4 5 7 8 9	tglinecom	$⊢ φ \to A L B = B L A$
42	41 14	eqbrtrrd	$⊢ φ \to (B L A) ⟂_{𝒢} (G) (A L O)$
43	1 2 3 4 5 8 7 40 11 42	perprag	$⊢ φ \to ⟨“ B A O ”⟩ \in ∟_{𝒢} (G)$
44	43	adantr	$⊢ (φ \land O \in (B L A)) \to ⟨“ B A O ”⟩ \in ∟_{𝒢} (G)$
45		simpr	$⊢ (φ \land O \in (B L A)) \to O \in (B L A)$
46	45	orcd	$⊢ (φ \land O \in (B L A)) \to (O \in (B L A) \lor B = A)$
47	1 2 3 4 6 36 37 38 39 44 46	ragflat3	$⊢ (φ \land O \in (B L A)) \to (B = A \lor O = A)$
48		oran	$⊢ (B = A \lor O = A) \leftrightarrow \neg (\neg B = A \land \neg O = A)$
49	47 48	sylib	$⊢ (φ \land O \in (B L A)) \to \neg (\neg B = A \land \neg O = A)$
50	35 49	pm2.65da	$⊢ φ \to \neg O \in (B L A)$
51	50	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \neg O \in (B L A)$
52	41	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to A L B = B L A$
53	51 52	neleqtrrd	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \neg O \in (A L B)$
54	9	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to A \neq B$
55	54	neneqd	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \neg A = B$
56	53 55	jca	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to (\neg O \in (A L B) \land \neg A = B)$
57		pm4.56	$⊢ (\neg O \in (A L B) \land \neg A = B) \leftrightarrow \neg (O \in (A L B) \lor A = B)$
58	56 57	sylib	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \neg (O \in (A L B) \lor A = B)$
59	1 4 3 20 24 22 23 58	ncolrot2	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \neg (B \in (O L A) \lor O = A)$
60		simprrr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (R I O)$
61	1 2 3 20 25 26 23 60	tgbtwncom	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (O I R)$
62	12	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to T \in P$
63	15	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to T \in (A L B)$
64		simprrl	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (T I B)$
65	1 3 4 20 62 24 22 26 63 64	coltr3	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (A L B)$
66	50 41	neleqtrrd	$⊢ φ \to \neg O \in (A L B)$
67	66	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \neg O \in (A L B)$
68		nelne2	$⊢ (x \in (A L B) \land \neg O \in (A L B)) \to x \neq O$
69	65 67 68	syl2anc	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \neq O$
70	1 2 3 20 23 26 25 61 69	tgbtwnne	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to O \neq R$
71	1 2 3 4 6 5 8 7 11	israg	$⊢ φ \to (⟨“ B A O ”⟩ \in ∟_{𝒢} (G) \leftrightarrow B \underset{˙}{-} O = B \underset{˙}{-} S (A) (O))$
72	43 71	mpbid	$⊢ φ \to B \underset{˙}{-} O = B \underset{˙}{-} S (A) (O)$
73	72	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \underset{˙}{-} O = B \underset{˙}{-} S (A) (O)$
74	5	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to G \in 𝒢_{Tarski}$
75		eqid	$⊢ S (A) = S (A)$
76	1 2 3 4 6 20 24 75 23	mircl	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to S (A) (O) \in P$
77	76	ad2antrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to S (A) (O) \in P$
78	7	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \in P$
79	11	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to O \in P$
80	17	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to R \in P$
81	8	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \in P$
82		simplr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to s \in P$
83	1 2 3 4 6 74 78 75 79	mirbtwn	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \in (S (A) (O) I O)$
84		eqid	$⊢ S (B) = S (B)$
85	1 2 3 4 6 74 81 84 82	mirbtwn	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \in (S (B) (s) I s)$
86		simpr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to R = S (m) (s)$
87	74	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to G \in 𝒢_{Tarski}$
88	78	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to A \in P$
89	81	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to B \in P$
90	54	ad4antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to A \neq B$
91	10	ad5antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to Q \in P$
92	79	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to O \in P$
93	62	ad4antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to T \in P$
94	13	ad5antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to (A L B) ⟂_{𝒢} (G) (Q L B)$
95	14	ad5antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to (A L B) ⟂_{𝒢} (G) (A L O)$
96	63	ad4antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to T \in (A L B)$
97	16	ad5antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to T \in (Q I O)$
98	80	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to R \in P$
99	18	ad5antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to R \in (B I Q)$
100	19	ad5antr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to A \underset{˙}{-} O = B \underset{˙}{-} R$
101	26	ad2antrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \in P$
102	101	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to x \in P$
103		simp-5r	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to (x \in P \land (x \in (T I B) \land x \in (R I O)))$
104	103	simprd	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to (x \in (T I B) \land x \in (R I O))$
105	104	simpld	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to x \in (T I B)$
106	104	simprd	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to x \in (R I O)$
107	82	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to s \in P$
108		simpllr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)$
109	108	simpld	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to x \in (S (A) (O) I s)$
110		simprr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \underset{˙}{-} s = x \underset{˙}{-} R$
111	110	ad2antrr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to x \underset{˙}{-} s = x \underset{˙}{-} R$
112		simplr	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to m \in P$
113	1 2 3 4 87 6 88 89 90 91 92 93 94 95 96 97 98 99 100 102 105 106 107 109 111 112 86	mideulem2	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to B = m$
114	113	eqcomd	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to m = B$
115	114	fveq2d	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to S (m) = S (B)$
116	115	fveq1d	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to S (m) (s) = S (B) (s)$
117	86 116	eqtrd	$⊢ (((((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \land m \in P) \land R = S (m) (s)) \to R = S (B) (s)$
118		eqid	$⊢ S (m) = S (m)$
119	1 2 3 4 6 74 118 82 80 101 110	midexlem	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to \exists m \in P R = S (m) (s)$
120	117 119	r19.29a	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to R = S (B) (s)$
121	120	oveq1d	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to R I s = S (B) (s) I s$
122	85 121	eleqtrrd	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \in (R I s)$
123	1 2 3 4 6 74 78 75 79	mircgr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \underset{˙}{-} S (A) (O) = A \underset{˙}{-} O$
124	19	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \underset{˙}{-} O = B \underset{˙}{-} R$
125	123 124	eqtrd	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \underset{˙}{-} S (A) (O) = B \underset{˙}{-} R$
126	1 2 3 74 78 77 81 80 125	tgcgrcomlr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to S (A) (O) \underset{˙}{-} A = R \underset{˙}{-} B$
127	120	oveq2d	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \underset{˙}{-} R = B \underset{˙}{-} S (B) (s)$
128	1 2 3 4 6 74 81 84 82	mircgr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \underset{˙}{-} S (B) (s) = B \underset{˙}{-} s$
129	124 127 128	3eqtrd	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \underset{˙}{-} O = B \underset{˙}{-} s$
130	1 2 3 74 77 78 79 80 81 82 83 122 126 129	tgcgrextend	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to S (A) (O) \underset{˙}{-} O = R \underset{˙}{-} s$
131	1 2 3 74 77 80	axtgcgrrflx	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to S (A) (O) \underset{˙}{-} R = R \underset{˙}{-} S (A) (O)$
132	1 2 3 74 79 80	axtgcgrrflx	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to O \underset{˙}{-} R = R \underset{˙}{-} O$
133	60	ad2antrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \in (R I O)$
134		simprl	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \in (S (A) (O) I s)$
135	1 2 3 74 77 101 82 134	tgbtwncom	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \in (s I S (A) (O))$
136	1 2 3 74 101 82 101 80 110	tgcgrcomlr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to s \underset{˙}{-} x = R \underset{˙}{-} x$
137	136	eqcomd	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to R \underset{˙}{-} x = s \underset{˙}{-} x$
138	43	ad3antrrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to ⟨“ B A O ”⟩ \in ∟_{𝒢} (G)$
139	54	necomd	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to B \neq A$
140	139	ad2antrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \neq A$
141	65	ad2antrr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \in (A L B)$
142	141	orcd	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to (x \in (A L B) \lor A = B)$
143	1 4 3 74 78 81 101 142	colcom	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to (x \in (B L A) \lor B = A)$
144	1 4 3 74 81 78 101 143	colrot1	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to (B \in (A L x) \lor A = x)$
145	1 2 3 4 6 74 81 78 79 101 138 140 144	ragcol	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to ⟨“ x A O ”⟩ \in ∟_{𝒢} (G)$
146	1 2 3 4 6 74 101 78 79	israg	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to (⟨“ x A O ”⟩ \in ∟_{𝒢} (G) \leftrightarrow x \underset{˙}{-} O = x \underset{˙}{-} S (A) (O))$
147	145 146	mpbid	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to x \underset{˙}{-} O = x \underset{˙}{-} S (A) (O)$
148	1 2 3 74 80 101 79 82 101 77 133 135 137 147	tgcgrextend	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to R \underset{˙}{-} O = s \underset{˙}{-} S (A) (O)$
149	132 148	eqtrd	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to O \underset{˙}{-} R = s \underset{˙}{-} S (A) (O)$
150	1 2 3 74 77 78 79 80 80 81 82 77 83 122 130 129 131 149	tgifscgr	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to A \underset{˙}{-} R = B \underset{˙}{-} S (A) (O)$
151	73 150	eqtr4d	$⊢ (((φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \land s \in P) \land (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)) \to B \underset{˙}{-} O = A \underset{˙}{-} R$
152	1 2 3 20 76 26 26 25	axtgsegcon	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to \exists s \in P (x \in (S (A) (O) I s) \land x \underset{˙}{-} s = x \underset{˙}{-} R)$
153	151 152	r19.29a	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to B \underset{˙}{-} O = A \underset{˙}{-} R$
154	19	adantr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to A \underset{˙}{-} O = B \underset{˙}{-} R$
155	1 2 3 20 24 23 22 25 154	tgcgrcomlr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to O \underset{˙}{-} A = R \underset{˙}{-} B$
156	143 152	r19.29a	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to (x \in (B L A) \lor B = A)$
157	1 4 3 20 23 25 26 61	btwncolg1	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to (x \in (O L R) \lor O = R)$
158	1 2 3 4 6 20 21 22 23 24 25 26 59 70 153 155 156 157	symquadlem	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to B = S (x) (A)$
159	1 2 3 4 6 20 26 21 24	mirbtwn	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (S (x) (A) I A)$
160	158	oveq1d	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to B I A = S (x) (A) I A$
161	159 160	eleqtrrd	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (B I A)$
162	1 2 3 20 22 26 24 161	tgbtwncom	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \in (A I B)$
163	1 2 3 20 24 22	axtgcgrrflx	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to A \underset{˙}{-} B = B \underset{˙}{-} A$
164	158	oveq2d	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \underset{˙}{-} B = x \underset{˙}{-} S (x) (A)$
165	1 2 3 4 6 20 26 21 24	mircgr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \underset{˙}{-} S (x) (A) = x \underset{˙}{-} A$
166	164 165	eqtrd	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \underset{˙}{-} B = x \underset{˙}{-} A$
167	1 2 3 20 24 26 22 23 22 26 24 25 162 161 163 166 154 153	tgifscgr	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to x \underset{˙}{-} O = x \underset{˙}{-} R$
168	1 2 3 4 6 20 26 21 25 23 167 61	ismir	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to O = S (x) (R)$
169	158 168	jca	$⊢ (φ \land (x \in P \land (x \in (T I B) \land x \in (R I O)))) \to (B = S (x) (A) \land O = S (x) (R))$
170	1 2 3 5 10 12 11 16	tgbtwncom	$⊢ φ \to T \in (O I Q)$
171	1 2 3 5 11 8 10 12 17 170 18	axtgpasch	$⊢ φ \to \exists x \in P (x \in (T I B) \land x \in (R I O))$
172	169 171	reximddv	$⊢ φ \to \exists x \in P (B = S (x) (A) \land O = S (x) (R))$

Metamath Proof Explorer

Theorem opphllem

Proof