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 29318

Description: Lemma for prlngmo 29319. (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 474	. . . . . 6 ⊢ (((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) ↔ (𝐴 ∥ 𝑏 ∧ (𝑋 ∈ 𝑏 ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐))))
2		prlngeu.l	. . . . . . . . . . 11 ⊢ 𝐿 = (LineG‘𝐺)
3		prlngeu.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
4	3	ad6antr 749	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝐺 ∈ TarskiG)
5		prlngeu.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
6	5	ad6antr 749	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝐴 ∈ ran 𝐿)
7	2, 4, 6	tglnne0 28996	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝐴 ≠ ∅)
8		simpr 490	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 = 𝑐) → 𝑏 = 𝑐)
9		prlngeu.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
10	9	ad8antr 753	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝐺 ∈ TarskiG_E)
11		prlngeu.p	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (Base‘𝐺)
12		prlngeu.r	. . . . . . . . . . . . . . 15 ⊢ ∥ = (parlnG‘𝐺)
13	4	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝐺 ∈ TarskiG)
14	13	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐺 ∈ TarskiG)
15	6	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐴 ∈ ran 𝐿)
16		prlngeu.x	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ 𝐴))
17	16	ad8antr 753	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑋 ∈ (𝑃 ∖ 𝐴))
18	17	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑋 ∈ (𝑃 ∖ 𝐴))
19		prlngmolem2.1	. . . . . . . . . . . . . . 15 ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝑏) ∧ 𝑦 ∈ (𝑃 ∖ 𝑏)) ∧ ∃𝑟 ∈ 𝑏 𝑟 ∈ (𝑥(Itv‘𝐺)𝑦))}
20		prlngmolem2.2	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑃 ∖ 𝐴) ∧ 𝑦 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑠 ∈ 𝐴 𝑠 ∈ (𝑥(Itv‘𝐺)𝑦))}
21		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
22		simp-8r 804	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ∈ ran 𝐿)
23	22	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑏 ∈ ran 𝐿)
24		simp-7r 802	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ∈ ran 𝐿)
25	24	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑐 ∈ ran 𝐿)
26		simp-9r 806	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐴 ∥ 𝑏)
27		simp-7r 802	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝐴 ∥ 𝑐)
28		simp-8r 804	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑋 ∈ 𝑏)
29		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑋 ∈ 𝑐)
30	29	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑋 ∈ 𝑐)
31		simp-5r 798	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑡 ∈ 𝐴)
32		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
33		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑏 ≠ 𝑐)
34		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → 𝑤𝑂𝑡)
35	11, 2, 12, 14, 15, 18, 19, 20, 21, 23, 25, 26, 27, 28, 30, 31, 32, 33, 34	prlngmolem1 29317	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑤𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
36	13	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐺 ∈ TarskiG)
37	6	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐴 ∈ ran 𝐿)
38	17	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑋 ∈ (𝑃 ∖ 𝐴))
39	22	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑏 ∈ ran 𝐿)
40	24	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑐 ∈ ran 𝐿)
41		simp-9r 806	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐴 ∥ 𝑏)
42		simp-7r 802	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝐴 ∥ 𝑐)
43		simp-8r 804	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑋 ∈ 𝑏)
44	29	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑋 ∈ 𝑐)
45		simp-5r 798	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑡 ∈ 𝐴)
46		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘𝐺) = (dist‘𝐺)
47		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
48		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
49		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑐 ∖ 𝑏))
50	49	eldifad 3914	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑐)
51	50	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ 𝑐)
52	11, 46, 21, 2, 47, 36, 48, 40, 44, 51	mirln 29035	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑐)
53		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
54	53	eldifbd 3915	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝑤 ∈ 𝑏)
55	36	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝐺 ∈ TarskiG)
56	11, 2, 21, 13, 24, 29	tglnpt 28899	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑋 ∈ 𝑃)
57	56	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑋 ∈ 𝑃)
58	13	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐺 ∈ TarskiG)
59	24	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ∈ ran 𝐿)
60	11, 2, 21, 58, 59, 50	tglnpt 28899	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑃)
61	60	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑃)
62	11, 46, 21, 2, 47, 55, 57, 48, 61	mirmir 29021	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) = 𝑤)
63	39	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑏 ∈ ran 𝐿)
64	43	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑋 ∈ 𝑏)
65		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
66	11, 46, 21, 2, 47, 55, 48, 63, 64, 65	mirln 29035	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) ∈ 𝑏)
67	62, 66	eqeltrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑏)
68	54, 67	mtand 828	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
69	52, 68	eldifd 3913	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ (𝑐 ∖ 𝑏))
70		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑏 ≠ 𝑐)
71		simpr 490	. . . . . . . . . . . . . . 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 29317	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
73		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
74	22	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ∈ ran 𝐿)
75	49	eldifbd 3915	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑤 ∈ 𝑏)
76	60, 75	eldifd 3913	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑃 ∖ 𝑏))
77	6	ad4antr 745	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∈ ran 𝐿)
78	16	ad10antr 757	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ (𝑃 ∖ 𝐴))
79	11, 21, 2, 73, 58, 77, 78	elplnglnid 29148	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ⊆ (𝐴(hlG‘𝐺)𝑋))
80		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ 𝐴)
81	79, 80	sseldd 3935	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝐴(hlG‘𝐺)𝑋))
82	11, 2, 73, 58, 77, 78	tgelrnpln 29141	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) ∈ ran (hlG‘𝐺))
83		simp-6r 800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑐)
84	29	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑐)
85	16	eldifbd 3915	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴)
86	85	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑋 ∈ 𝐴)
87		nelne1 3054	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ 𝑐 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑐 ≠ 𝐴)
88	84, 86, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ≠ 𝐴)
89	88	necomd 3012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑐)
90	2, 73, 12, 58, 83, 89, 50, 84	prlnghpg 29311	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤((hpG‘𝐺)‘𝐴)𝑋)
91	11, 2, 73, 77, 60, 78, 58, 90	hpgssplng 29161	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝐴(hlG‘𝐺)𝑋))
92	91, 75	eldifd 3913	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ ((𝐴(hlG‘𝐺)𝑋) ∖ 𝑏))
93		simp-8r 804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑏)
94		simp-7r 802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑏)
95		nelne1 3054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ 𝑏 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑏 ≠ 𝐴)
96	94, 86, 95	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ≠ 𝐴)
97	96	necomd 3012	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑏)
98	2, 73, 12, 58, 93, 97, 94	prlngpln3 29314	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ⊆ (𝐴(hlG‘𝐺)𝑋))
99	11, 2, 73, 58, 82, 74, 92, 98	plng3p 29162	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) = (𝑏(hlG‘𝐺)𝑤))
100	81, 99	eleqtrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝑏(hlG‘𝐺)𝑤))
101	2, 12, 58, 93, 97	prlngin0 29309	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴 ∩ 𝑏) = ∅)
102	101	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) = ∅)
103		simp-5r 798	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ 𝐴)
104		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ 𝑏)
105	103, 104	elind 4149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ (𝐴 ∩ 𝑏))
106	105	ne0d 4291	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) ≠ ∅)
107	106	neneqd 2962	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → ¬ (𝐴 ∩ 𝑏) = ∅)
108	102, 107	pm2.65da 829	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑡 ∈ 𝑏)
109	100, 108	eldifd 3913	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ ((𝑏(hlG‘𝐺)𝑤) ∖ 𝑏))
110	11, 21, 2, 73, 47, 48, 19, 58, 74, 76, 109, 94	plngmiropp 29159	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝑤𝑂𝑡 ∨ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡))
111	35, 72, 110	mpjaodan 973	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝐺 ∈ TarskiG_E)
112		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ≠ 𝑐)
113	112	necomd 3012	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ≠ 𝑏)
114	11, 21, 2, 13, 24, 22, 29, 113	tglnpt4 29010	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ∃𝑤 ∈ (𝑐 ∖ 𝑏)𝑤 ≠ 𝑋)
115	111, 114	r19.29a 3172	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ¬ 𝐺 ∈ TarskiG_E)
116	10, 115	pm2.21dd 198	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 = 𝑐)
117	8, 116	pm2.61dane 3044	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) → 𝑏 = 𝑐)
118	7, 117	n0limd 4304	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) → 𝑏 = 𝑐)
119	118	anasss 472	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐)
120	119	anasss 472	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ (𝑋 ∈ 𝑏 ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐))) → 𝑏 = 𝑐)
121	120	anasss 472	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ (𝐴 ∥ 𝑏 ∧ (𝑋 ∈ 𝑏 ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))) → 𝑏 = 𝑐)
122	1, 121	sylan2b 606	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐))) → 𝑏 = 𝑐)
123	122	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) → (((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
124	123	ralrimiva 3156	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐿) → ∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
125	124	ralrimiva 3156	. 2 ⊢ (𝜑 → ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
126		breq2 5111	. . . 4 ⊢ (𝑏 = 𝑐 → (𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝑐))
127		eleq2w 2846	. . . 4 ⊢ (𝑏 = 𝑐 → (𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝑐))
128	126, 127	anbi12d 644	. . 3 ⊢ (𝑏 = 𝑐 → ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))
129	128	rmo4 3691	. 2 ⊢ (∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
130	125, 129	sylibr 237	1 ⊢ (𝜑 → ∃*𝑏 ∈ ran 𝐿(𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ∃*wrmo 3366 ∖ cdif 3899 ∩ cin 3901 ∅c0 4282 class class class wbr 5107 {copab 5171 ran crn 5660 ‘cfv 6537 (class class class)co 7417 Basecbs 17307 distcds 17357 TarskiGcstrkg 28776 TarskiG_Ecstrkge 28781 Itvcitv 28782 LineGclng 28783 pInvGcmir 29011 hlGcplng 29138 parlnGcprlng 29301

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 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-oadd 8463 df-er 8700 df-map 8832 df-pm 8833 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-dju 9910 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-3 12332 df-n0 12533 df-xnn0 12606 df-z 12620 df-uz 12892 df-fz 13566 df-fzo 13714 df-hash 14399 df-word 14583 df-concat 14640 df-s1 14667 df-s2 14923 df-s3 14924 df-trkgc 28797 df-trkgb 28798 df-trkgcb 28799 df-trkge 28800 df-trkgld 28801 df-trkg 28802 df-cgrg 28861 df-leg 28933 df-hlg 28951 df-mir 29012 df-rag 29056 df-perpg 29058 df-hpg 29123 df-plng 29139 df-prlng 29302

This theorem is used by: prlngmo 29319

W3C validator