tgaaddcpbllem3

	Ref	Expression
Hypotheses	tgaaddcpbl.p	$⊢ P = {Base}_{G}$
	tgaaddcpbl.i	$⊢ I = Itv (G)$
	tgaaddcpbl.l	$⊢ L = {Line}_{𝒢} (G)$
	tgaaddcpbl.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
	tgaaddcpbl.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\}$
	tgaaddcpbl.q	$⊢ Q = \{⟨c, d⟩ \| ((c \in (P ∖ (V L T)) \land d \in (P ∖ (V L T))) \land \exists t \in (V L T) t \in (c I d))\}$
	tgaaddcpbl.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgaaddcpbl.s	$⊢ φ \to S \in P$
	tgaaddcpbl.t	$⊢ φ \to T \in P$
	tgaaddcpbl.u	$⊢ φ \to U \in P$
	tgaaddcpbl.v	$⊢ φ \to V \in P$
	tgaaddcpbl.w	$⊢ φ \to W \in P$
	tgaaddcpbl.x	$⊢ φ \to X \in P$
	tgaaddcpbl.y	$⊢ φ \to Y \in P$
	tgaaddcpbl.z	$⊢ φ \to Z \in P$
	tgaaddcpbl.2	$⊢ φ \to Y \neq S$
	tgaaddcpbl.3	$⊢ φ \to V \neq T$
	tgaaddcpbl.4	$⊢ φ \to X O Z$
	tgaaddcpbl.5	$⊢ φ \to U Q W$
	tgaaddcpbl.6	$⊢ φ \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
	tgaaddcpbl.7	$⊢ φ \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
	tgaaddcpbllem3.1	$⊢ φ \to \neg Y \in (X I Z)$
Assertion	tgaaddcpbllem3	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$

Proof

Step	Hyp	Ref	Expression
1		tgaaddcpbl.p	$⊢ P = {Base}_{G}$
2		tgaaddcpbl.i	$⊢ I = Itv (G)$
3		tgaaddcpbl.l	$⊢ L = {Line}_{𝒢} (G)$
4		tgaaddcpbl.c	$⊢ \underset{˙}{\sim} = \sim_{𝒢}^{∠} (G)$
5		tgaaddcpbl.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\}$
6		tgaaddcpbl.q	$⊢ Q = \{⟨c, d⟩ \| ((c \in (P ∖ (V L T)) \land d \in (P ∖ (V L T))) \land \exists t \in (V L T) t \in (c I d))\}$
7		tgaaddcpbl.1	$⊢ φ \to G \in 𝒢_{Tarski}$
8		tgaaddcpbl.s	$⊢ φ \to S \in P$
9		tgaaddcpbl.t	$⊢ φ \to T \in P$
10		tgaaddcpbl.u	$⊢ φ \to U \in P$
11		tgaaddcpbl.v	$⊢ φ \to V \in P$
12		tgaaddcpbl.w	$⊢ φ \to W \in P$
13		tgaaddcpbl.x	$⊢ φ \to X \in P$
14		tgaaddcpbl.y	$⊢ φ \to Y \in P$
15		tgaaddcpbl.z	$⊢ φ \to Z \in P$
16		tgaaddcpbl.2	$⊢ φ \to Y \neq S$
17		tgaaddcpbl.3	$⊢ φ \to V \neq T$
18		tgaaddcpbl.4	$⊢ φ \to X O Z$
19		tgaaddcpbl.5	$⊢ φ \to U Q W$
20		tgaaddcpbl.6	$⊢ φ \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
21		tgaaddcpbl.7	$⊢ φ \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
22		tgaaddcpbllem3.1	$⊢ φ \to \neg Y \in (X I Z)$
23		eleq1w	$⊢ s = r \to (s \in (a I b) \leftrightarrow r \in (a I b))$
24	23	cbvrexvw	$⊢ \exists s \in (Y L S) s \in (a I b) \leftrightarrow \exists r \in (Y L S) r \in (a I b)$
25	24	anbi2i	$⊢ ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b)) \leftrightarrow ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists r \in (Y L S) r \in (a I b))$
26	25	opabbii	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists s \in (Y L S) s \in (a I b))\} = \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists r \in (Y L S) r \in (a I b))\}$
27	5 26	eqtri	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (Y L S)) \land b \in (P ∖ (Y L S))) \land \exists r \in (Y L S) r \in (a I b))\}$
28	7	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to G \in 𝒢_{Tarski}$
29	8	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to S \in P$
30	9	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to T \in P$
31	10	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to U \in P$
32	11	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to V \in P$
33	12	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to W \in P$
34	13	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to X \in P$
35	14	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to Y \in P$
36	15	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to Z \in P$
37	16	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to Y \neq S$
38	17	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to V \neq T$
39	18	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to X O Z$
40	19	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to U Q W$
41	20	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
42	21	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
43	22	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to \neg Y \in (X I Z)$
44		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
45		simpllr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to s \in (Y L S)$
46		simplr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to s \in (X I Z)$
47		simpr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to s {hl}_{𝒢} (G) (Y) S$
48	1 2 3 4 27 6 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47	tgaaddcpbllem1	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land s {hl}_{𝒢} (G) (Y) S) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
49	7	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to G \in 𝒢_{Tarski}$
50	8	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to S \in P$
51	9	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to T \in P$
52	10	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to U \in P$
53	11	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to V \in P$
54	12	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to W \in P$
55	13	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to X \in P$
56	14	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to Y \in P$
57	15	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to Z \in P$
58	16	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to Y \neq S$
59	17	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to V \neq T$
60	18	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to X O Z$
61	19	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to U Q W$
62	20	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to ⟨“ X Y S ”⟩ \underset{˙}{\sim} ⟨“ U V T ”⟩$
63	21	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to ⟨“ S Y Z ”⟩ \underset{˙}{\sim} ⟨“ T V W ”⟩$
64	22	ad3antrrr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to \neg Y \in (X I Z)$
65		simpllr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to s \in (Y L S)$
66		simplr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to s \in (X I Z)$
67		simpr	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to Y \in (S I s)$
68		eqid	$⊢ {pInv}_{𝒢} (G) (V) = {pInv}_{𝒢} (G) (V)$
69	1 2 3 4 27 6 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 44	tgaaddcpbllem2	$⊢ (((φ \land s \in (Y L S)) \land s \in (X I Z)) \land Y \in (S I s)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
70	8	ad2antrr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to S \in P$
71	14	ad2antrr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to Y \in P$
72	7	ad2antrr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to G \in 𝒢_{Tarski}$
73	1 2 3 7 14 8 16	tgelrnln	$⊢ φ \to Y L S \in ran L$
74	73	ad2antrr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to Y L S \in ran L$
75		simplr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to s \in (Y L S)$
76	1 3 2 72 74 75	tglnpt	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to s \in P$
77	13	ad2antrr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to X \in P$
78	16	necomd	$⊢ φ \to S \neq Y$
79	78	ad2antrr	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to S \neq Y$
80	1 2 3 72 70 71 76 79 75	lncom	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to s \in (S L Y)$
81	1 2 44 70 71 76 72 77 3 80	lnhl	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to (s {hl}_{𝒢} (G) (Y) S \lor Y \in (S I s))$
82	48 69 81	mpjaodan	$⊢ ((φ \land s \in (Y L S)) \land s \in (X I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$
83		eqid	$⊢ dist (G) = dist (G)$
84	1 83 2 5 13 15	islnopp	$⊢ φ \to (X O Z \leftrightarrow ((\neg X \in (Y L S) \land \neg Z \in (Y L S)) \land \exists s \in (Y L S) s \in (X I Z)))$
85	18 84	mpbid	$⊢ φ \to ((\neg X \in (Y L S) \land \neg Z \in (Y L S)) \land \exists s \in (Y L S) s \in (X I Z))$
86	85	simprd	$⊢ φ \to \exists s \in (Y L S) s \in (X I Z)$
87	82 86	r19.29a	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ U V W ”⟩$

Metamath Proof Explorer

Theorem tgaaddcpbllem3

Proof