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 29232

Description: Lemma for prlngmo 29233. (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 28943	. . . . . . . . . 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 2765	. . . . . . . . . . . . . . 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 29231	. . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘𝐺) = (dist‘𝐺)
47		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
48		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
49		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑐 ∖ 𝑏))
50	49	eldifad 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑐)
51	50	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ 𝑐)
52	11, 46, 21, 2, 47, 36, 48, 40, 44, 51	mirln 28982	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑐)
53		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
54	53	eldifbd 3919	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝑤 ∈ 𝑏)
55	36	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝐺 ∈ TarskiG)
56	11, 2, 21, 13, 24, 29	tglnpt 28847	. . . . . . . . . . . . . . . . . . . 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 28847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑃)
61	60	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑃)
62	11, 46, 21, 2, 47, 55, 57, 48, 61	mirmir 28968	. . . . . . . . . . . . . . . . . 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 28982	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) ∈ 𝑏)
67	62, 66	eqeltrrd 2866	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑏)
68	54, 67	mtand 828	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
69	52, 68	eldifd 3917	. . . . . . . . . . . . . . 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 29231	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
73		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
74	22	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ∈ ran 𝐿)
75	49	eldifbd 3919	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑤 ∈ 𝑏)
76	60, 75	eldifd 3917	. . . . . . . . . . . . . . 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 29094	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ⊆ (𝐴(hlG‘𝐺)𝑋))
80		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ 𝐴)
81	79, 80	sseldd 3939	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝐴(hlG‘𝐺)𝑋))
82	11, 2, 73, 58, 77, 78	tgelrnpln 29087	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) ∈ ran (hlG‘𝐺))
83		simp-6r 800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑐)
84	29	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑐)
85	16	eldifbd 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴)
86	85	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑋 ∈ 𝐴)
87		nelne1 3057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ 𝑐 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑐 ≠ 𝐴)
88	84, 86, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ≠ 𝐴)
89	88	necomd 3015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑐)
90	2, 73, 12, 58, 83, 89, 50, 84	prlnghpg 29225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤((hpG‘𝐺)‘𝐴)𝑋)
91	11, 2, 73, 77, 60, 78, 58, 90	hpgssplng 29107	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝐴(hlG‘𝐺)𝑋))
92	91, 75	eldifd 3917	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ ((𝐴(hlG‘𝐺)𝑋) ∖ 𝑏))
93		simp-8r 804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑏)
94		simp-7r 802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑏)
95		nelne1 3057	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ 𝑏 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑏 ≠ 𝐴)
96	94, 86, 95	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ≠ 𝐴)
97	96	necomd 3015	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑏)
98	2, 73, 12, 58, 93, 97, 94	prlngpln3 29228	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ⊆ (𝐴(hlG‘𝐺)𝑋))
99	11, 2, 73, 58, 82, 74, 92, 98	plng3p 29108	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) = (𝑏(hlG‘𝐺)𝑤))
100	81, 99	eleqtrd 2867	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝑏(hlG‘𝐺)𝑤))
101	2, 12, 58, 93, 97	prlngin0 29223	. . . . . . . . . . . . . . . . . 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 4153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ (𝐴 ∩ 𝑏))
106	105	ne0d 4295	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) ≠ ∅)
107	106	neneqd 2965	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → ¬ (𝐴 ∩ 𝑏) = ∅)
108	102, 107	pm2.65da 829	. . . . . . . . . . . . . . . 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 29105	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝑤𝑂𝑡 ∨ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡))
111	35, 72, 110	mpjaodan 973	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝐺 ∈ TarskiG_E)
112		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ≠ 𝑐)
113	112	necomd 3015	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ≠ 𝑏)
114	11, 21, 2, 13, 24, 22, 29, 113	tglnpt4 28957	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ∃𝑤 ∈ (𝑐 ∖ 𝑏)𝑤 ≠ 𝑋)
115	111, 114	r19.29a 3175	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ¬ 𝐺 ∈ TarskiG_E)
116	10, 115	pm2.21dd 198	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 = 𝑐)
117	8, 116	pm2.61dane 3047	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) → 𝑏 = 𝑐)
118	7, 117	n0limd 4308	. . . . . . . . 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 3159	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐿) → ∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
125	124	ralrimiva 3159	. 2 ⊢ (𝜑 → ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
126		breq2 5115	. . . 4 ⊢ (𝑏 = 𝑐 → (𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝑐))
127		eleq2w 2849	. . . 4 ⊢ (𝑏 = 𝑐 → (𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝑐))
128	126, 127	anbi12d 644	. . 3 ⊢ (𝑏 = 𝑐 → ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))
129	128	rmo4 3695	. 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 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 ∃*wrmo 3370 ∖ cdif 3903 ∩ cin 3905 ∅c0 4286 class class class wbr 5111 {copab 5175 ran crn 5664 ‘cfv 6540 (class class class)co 7416 Basecbs 17286 distcds 17336 TarskiGcstrkg 28725 TarskiG_Ecstrkge 28730 Itvcitv 28731 LineGclng 28732 pInvGcmir 28958 hlGcplng 29084 parlnGcprlng 29215

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 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 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7865 df-1st 7988 df-2nd 7989 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 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-dju 9899 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-nn 12245 df-2 12314 df-3 12315 df-n0 12516 df-xnn0 12589 df-z 12603 df-uz 12874 df-fz 13547 df-fzo 13695 df-hash 14380 df-word 14564 df-concat 14621 df-s1 14648 df-s2 14904 df-s3 14905 df-trkgc 28746 df-trkgb 28747 df-trkgcb 28748 df-trkge 28749 df-trkgld 28750 df-trkg 28751 df-cgrg 28809 df-leg 28881 df-hlg 28899 df-mir 28959 df-rag 29003 df-perpg 29005 df-hpg 29069 df-plng 29085 df-prlng 29216

This theorem is used by: prlngmo 29233

W3C validator