tgaaddcpbllem3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgaaddcpbllem3		Structured version Visualization version GIF version

Theorem tgaaddcpbllem3 29230

Description: Lemma for tgaaddcpbl 29231. (Contributed by Thierry Arnoux, 2-Aug-2026.)

**Hypotheses**
Ref	Expression
tgaaddcpbl.p	⊢ 𝑃 = (Base‘𝐺)
tgaaddcpbl.i	⊢ 𝐼 = (Itv‘𝐺)
tgaaddcpbl.l	⊢ 𝐿 = (LineG‘𝐺)
tgaaddcpbl.c	⊢ ∼ = (cgrA‘𝐺)
tgaaddcpbl.o	⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
tgaaddcpbl.q	⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
tgaaddcpbl.1	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgaaddcpbl.s	⊢ (𝜑 → 𝑆 ∈ 𝑃)
tgaaddcpbl.t	⊢ (𝜑 → 𝑇 ∈ 𝑃)
tgaaddcpbl.u	⊢ (𝜑 → 𝑈 ∈ 𝑃)
tgaaddcpbl.v	⊢ (𝜑 → 𝑉 ∈ 𝑃)
tgaaddcpbl.w	⊢ (𝜑 → 𝑊 ∈ 𝑃)
tgaaddcpbl.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
tgaaddcpbl.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
tgaaddcpbl.z	⊢ (𝜑 → 𝑍 ∈ 𝑃)
tgaaddcpbl.2	⊢ (𝜑 → 𝑌 ≠ 𝑆)
tgaaddcpbl.3	⊢ (𝜑 → 𝑉 ≠ 𝑇)
tgaaddcpbl.4	⊢ (𝜑 → 𝑋𝑂𝑍)
tgaaddcpbl.5	⊢ (𝜑 → 𝑈𝑄𝑊)
tgaaddcpbl.6	⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
tgaaddcpbl.7	⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
tgaaddcpbllem3.1	⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))

**Assertion**
Ref	Expression
tgaaddcpbllem3	⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

Distinct variable groups: ∼ ,𝑠,𝑡 𝐺,𝑐,𝑑,𝑡,𝑠 𝐼,𝑎,𝑏,𝑠,𝑐,𝑑,𝑡 𝐿,𝑎,𝑏,𝑠,𝑐,𝑑,𝑡 𝑂,𝑠 𝑃,𝑎,𝑏,𝑠,𝑐,𝑑,𝑡 𝑄,𝑐,𝑑,𝑡 𝑆,𝑎,𝑏,𝑠,𝑡 𝑇,𝑐,𝑑,𝑡 𝑈,𝑐,𝑑,𝑡,𝑠 𝑉,𝑐,𝑑,𝑡,𝑠 𝑊,𝑠,𝑡 𝑋,𝑠,𝑡 𝑌,𝑎,𝑏,𝑠,𝑡 𝑍,𝑠,𝑡 𝜑,𝑠,𝑡 𝐺,𝑎,𝑏,𝑐,𝑑,𝑡,𝑠 𝑆,𝑐,𝑑 𝑇,𝑎,𝑏 𝑉,𝑎,𝑏 𝑋,𝑐,𝑑 𝑌,𝑐,𝑑 𝑍,𝑐,𝑑 𝜑,𝑐,𝑑 Allowed substitution hints: 𝜑(𝑎, 𝑏) 𝑄(𝑠, 𝑎, 𝑏) ∼ (𝑎, 𝑏, 𝑐, 𝑑) 𝑇(𝑠) 𝑈(𝑎, 𝑏) 𝑂(𝑡, 𝑎, 𝑏, 𝑐, 𝑑) 𝑊(𝑎, 𝑏, 𝑐, 𝑑) 𝑋(𝑎, 𝑏) 𝑍(𝑎, 𝑏)

Proof of Theorem tgaaddcpbllem3 Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tgaaddcpbl.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		tgaaddcpbl.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
3		tgaaddcpbl.l	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
4		tgaaddcpbl.c	. . . 4 ⊢ ∼ = (cgrA‘𝐺)
5		tgaaddcpbl.o	. . . . 5 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))}
6		eleq1w 2843	. . . . . . . 8 ⊢ (𝑠 = 𝑟 → (𝑠 ∈ (𝑎𝐼𝑏) ↔ 𝑟 ∈ (𝑎𝐼𝑏)))
7	6	cbvrexvw 3241	. . . . . . 7 ⊢ (∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏) ↔ ∃𝑟 ∈ (𝑌𝐿𝑆)𝑟 ∈ (𝑎𝐼𝑏))
8	7	anbi2i 635	. . . . . 6 ⊢ (((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑟 ∈ (𝑌𝐿𝑆)𝑟 ∈ (𝑎𝐼𝑏)))
9	8	opabbii 5172	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑎𝐼𝑏))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑟 ∈ (𝑌𝐿𝑆)𝑟 ∈ (𝑎𝐼𝑏))}
10	5, 9	eqtri 2783	. . . 4 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑌𝐿𝑆)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑌𝐿𝑆))) ∧ ∃𝑟 ∈ (𝑌𝐿𝑆)𝑟 ∈ (𝑎𝐼𝑏))}
11		tgaaddcpbl.q	. . . 4 ⊢ 𝑄 = {⟨𝑐, 𝑑⟩ ∣ ((𝑐 ∈ (𝑃 ∖ (𝑉𝐿𝑇)) ∧ 𝑑 ∈ (𝑃 ∖ (𝑉𝐿𝑇))) ∧ ∃𝑡 ∈ (𝑉𝐿𝑇)𝑡 ∈ (𝑐𝐼𝑑))}
12		tgaaddcpbl.1	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
13	12	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝐺 ∈ TarskiG)
14		tgaaddcpbl.s	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
15	14	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑆 ∈ 𝑃)
16		tgaaddcpbl.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ 𝑃)
17	16	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑇 ∈ 𝑃)
18		tgaaddcpbl.u	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝑃)
19	18	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑈 ∈ 𝑃)
20		tgaaddcpbl.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ 𝑃)
21	20	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑉 ∈ 𝑃)
22		tgaaddcpbl.w	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
23	22	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑊 ∈ 𝑃)
24		tgaaddcpbl.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
25	24	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑋 ∈ 𝑃)
26		tgaaddcpbl.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
27	26	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑌 ∈ 𝑃)
28		tgaaddcpbl.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
29	28	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑍 ∈ 𝑃)
30		tgaaddcpbl.2	. . . . 5 ⊢ (𝜑 → 𝑌 ≠ 𝑆)
31	30	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑌 ≠ 𝑆)
32		tgaaddcpbl.3	. . . . 5 ⊢ (𝜑 → 𝑉 ≠ 𝑇)
33	32	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑉 ≠ 𝑇)
34		tgaaddcpbl.4	. . . . 5 ⊢ (𝜑 → 𝑋𝑂𝑍)
35	34	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑋𝑂𝑍)
36		tgaaddcpbl.5	. . . . 5 ⊢ (𝜑 → 𝑈𝑄𝑊)
37	36	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑈𝑄𝑊)
38		tgaaddcpbl.6	. . . . 5 ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
39	38	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
40		tgaaddcpbl.7	. . . . 5 ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
41	40	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
42		tgaaddcpbllem3.1	. . . . 5 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑋𝐼𝑍))
43	42	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → ¬ 𝑌 ∈ (𝑋𝐼𝑍))
44		eqid 2760	. . . 4 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
45		simpllr 788	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑠 ∈ (𝑌𝐿𝑆))
46		simplr 781	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑠 ∈ (𝑋𝐼𝑍))
47		simpr 490	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → 𝑠((hlG‘𝐺)‘𝑌)𝑆)
48	1, 2, 3, 4, 10, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, 44, 45, 46, 47	tgaaddcpbllem1 29228	. . 3 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑠((hlG‘𝐺)‘𝑌)𝑆) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
49	12	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝐺 ∈ TarskiG)
50	14	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑆 ∈ 𝑃)
51	16	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑇 ∈ 𝑃)
52	18	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑈 ∈ 𝑃)
53	20	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑉 ∈ 𝑃)
54	22	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑊 ∈ 𝑃)
55	24	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑋 ∈ 𝑃)
56	26	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑌 ∈ 𝑃)
57	28	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑍 ∈ 𝑃)
58	30	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑌 ≠ 𝑆)
59	32	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑉 ≠ 𝑇)
60	34	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑋𝑂𝑍)
61	36	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑈𝑄𝑊)
62	38	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩)
63	40	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩)
64	42	ad3antrrr 743	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → ¬ 𝑌 ∈ (𝑋𝐼𝑍))
65		simpllr 788	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑠 ∈ (𝑌𝐿𝑆))
66		simplr 781	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑠 ∈ (𝑋𝐼𝑍))
67		simpr 490	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → 𝑌 ∈ (𝑆𝐼𝑠))
68		eqid 2760	. . . 4 ⊢ ((pInvG‘𝐺)‘𝑉) = ((pInvG‘𝐺)‘𝑉)
69	1, 2, 3, 4, 10, 11, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 44	tgaaddcpbllem2 29229	. . 3 ⊢ ((((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) ∧ 𝑌 ∈ (𝑆𝐼𝑠)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
70	14	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑆 ∈ 𝑃)
71	26	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ 𝑃)
72	12	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝐺 ∈ TarskiG)
73	1, 2, 3, 12, 26, 14, 30	tgelrnln 28977	. . . . . 6 ⊢ (𝜑 → (𝑌𝐿𝑆) ∈ ran 𝐿)
74	73	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → (𝑌𝐿𝑆) ∈ ran 𝐿)
75		simplr 781	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑠 ∈ (𝑌𝐿𝑆))
76	1, 3, 2, 72, 74, 75	tglnpt 28891	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑠 ∈ 𝑃)
77	24	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑋 ∈ 𝑃)
78	30	necomd 3010	. . . . . 6 ⊢ (𝜑 → 𝑆 ≠ 𝑌)
79	78	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑆 ≠ 𝑌)
80	1, 2, 3, 72, 70, 71, 76, 79, 75	lncom 28969	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → 𝑠 ∈ (𝑆𝐿𝑌))
81	1, 2, 44, 70, 71, 76, 72, 77, 3, 80	lnhl 28960	. . 3 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → (𝑠((hlG‘𝐺)‘𝑌)𝑆 ∨ 𝑌 ∈ (𝑆𝐼𝑠)))
82	48, 69, 81	mpjaodan 973	. 2 ⊢ (((𝜑 ∧ 𝑠 ∈ (𝑌𝐿𝑆)) ∧ 𝑠 ∈ (𝑋𝐼𝑍)) → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)
83		eqid 2760	. . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺)
84	1, 83, 2, 5, 24, 28	islnopp 29094	. . . 4 ⊢ (𝜑 → (𝑋𝑂𝑍 ↔ ((¬ 𝑋 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑋𝐼𝑍))))
85	34, 84	mpbid 235	. . 3 ⊢ (𝜑 → ((¬ 𝑋 ∈ (𝑌𝐿𝑆) ∧ ¬ 𝑍 ∈ (𝑌𝐿𝑆)) ∧ ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑋𝐼𝑍)))
86	85	simprd 501	. 2 ⊢ (𝜑 → ∃𝑠 ∈ (𝑌𝐿𝑆)𝑠 ∈ (𝑋𝐼𝑍))
87	82, 86	r19.29a 3170	1 ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∃wrex 3086 ∖ cdif 3896 class class class wbr 5103 {copab 5167 ran crn 5656 ‘cfv 6533 (class class class)co 7413 ⟨“cs3 14913 Basecbs 17301 distcds 17351 TarskiGcstrkg 28768 Itvcitv 28774 LineGclng 28775 hlGchlg 28942 pInvGcmir 29003 cgrAccgra 29193

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-oadd 8459 df-er 8696 df-map 8828 df-pm 8829 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-dju 9906 df-card 9944 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-nn 12258 df-2 12327 df-3 12328 df-n0 12529 df-xnn0 12602 df-z 12616 df-uz 12888 df-fz 13562 df-fzo 13710 df-hash 14395 df-word 14579 df-concat 14636 df-s1 14663 df-s2 14919 df-s3 14920 df-trkgc 28789 df-trkgb 28790 df-trkgcb 28791 df-trkgld 28793 df-trkg 28794 df-cgrg 28853 df-leg 28925 df-hlg 28943 df-mir 29004 df-rag 29048 df-perpg 29050 df-hpg 29115 df-mid 29158 df-lmi 29159 df-cgra 29194

This theorem is used by: tgaaddcpbl 29231

W3C validator