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	$⊢ P = {Base}_{G}$
	prlngeu.l	$⊢ L = {Line}_{𝒢} (G)$
	prlngeu.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlngeu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlngeu.a	$⊢ φ \to A \in ran L$
	prlngex.6	$⊢ φ \to X \in P$
Assertion	prlngex	$⊢ φ \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	$⊢ P = {Base}_{G}$
2		prlngeu.l	$⊢ L = {Line}_{𝒢} (G)$
3		prlngeu.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
4		prlngeu.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		prlngeu.a	$⊢ φ \to A \in ran L$
6		prlngex.6	$⊢ φ \to X \in P$
7		breq2	$⊢ b = A \to (A \underset{˙}{∥} b \leftrightarrow A \underset{˙}{∥} A)$
8		eleq2	$⊢ b = A \to (X \in b \leftrightarrow X \in A)$
9	7 8	anbi12d	$⊢ b = A \to ((A \underset{˙}{∥} b \land X \in b) \leftrightarrow (A \underset{˙}{∥} A \land X \in A))$
10	5	adantr	$⊢ (φ \land X \in A) \to A \in ran L$
11		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for \|- ( PlnG ` G ) = ( PlnG ` G ) with typecode \|-
12	4	adantr	$⊢ (φ \land X \in A) \to G \in 𝒢_{Tarski}$
13	2 11 3 12 10	prlngref	$⊢ (φ \land X \in A) \to A \underset{˙}{∥} A$
14		simpr	$⊢ (φ \land X \in A) \to X \in A$
15	13 14	jca	$⊢ (φ \land X \in A) \to (A \underset{˙}{∥} A \land X \in A)$
16	9 10 15	rspcedvdw	$⊢ (φ \land X \in A) \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$
17		breq2	$⊢ b = w L X \to (A \underset{˙}{∥} b \leftrightarrow A \underset{˙}{∥} (w L X))$
18		eleq2	$⊢ b = w L X \to (X \in b \leftrightarrow X \in (w L X))$
19	17 18	anbi12d	$⊢ b = w L X \to ((A \underset{˙}{∥} b \land X \in b) \leftrightarrow (A \underset{˙}{∥} (w L X) \land X \in (w L X)))$
20	4	adantr	$⊢ (φ \land \neg X \in A) \to G \in 𝒢_{Tarski}$
21	20	ad2antrr	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to G \in 𝒢_{Tarski}$
22	21	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to G \in 𝒢_{Tarski}$
23	22	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to G \in 𝒢_{Tarski}$
24		simplr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to (X L y) ⟂_{𝒢} (G) (w L X)$
25	2 23 24	perpln2	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to w L X \in ran L$
26	5	adantr	$⊢ (φ \land \neg X \in A) \to A \in ran L$
27	26	ad2antrr	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to A \in ran L$
28	27	ad5antr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to A \in ran L$
29	6	adantr	$⊢ (φ \land \neg X \in A) \to X \in P$
30	29	ad2antrr	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to X \in P$
31		simpllr	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to \neg X \in A$
32	30 31	eldifd	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to X \in (P ∖ A)$
33	32	ad5antr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to X \in (P ∖ A)$
34	1 2 11 23 28 33	tgelrnpln	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A ( PlnG ` G ) X ) e. ran ( PlnG ` G ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A ( PlnG ` G ) X ) e. ran ( PlnG ` G ) ) with typecode \|-
35		eqid	$⊢ Itv (G) = Itv (G)$
36	1 35 2 11 23 28 33	elplnglnid	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A C_ ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> A C_ ( A ( PlnG ` G ) X ) ) with typecode \|-
37		simplr	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to y \in A$
38	1 2 35 21 27 37	tglnpt	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to y \in P$
39		nelne2	$⊢ (y \in A \land \neg X \in A) \to y \neq X$
40	37 31 39	syl2anc	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to y \neq X$
41	40	necomd	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to X \neq y$
42	1 35 2 21 30 38 41	tgelrnln	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to X L y \in ran L$
43	42	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to X L y \in ran L$
44	43	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to X L y \in ran L$
45		simpllr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to w \in P$
46	27	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to A \in ran L$
47		simplr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to t \in (A ∖ (X L y))$
48	47	eldifad	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to t \in A$
49	1 2 35 22 46 48	tglnpt	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to t \in P$
50	47	eldifbd	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to \neg t \in (X L y)$
51	49 50	eldifd	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to t \in (P ∖ (X L y))$
52	51	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to t \in (P ∖ (X L y))$
53		simpr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to w {hp}_{𝒢} (G) (X L y) t$
54	1 2 11 44 45 52 23 53	hpgssplng	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. ( ( X L y ) ( PlnG ` G ) t ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. ( ( X L y ) ( PlnG ` G ) t ) ) with typecode \|-
55	30	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to X \in P$
56	55	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to X \in P$
57	31	ad5antr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to \neg X \in A$
58	49	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to t \in P$
59	38	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to y \in P$
60	59	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to y \in P$
61		simp-4r	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to t \neq y$
62	48	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to t \in A$
63	37	ad5antr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to y \in A$
64	1 35 2 23 58 60 61 61 28 62 63	tglinethru	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to A = t L y$
65	57 64	neleqtrd	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to \neg X \in (t L y)$
66	56 65	eldifd	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to X \in (P ∖ (t L y))$
67	41	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to X \neq y$
68	67	ad3antrrr	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to X \neq y$
69	1 35 2 11 23 66 60 52 68	plngrot	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( ( X L y ) ( PlnG ` G ) t ) = ( ( t L y ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( ( X L y ) ( PlnG ` G ) t ) = ( ( t L y ) ( PlnG ` G ) X ) ) with typecode \|-
70	64	oveq1d	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A ( PlnG ` G ) X ) = ( ( t L y ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( A ( PlnG ` G ) X ) = ( ( t L y ) ( PlnG ` G ) X ) ) with typecode \|-
71	69 70	eqtr4d	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( ( X L y ) ( PlnG ` G ) t ) = ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( ( X L y ) ( PlnG ` G ) t ) = ( A ( PlnG ` G ) X ) ) with typecode \|-
72	54 71	eleqtrd	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> w e. ( A ( PlnG ` G ) X ) ) with typecode \|-
73	1 35 2 11 23 28 33	elplngid	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> X e. ( A ( PlnG ` G ) X ) ) with typecode \|-
74	1 35 2 23 45 56 25	tglnne	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to w \neq X$
75	1 35 2 11 23 34 72 73 74	lnssplng1	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( w L X ) C_ ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( w L X ) C_ ( A ( PlnG ` G ) X ) ) with typecode \|-
76	36 63	sseldd	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> y e. ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> y e. ( A ( PlnG ` G ) X ) ) with typecode \|-
77	1 35 2 11 23 34 73 76 68	lnssplng1	Could not format ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( X L y ) C_ ( A ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ( ( ( ( ( ph /\ -. X e. A ) /\ y e. A ) /\ ( X L y ) ( perpG ` G ) A ) /\ t e. ( A \ ( X L y ) ) ) /\ t =/= y ) /\ w e. P ) /\ ( X L y ) ( perpG ` G ) ( w L X ) ) /\ w ( ( hpG ` G ) ` ( X L y ) ) t ) -> ( X L y ) C_ ( A ( PlnG ` G ) X ) ) with typecode \|-
78		eqid	$⊢ dist (G) = dist (G)$
79		simp-6r	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to (X L y) ⟂_{𝒢} (G) A$
80	1 78 35 2 23 44 28 79	perpcom	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to A ⟂_{𝒢} (G) (X L y)$
81	1 78 35 2 23 44 25 24	perpcom	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to (w L X) ⟂_{𝒢} (G) (X L y)$
82	1 2 11 3 23 34 36 75 77 80 81	perpprlng	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to A \underset{˙}{∥} (w L X)$
83	1 35 2 23 45 56 74	tglinerflx2	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to X \in (w L X)$
84	82 83	jca	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to (A \underset{˙}{∥} (w L X) \land X \in (w L X))$
85	19 25 84	rspcedvdw	$⊢ ((((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land (X L y) ⟂_{𝒢} (G) (w L X)) \land w {hp}_{𝒢} (G) (X L y) t) \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$
86	85	anasss	$⊢ (((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \land w \in P) \land ((X L y) ⟂_{𝒢} (G) (w L X) \land w {hp}_{𝒢} (G) (X L y) t)) \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$
87	21	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to G \in 𝒢_{Tarski}$
88	29	ad4antr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to X \in P$
89	38	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to y \in P$
90	27	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to A \in ran L$
91		simplr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to z \in A$
92	1 2 35 87 90 91	tglnpt	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to z \in P$
93	42	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to X L y \in ran L$
94		simpllr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to (X L y) ⟂_{𝒢} (G) A$
95	1 78 35 2 87 93 90 94	perpneq	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to X L y \neq A$
96	95	neneqd	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to \neg X L y = A$
97	87	adantr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to G \in 𝒢_{Tarski}$
98	92	adantr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to z \in P$
99	89	adantr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to y \in P$
100		simplr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to y \neq z$
101	100	necomd	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to z \neq y$
102	93	adantr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to X L y \in ran L$
103		simpr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to z \in (X L y)$
104	88	adantr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to X \in P$
105	41	ad3antrrr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to X \neq y$
106	1 35 2 97 104 99 105	tglinerflx2	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to y \in (X L y)$
107	1 35 2 97 98 99 101 101 102 103 106	tglinethru	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to X L y = z L y$
108	90	adantr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to A \in ran L$
109		simpllr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to z \in A$
110	37	ad3antrrr	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to y \in A$
111	1 35 2 97 98 99 101 101 108 109 110	tglinethru	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to A = z L y$
112	107 111	eqtr4d	$⊢ ((((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \land z \in (X L y)) \to X L y = A$
113	96 112	mtand	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to \neg z \in (X L y)$
114	41	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to X \neq y$
115	114	neneqd	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to \neg X = y$
116		ioran	$⊢ \neg (z \in (X L y) \lor X = y) \leftrightarrow (\neg z \in (X L y) \land \neg X = y)$
117	113 115 116	sylanbrc	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to \neg (z \in (X L y) \lor X = y)$
118	1 2 35 87 88 89 92 117	ncoltgdim2	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land z \in A) \land y \neq z) \to G {Dim}_{𝒢} \geq 2$
119	1 35 2 21 27 37	tglnpt2	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to \exists z \in A y \neq z$
120	118 119	r19.29a	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to G {Dim}_{𝒢} \geq 2$
121	120	ad2antrr	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to G {Dim}_{𝒢} \geq 2$
122	1 35 2 22 55 59 67	tglinerflx1	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to X \in (X L y)$
123	1 2 22 121 43 122 49 50	lnperpexs	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to \exists w \in P ((X L y) ⟂_{𝒢} (G) (w L X) \land w {hp}_{𝒢} (G) (X L y) t)$
124	86 123	r19.29a	$⊢ (((((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \land t \in (A ∖ (X L y))) \land t \neq y) \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$
125		simpr	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to (X L y) ⟂_{𝒢} (G) A$
126	1 78 35 2 21 42 27 125	perpneq	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to X L y \neq A$
127	126	necomd	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to A \neq X L y$
128	1 35 2 21 27 42 37 127	tglnpt4	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to \exists t \in (A ∖ (X L y)) t \neq y$
129	124 128	r19.29a	$⊢ (((φ \land \neg X \in A) \land y \in A) \land (X L y) ⟂_{𝒢} (G) A) \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$
130		simpr	$⊢ (φ \land \neg X \in A) \to \neg X \in A$
131	1 78 35 2 20 26 29 130	footex	$⊢ (φ \land \neg X \in A) \to \exists y \in A (X L y) ⟂_{𝒢} (G) A$
132	129 131	r19.29a	$⊢ (φ \land \neg X \in A) \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$
133	16 132	pm2.61dan	$⊢ φ \to \exists b \in ran L (A \underset{˙}{∥} b \land X \in b)$

Metamath Proof Explorer

Theorem prlngex

Proof