Theorem prlnginn0

Description: A line C intersecting another line A also intersects any line B parallel to A . Theorem 12.16 of Schwabhauser p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	prlnginn0.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	prlnginn0.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	prlnginn0.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlnginn0.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	prlnginn0.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
	prlnginn0.h	$$⊢\phi \to H\in \mathrm{ran}E$$
	prlnginn0.c	$$⊢\phi \to C\in \mathrm{ran}L$$
	prlnginn0.2	$$⊢\phi \to A\cap C\ne \varnothing$$
	prlnginn0.3	$$⊢\phi \to A\ne C$$
	prlnginn0.4	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
	prlnginn0.5	$$⊢\phi \to A\subseteq H$$
	prlnginn0.6	$$⊢\phi \to B\subseteq H$$
	prlnginn0.7	$$⊢\phi \to C\subseteq H$$
Assertion	prlnginn0	$$⊢\phi \to B\cap C\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		prlnginn0.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		prlnginn0.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3		prlnginn0.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		prlnginn0.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		prlnginn0.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
6		prlnginn0.h	$$⊢\phi \to H\in \mathrm{ran}E$$
7		prlnginn0.c	$$⊢\phi \to C\in \mathrm{ran}L$$
8		prlnginn0.2	$$⊢\phi \to A\cap C\ne \varnothing$$
9		prlnginn0.3	$$⊢\phi \to A\ne C$$
10		prlnginn0.4	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
11		prlnginn0.5	$$⊢\phi \to A\subseteq H$$
12		prlnginn0.6	$$⊢\phi \to B\subseteq H$$
13		prlnginn0.7	$$⊢\phi \to C\subseteq H$$
14	8	neneqd	$$⊢\phi \to \neg A\cap C=\varnothing$$
15	4	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{\parallel }C\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
16		simpr	$$⊢\left(\phi \wedge A\underset{\dot{}}{\parallel }C\right)\to A\underset{\dot{}}{\parallel }C$$
17	9	adantr	$$⊢\left(\phi \wedge A\underset{\dot{}}{\parallel }C\right)\to A\ne C$$
18	1 3 15 16 17	prlngin0	$$⊢\left(\phi \wedge A\underset{\dot{}}{\parallel }C\right)\to A\cap C=\varnothing$$
19	14 18	mtand	$$⊢\phi \to \neg A\underset{\dot{}}{\parallel }C$$
20	4	adantr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
21	6	adantr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to H\in \mathrm{ran}E$$
22	11	adantr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to A\subseteq H$$
23	10	adantr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to A\underset{\dot{}}{\parallel }B$$
24	5	adantr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to G\in {𝒢}_{\mathrm{Tarski}}^E$$
25	13	adantr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to C\subseteq H$$
26		simpr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to B\underset{\dot{}}{\parallel }C$$
27	2 3 20 21 22 23 24 25 26	prlngplngtr	$$⊢\left(\phi \wedge B\underset{\dot{}}{\parallel }C\right)\to A\underset{\dot{}}{\parallel }C$$
28	19 27	mtand	$$⊢\phi \to \neg B\underset{\dot{}}{\parallel }C$$
29	4	adantr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
30	1 3 4 10	prlngrcl2	$$⊢\phi \to B\in \mathrm{ran}L$$
31	30	adantr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to B\in \mathrm{ran}L$$
32	7	adantr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to C\in \mathrm{ran}L$$
33	6	adantr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to H\in \mathrm{ran}E$$
34	12	adantr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to B\subseteq H$$
35	13	adantr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to C\subseteq H$$
36		simpr	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to B\cap C=\varnothing$$
37	1 2 3 29 31 32 33 34 35 36	prlngd	$$⊢\left(\phi \wedge B\cap C=\varnothing \right)\to B\underset{\dot{}}{\parallel }C$$
38	28 37	mtand	$$⊢\phi \to \neg B\cap C=\varnothing$$
39	38	neqned	$$⊢\phi \to B\cap C\ne \varnothing$$