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 29437

Description: Lemma for prlngmo 29438. (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 29115	. . . . . . . . . 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 2760	. . . . . . . . . . . . . . 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 29436	. . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . . . 17 ⊢ (dist‘𝐺) = (dist‘𝐺)
47		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
48		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
49		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝑐 ∖ 𝑏))
50	49	eldifad 4051	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑐)
51	50	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ 𝑐)
52	11, 46, 21, 2, 47, 36, 48, 40, 44, 51	mirln 29154	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑐)
53		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → 𝑤 ∈ (𝑐 ∖ 𝑏))
54	53	eldifbd 4052	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝑤 ∈ 𝑏)
55	36	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝐺 ∈ TarskiG)
56	11, 2, 21, 13, 24, 29	tglnpt 29018	. . . . . . . . . . . . . . . . . . . 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 29018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ 𝑃)
61	60	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑃)
62	11, 46, 21, 2, 47, 55, 57, 48, 61	mirmir 29140	. . . . . . . . . . . . . . . . . 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 29154	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → (((pInvG‘𝐺)‘𝑋)‘(((pInvG‘𝐺)‘𝑋)‘𝑤)) ∈ 𝑏)
67	62, 66	eqeltrrd 2861	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏) → 𝑤 ∈ 𝑏)
68	54, 67	mtand 828	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ (((pInvG‘𝐺)‘𝑋)‘𝑤) ∈ 𝑏)
69	52, 68	eldifd 4050	. . . . . . . . . . . . . . 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 29436	. . . . . . . . . . . . . 14 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡) → ¬ 𝐺 ∈ TarskiG_E)
73		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
74	22	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ∈ ran 𝐿)
75	49	eldifbd 4052	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑤 ∈ 𝑏)
76	60, 75	eldifd 4050	. . . . . . . . . . . . . . 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 29267	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ⊆ (𝐴(hlG‘𝐺)𝑋))
80		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ 𝐴)
81	79, 80	sseldd 3909	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝐴(hlG‘𝐺)𝑋))
82	11, 2, 73, 58, 77, 78	tgelrnpln 29260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) ∈ ran (hlG‘𝐺))
83		simp-6r 800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑐)
84	29	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑐)
85	16	eldifbd 4052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴)
86	85	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑋 ∈ 𝐴)
87		nelne1 3052	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ 𝑐 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑐 ≠ 𝐴)
88	84, 86, 87	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑐 ≠ 𝐴)
89	88	necomd 3010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑐)
90	2, 73, 12, 58, 83, 89, 50, 84	prlnghpg 29430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤((hpG‘𝐺)‘𝐴)𝑋)
91	11, 2, 73, 77, 60, 78, 58, 90	hpgssplng 29280	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ (𝐴(hlG‘𝐺)𝑋))
92	91, 75	eldifd 4050	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑤 ∈ ((𝐴(hlG‘𝐺)𝑋) ∖ 𝑏))
93		simp-8r 804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ∥ 𝑏)
94		simp-7r 802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑋 ∈ 𝑏)
95		nelne1 3052	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ 𝑏 ∧ ¬ 𝑋 ∈ 𝐴) → 𝑏 ≠ 𝐴)
96	94, 86, 95	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ≠ 𝐴)
97	96	necomd 3010	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝐴 ≠ 𝑏)
98	2, 73, 12, 58, 93, 97, 94	prlngpln3 29433	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑏 ⊆ (𝐴(hlG‘𝐺)𝑋))
99	11, 2, 73, 58, 82, 74, 92, 98	plng3p 29281	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝐴(hlG‘𝐺)𝑋) = (𝑏(hlG‘𝐺)𝑤))
100	81, 99	eleqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ (𝑏(hlG‘𝐺)𝑤))
101	2, 12, 58, 93, 97	prlngin0 29428	. . . . . . . . . . . . . . . . . 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 4097	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → 𝑡 ∈ (𝐴 ∩ 𝑏))
106	105	ne0d 4287	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → (𝐴 ∩ 𝑏) ≠ ∅)
107	106	neneqd 2960	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) ∧ 𝑡 ∈ 𝑏) → ¬ (𝐴 ∩ 𝑏) = ∅)
108	102, 107	pm2.65da 829	. . . . . . . . . . . . . . . 16 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝑡 ∈ 𝑏)
109	100, 108	eldifd 4050	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → 𝑡 ∈ ((𝑏(hlG‘𝐺)𝑤) ∖ 𝑏))
110	11, 21, 2, 73, 47, 48, 19, 58, 74, 76, 109, 94	plngmiropp 29278	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → (𝑤𝑂𝑡 ∨ (((pInvG‘𝐺)‘𝑋)‘𝑤)𝑂𝑡))
111	35, 72, 110	mpjaodan 973	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) ∧ 𝑤 ∈ (𝑐 ∖ 𝑏)) ∧ 𝑤 ≠ 𝑋) → ¬ 𝐺 ∈ TarskiG_E)
112		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 ≠ 𝑐)
113	112	necomd 3010	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑐 ≠ 𝑏)
114	11, 21, 2, 13, 24, 22, 29, 113	tglnpt4 29129	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ∃𝑤 ∈ (𝑐 ∖ 𝑏)𝑤 ≠ 𝑋)
115	111, 114	r19.29a 3170	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → ¬ 𝐺 ∈ TarskiG_E)
116	10, 115	pm2.21dd 198	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) ∧ 𝑏 ≠ 𝑐) → 𝑏 = 𝑐)
117	8, 116	pm2.61dane 3042	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑏 ∈ ran 𝐿) ∧ 𝑐 ∈ ran 𝐿) ∧ 𝐴 ∥ 𝑏) ∧ 𝑋 ∈ 𝑏) ∧ 𝐴 ∥ 𝑐) ∧ 𝑋 ∈ 𝑐) ∧ 𝑡 ∈ 𝐴) → 𝑏 = 𝑐)
118	7, 117	n0limd 4300	. . . . . . . . 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 3154	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐿) → ∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
125	124	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑏 ∈ ran 𝐿∀𝑐 ∈ ran 𝐿(((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ∧ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)) → 𝑏 = 𝑐))
126		breq2 5106	. . . 4 ⊢ (𝑏 = 𝑐 → (𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝑐))
127		eleq2w 2844	. . . 4 ⊢ (𝑏 = 𝑐 → (𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝑐))
128	126, 127	anbi12d 644	. . 3 ⊢ (𝑏 = 𝑐 → ((𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏) ↔ (𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐)))
129	128	rmo4 3687	. 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 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ∃*wrmo 3364 ∖ cdif 4045 ∩ cin 4089 ∅c0 4278 class class class wbr 5102 {copab 5166 ran crn 5651 ‘cfv 6539 (class class class)co 7421 Basecbs 17393 distcds 17443 TarskiGcstrkg 28895 TarskiG_Ecstrkge 28900 Itvcitv 28901 LineGclng 28902 pInvGcmir 29130 hlGcplng 29257 parlnGcprlng 29420

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-oadd 8484 df-er 8721 df-map 8853 df-pm 8854 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-dju 9986 df-card 10024 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-2 12409 df-3 12410 df-n0 12611 df-xnn0 12684 df-z 12698 df-uz 12970 df-fz 13644 df-fzo 13793 df-hash 14479 df-word 14663 df-concat 14720 df-s1 14747 df-s2 15004 df-s3 15005 df-trkgc 28916 df-trkgb 28917 df-trkgcb 28918 df-trkge 28919 df-trkgld 28920 df-trkg 28921 df-cgrg 28980 df-leg 29052 df-hlg 29070 df-mir 29131 df-rag 29175 df-perpg 29177 df-hpg 29242 df-plng 29258 df-prlng 29421

This theorem is used by: prlngmo 29438

W3C validator