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 29424

Description: Lemma for prlngmo 29425. (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 29102	. . . . . . . . . 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 2761	. . . . . . . . . . . . . . 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 29423	. . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘𝐺) = (dist‘𝐺)
47		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
48		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
49		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑐 ∖ 𝑏))
50	49	eldifad 3911	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑐)
51	50	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ 𝑐)
52	11, 46, 21, 2, 47, 36, 48, 40, 44, 51	mirln 29141	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑐)
53		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
54	53	eldifbd 3912	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝑤 ∈ 𝑏)
55	36	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝐺 ∈ TarskiG)
56	11, 2, 21, 13, 24, 29	tglnpt 29005	. . . . . . . . . . . . . . . . . . . 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 29005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑃)
61	60	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑃)
62	11, 46, 21, 2, 47, 55, 57, 48, 61	mirmir 29127	. . . . . . . . . . . . . . . . . 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 29141	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) ∈ 𝑏)
67	62, 66	eqeltrrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑏)
68	54, 67	mtand 828	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
69	52, 68	eldifd 3910	. . . . . . . . . . . . . . 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 29423	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
73		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
74	22	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ∈ ran 𝐿)
75	49	eldifbd 3912	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑤 ∈ 𝑏)
76	60, 75	eldifd 3910	. . . . . . . . . . . . . . 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 29254	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ⊆ (𝐴(hlG‘𝐺)𝑋))
80		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ 𝐴)
81	79, 80	sseldd 3932	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝐴(hlG‘𝐺)𝑋))
82	11, 2, 73, 58, 77, 78	tgelrnpln 29247	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) ∈ ran (hlG‘𝐺))
83		simp-6r 800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑐)
84	29	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑐)
85	16	eldifbd 3912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴)
86	85	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑋 ∈ 𝐴)
87		nelne1 3053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ 𝑐 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑐 ≠ 𝐴)
88	84, 86, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ≠ 𝐴)
89	88	necomd 3011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑐)
90	2, 73, 12, 58, 83, 89, 50, 84	prlnghpg 29417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤((hpG‘𝐺)‘𝐴)𝑋)
91	11, 2, 73, 77, 60, 78, 58, 90	hpgssplng 29267	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝐴(hlG‘𝐺)𝑋))
92	91, 75	eldifd 3910	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ ((𝐴(hlG‘𝐺)𝑋) ∖ 𝑏))
93		simp-8r 804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑏)
94		simp-7r 802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑏)
95		nelne1 3053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ 𝑏 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑏 ≠ 𝐴)
96	94, 86, 95	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ≠ 𝐴)
97	96	necomd 3011	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑏)
98	2, 73, 12, 58, 93, 97, 94	prlngpln3 29420	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ⊆ (𝐴(hlG‘𝐺)𝑋))
99	11, 2, 73, 58, 82, 74, 92, 98	plng3p 29268	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) = (𝑏(hlG‘𝐺)𝑤))
100	81, 99	eleqtrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝑏(hlG‘𝐺)𝑤))
101	2, 12, 58, 93, 97	prlngin0 29415	. . . . . . . . . . . . . . . . . 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 4146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ (𝐴 ∩ 𝑏))
106	105	ne0d 4288	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) ≠ ∅)
107	106	neneqd 2961	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → ¬ (𝐴 ∩ 𝑏) = ∅)
108	102, 107	pm2.65da 829	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑡 ∈ 𝑏)
109	100, 108	eldifd 3910	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ ((𝑏(hlG‘𝐺)𝑤) ∖ 𝑏))
110	11, 21, 2, 73, 47, 48, 19, 58, 74, 76, 109, 94	plngmiropp 29265	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝑤𝑂𝑡 ∨ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡))
111	35, 72, 110	mpjaodan 973	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝐺 ∈ TarskiG_E)
112		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ≠ 𝑐)
113	112	necomd 3011	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ≠ 𝑏)
114	11, 21, 2, 13, 24, 22, 29, 113	tglnpt4 29116	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ∃𝑤 ∈ (𝑐 ∖ 𝑏)𝑤 ≠ 𝑋)
115	111, 114	r19.29a 3171	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ¬ 𝐺 ∈ TarskiG_E)
116	10, 115	pm2.21dd 198	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 = 𝑐)
117	8, 116	pm2.61dane 3043	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) → 𝑏 = 𝑐)
118	7, 117	n0limd 4301	. . . . . . . . 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 3155	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐿) → ∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
125	124	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
126		breq2 5107	. . . 4 ⊢ (𝑏 = 𝑐 → (𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝑐))
127		eleq2w 2845	. . . 4 ⊢ (𝑏 = 𝑐 → (𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝑐))
128	126, 127	anbi12d 644	. . 3 ⊢ (𝑏 = 𝑐 → ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))
129	128	rmo4 3688	. 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 2956 ∀wral 3077 ∃wrex 3087 ∃*wrmo 3365 ∖ cdif 3896 ∩ cin 3898 ∅c0 4279 class class class wbr 5103 {copab 5167 ran crn 5652 ‘cfv 6537 (class class class)co 7418 Basecbs 17380 distcds 17430 TarskiGcstrkg 28882 TarskiG_Ecstrkge 28887 Itvcitv 28888 LineGclng 28889 pInvGcmir 29117 hlGcplng 29244 parlnGcprlng 29407

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 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 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 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-oadd 8473 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-xnn0 12673 df-z 12687 df-uz 12959 df-fz 13633 df-fzo 13782 df-hash 14468 df-word 14652 df-concat 14709 df-s1 14736 df-s2 14992 df-s3 14993 df-trkgc 28903 df-trkgb 28904 df-trkgcb 28905 df-trkge 28906 df-trkgld 28907 df-trkg 28908 df-cgrg 28967 df-leg 29039 df-hlg 29057 df-mir 29118 df-rag 29162 df-perpg 29164 df-hpg 29229 df-plng 29245 df-prlng 29408

This theorem is used by: prlngmo 29425

W3C validator