prlngex

Description: There exists at least one parallel line b to a given line A through a given point X . Theorem 12.10 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngeu.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	prlngeu.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngeu.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngeu.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	prlngeu.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	prlngex.6	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
Assertion	prlngex	⊢ ( 𝜑 → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		prlngeu.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		prlngeu.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		prlngeu.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		prlngeu.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		prlngex.6	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7		breq2	⊢ ( 𝑏 = 𝐴 → ( 𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝐴 ) )
8		eleq2	⊢ ( 𝑏 = 𝐴 → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝐴 ) )
9	7 8	anbi12d	⊢ ( 𝑏 = 𝐴 → ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ( 𝐴 ∥ 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ∈ ran 𝐿 )
11		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
13	2 11 3 12 10	prlngref	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ∥ 𝐴 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
15	13 14	jca	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∥ 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
16	9 10 15	rspcedvdw	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
17		breq2	⊢ ( 𝑏 = ( 𝑤 𝐿 𝑋 ) → ( 𝐴 ∥ 𝑏 ↔ 𝐴 ∥ ( 𝑤 𝐿 𝑋 ) ) )
18		eleq2	⊢ ( 𝑏 = ( 𝑤 𝐿 𝑋 ) → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ ( 𝑤 𝐿 𝑋 ) ) )
19	17 18	anbi12d	⊢ ( 𝑏 = ( 𝑤 𝐿 𝑋 ) → ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ( 𝐴 ∥ ( 𝑤 𝐿 𝑋 ) ∧ 𝑋 ∈ ( 𝑤 𝐿 𝑋 ) ) ) )
20	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
21	20	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝐺 ∈ TarskiG )
22	21	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝐺 ∈ TarskiG )
23	22	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝐺 ∈ TarskiG )
24		simplr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) )
25	2 23 24	perpln2	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑤 𝐿 𝑋 ) ∈ ran 𝐿 )
26	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐴 ∈ ran 𝐿 )
27	26	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝐴 ∈ ran 𝐿 )
28	27	ad5antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝐴 ∈ ran 𝐿 )
29	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝑃 )
30	29	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝑋 ∈ 𝑃 )
31		simpllr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ¬ 𝑋 ∈ 𝐴 )
32	30 31	eldifd	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
33	32	ad5antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
34	1 2 11 23 28 33	tgelrnpln	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) ∈ ran ( hlG ‘ 𝐺 ) )
35		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
36	1 35 2 11 23 28 33	elplnglnid	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝐴 ⊆ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
37		simplr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝑦 ∈ 𝐴 )
38	1 2 35 21 27 37	tglnpt	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝑦 ∈ 𝑃 )
39		nelne2	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑦 ≠ 𝑋 )
40	37 31 39	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝑦 ≠ 𝑋 )
41	40	necomd	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝑋 ≠ 𝑦 )
42	1 35 2 21 30 38 41	tgelrnln	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ( 𝑋 𝐿 𝑦 ) ∈ ran 𝐿 )
43	42	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → ( 𝑋 𝐿 𝑦 ) ∈ ran 𝐿 )
44	43	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑋 𝐿 𝑦 ) ∈ ran 𝐿 )
45		simpllr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑤 ∈ 𝑃 )
46	27	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝐴 ∈ ran 𝐿 )
47		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) )
48	47	eldifad	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑡 ∈ 𝐴 )
49	1 2 35 22 46 48	tglnpt	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑡 ∈ 𝑃 )
50	47	eldifbd	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → ¬ 𝑡 ∈ ( 𝑋 𝐿 𝑦 ) )
51	49 50	eldifd	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑡 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑦 ) ) )
52	51	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑡 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑦 ) ) )
53		simpr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 )
54	1 2 11 44 45 52 23 53	hpgssplng	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑤 ∈ ( ( 𝑋 𝐿 𝑦 ) ( hlG ‘ 𝐺 ) 𝑡 ) )
55	30	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑋 ∈ 𝑃 )
56	55	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑋 ∈ 𝑃 )
57	31	ad5antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ¬ 𝑋 ∈ 𝐴 )
58	49	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑡 ∈ 𝑃 )
59	38	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑦 ∈ 𝑃 )
60	59	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑦 ∈ 𝑃 )
61		simp-4r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑡 ≠ 𝑦 )
62	48	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑡 ∈ 𝐴 )
63	37	ad5antr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑦 ∈ 𝐴 )
64	1 35 2 23 58 60 61 61 28 62 63	tglinethru	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝐴 = ( 𝑡 𝐿 𝑦 ) )
65	57 64	neleqtrd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ¬ 𝑋 ∈ ( 𝑡 𝐿 𝑦 ) )
66	56 65	eldifd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑋 ∈ ( 𝑃 ∖ ( 𝑡 𝐿 𝑦 ) ) )
67	41	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑋 ≠ 𝑦 )
68	67	ad3antrrr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑋 ≠ 𝑦 )
69	1 35 2 11 23 66 60 52 68	plngrot	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( ( 𝑋 𝐿 𝑦 ) ( hlG ‘ 𝐺 ) 𝑡 ) = ( ( 𝑡 𝐿 𝑦 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
70	64	oveq1d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) = ( ( 𝑡 𝐿 𝑦 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
71	69 70	eqtr4d	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( ( 𝑋 𝐿 𝑦 ) ( hlG ‘ 𝐺 ) 𝑡 ) = ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
72	54 71	eleqtrd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑤 ∈ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
73	1 35 2 11 23 28 33	elplngid	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑋 ∈ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
74	1 35 2 23 45 56 25	tglnne	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑤 ≠ 𝑋 )
75	1 35 2 11 23 34 72 73 74	lnssplng1	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑤 𝐿 𝑋 ) ⊆ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
76	36 63	sseldd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑦 ∈ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
77	1 35 2 11 23 34 73 76 68	lnssplng1	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑋 𝐿 𝑦 ) ⊆ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
78		eqid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
79		simp-6r	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
80	1 78 35 2 23 44 28 79	perpcom	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝐴 ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑦 ) )
81	1 78 35 2 23 44 25 24	perpcom	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝑤 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑦 ) )
82	1 2 11 3 23 34 36 75 77 80 81	perpprlng	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝐴 ∥ ( 𝑤 𝐿 𝑋 ) )
83	1 35 2 23 45 56 74	tglinerflx2	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → 𝑋 ∈ ( 𝑤 𝐿 𝑋 ) )
84	82 83	jca	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ( 𝐴 ∥ ( 𝑤 𝐿 𝑋 ) ∧ 𝑋 ∈ ( 𝑤 𝐿 𝑋 ) ) )
85	19 25 84	rspcedvdw	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
86	85	anasss	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) ) → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
87	21	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
88	29	ad4antr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑋 ∈ 𝑃 )
89	38	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ 𝑃 )
90	27	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐴 ∈ ran 𝐿 )
91		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑧 ∈ 𝐴 )
92	1 2 35 87 90 91	tglnpt	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑧 ∈ 𝑃 )
93	42	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑋 𝐿 𝑦 ) ∈ ran 𝐿 )
94		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
95	1 78 35 2 87 93 90 94	perpneq	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑋 𝐿 𝑦 ) ≠ 𝐴 )
96	95	neneqd	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ¬ ( 𝑋 𝐿 𝑦 ) = 𝐴 )
97	87	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝐺 ∈ TarskiG )
98	92	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑧 ∈ 𝑃 )
99	89	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑦 ∈ 𝑃 )
100		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑦 ≠ 𝑧 )
101	100	necomd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑧 ≠ 𝑦 )
102	93	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → ( 𝑋 𝐿 𝑦 ) ∈ ran 𝐿 )
103		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) )
104	88	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑋 ∈ 𝑃 )
105	41	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑋 ≠ 𝑦 )
106	1 35 2 97 104 99 105	tglinerflx2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑦 ∈ ( 𝑋 𝐿 𝑦 ) )
107	1 35 2 97 98 99 101 101 102 103 106	tglinethru	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → ( 𝑋 𝐿 𝑦 ) = ( 𝑧 𝐿 𝑦 ) )
108	90	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝐴 ∈ ran 𝐿 )
109		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑧 ∈ 𝐴 )
110	37	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝑦 ∈ 𝐴 )
111	1 35 2 97 98 99 101 101 108 109 110	tglinethru	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → 𝐴 = ( 𝑧 𝐿 𝑦 ) )
112	107 111	eqtr4d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ) → ( 𝑋 𝐿 𝑦 ) = 𝐴 )
113	96 112	mtand	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) )
114	41	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝑋 ≠ 𝑦 )
115	114	neneqd	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ¬ 𝑋 = 𝑦 )
116		ioran	⊢ ( ¬ ( 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ∨ 𝑋 = 𝑦 ) ↔ ( ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ∧ ¬ 𝑋 = 𝑦 ) )
117	113 115 116	sylanbrc	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ¬ ( 𝑧 ∈ ( 𝑋 𝐿 𝑦 ) ∨ 𝑋 = 𝑦 ) )
118	1 2 35 87 88 89 92 117	ncoltgdim2	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → 𝐺 Dim_TarskiG≥ 2 )
119	1 35 2 21 27 37	tglnpt2	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ∃ 𝑧 ∈ 𝐴 𝑦 ≠ 𝑧 )
120	118 119	r19.29a	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝐺 Dim_TarskiG≥ 2 )
121	120	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝐺 Dim_TarskiG≥ 2 )
122	1 35 2 22 55 59 67	tglinerflx1	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → 𝑋 ∈ ( 𝑋 𝐿 𝑦 ) )
123	1 2 22 121 43 122 49 50	lnperpexs	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → ∃ 𝑤 ∈ 𝑃 ( ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) ( 𝑤 𝐿 𝑋 ) ∧ 𝑤 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ) )
124	86 123	r19.29a	⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) ) ∧ 𝑡 ≠ 𝑦 ) → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
125		simpr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
126	1 78 35 2 21 42 27 125	perpneq	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ( 𝑋 𝐿 𝑦 ) ≠ 𝐴 )
127	126	necomd	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → 𝐴 ≠ ( 𝑋 𝐿 𝑦 ) )
128	1 35 2 21 27 42 37 127	tglnpt4	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ∃ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑦 ) ) 𝑡 ≠ 𝑦 )
129	124 128	r19.29a	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 ) → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
130		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ¬ 𝑋 ∈ 𝐴 )
131	1 78 35 2 20 26 29 130	footex	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 ( 𝑋 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
132	129 131	r19.29a	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
133	16 132	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )

Metamath Proof Explorer

Theorem prlngex

Proof