prlngmolem2 - Metamath Proof Explorer

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

Theorem prlngmolem2 29184

Description: Lemma for prlngmo 29185. (Contributed by Thierry Arnoux, 5-Jul-2026.)

**Hypotheses**
Ref	Expression
prlngeu.p	⊢ 𝑃 = (Base‘𝐺)
prlngeu.l	⊢ 𝐿 = (LineG‘𝐺)
prlngeu.r	⊢ ∥ = (parlnG‘𝐺)
prlngeu.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
prlngeu.a	⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
prlngeu.x	⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))
prlngeu.1	⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
prlngmolem2.1	⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝑏) ∧ 𝑦 ∈ (𝑃 ∖ 𝑏)) ∧ ∃𝑟 ∈ 𝑏 𝑟 ∈ (𝑥(Itv‘𝐺)𝑦))}
prlngmolem2.2	⊢ 𝑄 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝐴) ∧ 𝑦 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑠 ∈ 𝐴 𝑠 ∈ (𝑥(Itv‘𝐺)𝑦))}

**Assertion**
Ref	Expression
prlngmolem2	⊢ (𝜑 → ∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))

Distinct variable groups: ∥ ,𝑏 𝐴,𝑏 𝐿,𝑏 𝑋,𝑏 𝜑,𝑏 ∥ ,𝑟,𝑠,𝑦,𝑏 𝐴,𝑟,𝑠,𝑥,𝑦,𝑏 𝐺,𝑟,𝑠,𝑥,𝑦 𝐿,𝑟,𝑠,𝑥,𝑦 𝑂,𝑟,𝑠,𝑥,𝑦 𝑃,𝑟,𝑠,𝑥,𝑦 𝑄,𝑠,𝑥,𝑦 𝑋,𝑟,𝑠,𝑥,𝑦 𝜑,𝑟,𝑠,𝑦 Allowed substitution hints: 𝜑(𝑥) ∥ (𝑥) 𝑃(𝑏) 𝑄(𝑟,𝑏) 𝐺(𝑏) 𝑂(𝑏)

Proof of Theorem prlngmolem2 Dummy variables 𝑐 𝑡 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		anass 473	. . . . . 6 ⊢ (((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) ↔ (𝐴 ∥ 𝑏 ∧ (𝑋 ∈ 𝑏 ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐))))
2		prlngeu.l	. . . . . . . . . . 11 ⊢ 𝐿 = (LineG‘𝐺)
3		prlngeu.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
4	3	ad6antr 748	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝐺 ∈ TarskiG)
5		prlngeu.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
6	5	ad6antr 748	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝐴 ∈ ran 𝐿)
7	2, 4, 6	tglnne0 28895	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝐴 ≠ ∅)
8		simpr 489	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 = 𝑐) → 𝑏 = 𝑐)
9		prlngeu.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
10	9	ad8antr 752	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝐺 ∈ TarskiG_E)
11		prlngeu.p	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (Base‘𝐺)
12		prlngeu.r	. . . . . . . . . . . . . . 15 ⊢ ∥ = (parlnG‘𝐺)
13	4	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝐺 ∈ TarskiG)
14	13	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐺 ∈ TarskiG)
15	6	ad5antr 746	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐴 ∈ ran 𝐿)
16		prlngeu.x	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))
17	16	ad8antr 752	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑋 ∈ (𝑃 ∖ 𝐴))
18	17	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑋 ∈ (𝑃 ∖ 𝐴))
19		prlngmolem2.1	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝑏) ∧ 𝑦 ∈ (𝑃 ∖ 𝑏)) ∧ ∃𝑟 ∈ 𝑏 𝑟 ∈ (𝑥(Itv‘𝐺)𝑦))}
20		prlngmolem2.2	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝐴) ∧ 𝑦 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑠 ∈ 𝐴 𝑠 ∈ (𝑥(Itv‘𝐺)𝑦))}
21		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
22		simp-8r 803	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ∈ ran 𝐿)
23	22	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑏 ∈ ran 𝐿)
24		simp-7r 801	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ∈ ran 𝐿)
25	24	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑐 ∈ ran 𝐿)
26		simp-9r 805	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐴 ∥ 𝑏)
27		simp-7r 801	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐴 ∥ 𝑐)
28		simp-8r 803	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑋 ∈ 𝑏)
29		simpllr 787	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑋 ∈ 𝑐)
30	29	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑋 ∈ 𝑐)
31		simp-5r 797	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑡 ∈ 𝐴)
32		simpllr 787	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
33		simp-4r 795	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑏 ≠ 𝑐)
34		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑤𝑂𝑡)
35	11, 2, 12, 14, 15, 18, 19, 20, 21, 23, 25, 26, 27, 28, 30, 31, 32, 33, 34	prlngmolem1 29183	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
36	13	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐺 ∈ TarskiG)
37	6	ad5antr 746	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐴 ∈ ran 𝐿)
38	17	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑋 ∈ (𝑃 ∖ 𝐴))
39	22	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑏 ∈ ran 𝐿)
40	24	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑐 ∈ ran 𝐿)
41		simp-9r 805	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐴 ∥ 𝑏)
42		simp-7r 801	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐴 ∥ 𝑐)
43		simp-8r 803	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑋 ∈ 𝑏)
44	29	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑋 ∈ 𝑐)
45		simp-5r 797	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑡 ∈ 𝐴)
46		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘𝐺) = (dist‘𝐺)
47		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
48		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
49		simplr 780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑐 ∖ 𝑏))
50	49	eldifad 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑐)
51	50	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ 𝑐)
52	11, 46, 21, 2, 47, 36, 48, 40, 44, 51	mirln 28934	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑐)
53		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
54	53	eldifbd 3919	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝑤 ∈ 𝑏)
55	36	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝐺 ∈ TarskiG)
56	11, 2, 21, 13, 24, 29	tglnpt 28799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑋 ∈ 𝑃)
57	56	ad4antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑋 ∈ 𝑃)
58	13	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐺 ∈ TarskiG)
59	24	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ∈ ran 𝐿)
60	11, 2, 21, 58, 59, 50	tglnpt 28799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑃)
61	60	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑃)
62	11, 46, 21, 2, 47, 55, 57, 48, 61	mirmir 28920	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) = 𝑤)
63	39	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑏 ∈ ran 𝐿)
64	43	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑋 ∈ 𝑏)
65		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
66	11, 46, 21, 2, 47, 55, 48, 63, 64, 65	mirln 28934	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) ∈ 𝑏)
67	62, 66	eqeltrrd 2864	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑏)
68	54, 67	mtand 827	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
69	52, 68	eldifd 3917	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ (𝑐 ∖ 𝑏))
70		simp-4r 795	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑏 ≠ 𝑐)
71		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡)
72	11, 2, 12, 36, 37, 38, 19, 20, 21, 39, 40, 41, 42, 43, 44, 45, 69, 70, 71	prlngmolem1 29183	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
73		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
74	22	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ∈ ran 𝐿)
75	49	eldifbd 3919	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑤 ∈ 𝑏)
76	60, 75	eldifd 3917	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑃 ∖ 𝑏))
77	6	ad4antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∈ ran 𝐿)
78	16	ad10antr 756	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ (𝑃 ∖ 𝐴))
79	11, 21, 2, 73, 58, 77, 78	elplnglnid 29046	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ⊆ (𝐴(hlG‘𝐺)𝑋))
80		simp-4r 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ 𝐴)
81	79, 80	sseldd 3939	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝐴(hlG‘𝐺)𝑋))
82	11, 2, 73, 58, 77, 78	tgelrnpln 29039	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) ∈ ran (hlG‘𝐺))
83		simp-6r 799	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑐)
84	29	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑐)
85	16	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴)
86	85	ad10antr 756	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑋 ∈ 𝐴)
87		nelne1 3055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ 𝑐 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑐 ≠ 𝐴)
88	84, 86, 87	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ≠ 𝐴)
89	88	necomd 3013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑐)
90	2, 73, 12, 58, 83, 89, 50, 84	prlnghpg 29177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤((hpG‘𝐺)‘𝐴)𝑋)
91	11, 2, 73, 77, 60, 78, 58, 90	hpgssplng 29059	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝐴(hlG‘𝐺)𝑋))
92	91, 75	eldifd 3917	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ ((𝐴(hlG‘𝐺)𝑋) ∖ 𝑏))
93		simp-8r 803	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑏)
94		simp-7r 801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑏)
95		nelne1 3055	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ 𝑏 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑏 ≠ 𝐴)
96	94, 86, 95	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ≠ 𝐴)
97	96	necomd 3013	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑏)
98	2, 73, 12, 58, 93, 97, 94	prlngpln3 29180	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ⊆ (𝐴(hlG‘𝐺)𝑋))
99	11, 2, 73, 58, 82, 74, 92, 98	plng3p 29060	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) = (𝑏(hlG‘𝐺)𝑤))
100	81, 99	eleqtrd 2865	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝑏(hlG‘𝐺)𝑤))
101	2, 12, 58, 93, 97	prlngin0 29175	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴 ∩ 𝑏) = ∅)
102	101	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) = ∅)
103		simp-5r 797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ 𝐴)
104		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ 𝑏)
105	103, 104	elind 4154	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ (𝐴 ∩ 𝑏))
106	105	ne0d 4296	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) ≠ ∅)
107	106	neneqd 2963	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → ¬ (𝐴 ∩ 𝑏) = ∅)
108	102, 107	pm2.65da 828	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑡 ∈ 𝑏)
109	100, 108	eldifd 3917	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ ((𝑏(hlG‘𝐺)𝑤) ∖ 𝑏))
110	11, 21, 2, 73, 47, 48, 19, 58, 74, 76, 109, 94	plngmiropp 29057	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝑤𝑂𝑡 ∨ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡))
111	35, 72, 110	mpjaodan 973	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝐺 ∈ TarskiG_E)
112		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ≠ 𝑐)
113	112	necomd 3013	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ≠ 𝑏)
114	11, 21, 2, 13, 24, 22, 29, 113	tglnpt4 28909	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ∃𝑤 ∈ (𝑐 ∖ 𝑏)𝑤 ≠ 𝑋)
115	111, 114	r19.29a 3173	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ¬ 𝐺 ∈ TarskiG_E)
116	10, 115	pm2.21dd 198	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 = 𝑐)
117	8, 116	pm2.61dane 3045	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) → 𝑏 = 𝑐)
118	7, 117	n0limd 4309	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝑏 = 𝑐)
119	118	anasss 471	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐)
120	119	anasss 471	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ (𝑋 ∈ 𝑏 ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐))) → 𝑏 = 𝑐)
121	120	anasss 471	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ (𝐴 ∥ 𝑏 ∧ (𝑋 ∈ 𝑏 ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))) → 𝑏 = 𝑐)
122	1, 121	sylan2b 605	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐))) → 𝑏 = 𝑐)
123	122	ex 417	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) → (((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
124	123	ralrimiva 3157	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐿) → ∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
125	124	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
126		breq2 5114	. . . 4 ⊢ (𝑏 = 𝑐 → (𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝑐))
127		eleq2w 2847	. . . 4 ⊢ (𝑏 = 𝑐 → (𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝑐))
128	126, 127	anbi12d 643	. . 3 ⊢ (𝑏 = 𝑐 → ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))
129	128	rmo4 3694	. 2 ⊢ (∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
130	125, 129	sylibr 237	1 ⊢ (𝜑 → ∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 ∃*wrmo 3368 ∖ cdif 3903 ∩ cin 3905 ∅c0 4287 class class class wbr 5110 {copab 5174 ran crn 5664 ‘cfv 6538 (class class class)co 7412 Basecbs 17270 distcds 17320 TarskiGcstrkg 28677 TarskiG_Ecstrkge 28682 Itvcitv 28683 LineGclng 28684 pInvGcmir 28910 hlGcplng 29036 parlnGcprlng 29167

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-tp 4595 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-oadd 8458 df-er 8695 df-map 8827 df-pm 8828 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-dju 9888 df-card 9926 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-nn 12235 df-2 12304 df-3 12305 df-n0 12506 df-xnn0 12579 df-z 12593 df-uz 12864 df-fz 13537 df-fzo 13685 df-hash 14369 df-word 14553 df-concat 14610 df-s1 14636 df-s2 14887 df-s3 14888 df-trkgc 28698 df-trkgb 28699 df-trkgcb 28700 df-trkge 28701 df-trkgld 28702 df-trkg 28703 df-cgrg 28761 df-leg 28833 df-hlg 28851 df-mir 28911 df-rag 28955 df-perpg 28957 df-hpg 29021 df-plng 29037 df-prlng 29168

This theorem is referenced by: prlngmo 29185

W3C validator