Theorem prlngpln4

Description: Building a parallel line conserves planes, i.e. given a line A and a point X not on A , the (unique) parallel B to A through X lies completely within the plane defined by A and X . Theorem 12.14 of Schwabhauser p. 124. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	prlngpln4.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	prlngpln4.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlngpln4.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	prlngpln4.h	$$⊢\phi \to H\in \mathrm{ran}E$$
	prlngpln4.a	$$⊢\phi \to A\subseteq H$$
	prlngpln4.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
	prlngpln4.x	$$⊢\phi \to X\in H$$
	prlngpln4.2	$$⊢\phi \to X\in B$$
Assertion	prlngpln4	$$⊢\phi \to B\subseteq H$$

Proof

Step	Hyp	Ref	Expression
1		prlngpln4.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
2		prlngpln4.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
3		prlngpln4.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
4		prlngpln4.h	$$⊢\phi \to H\in \mathrm{ran}E$$
5		prlngpln4.a	$$⊢\phi \to A\subseteq H$$
6		prlngpln4.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
7		prlngpln4.x	$$⊢\phi \to X\in H$$
8		prlngpln4.2	$$⊢\phi \to X\in B$$
9		simpr	$$⊢\left(\phi \wedge A=B\right)\to A=B$$
10	5	adantr	$$⊢\left(\phi \wedge A=B\right)\to A\subseteq H$$
11	9 10	eqsstrrd	$$⊢\left(\phi \wedge A=B\right)\to B\subseteq H$$
12		eqid	$$⊢{Line}_{𝒢}\left(G\right)={Line}_{𝒢}\left(G\right)$$
13	3	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
14	6	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to A\underset{\dot{}}{\parallel }B$$
15		simpr	$$⊢\left(\phi \wedge A\ne B\right)\to A\ne B$$
16	8	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to X\in B$$
17	12 1 2 13 14 15 16	prlngpln3	$$⊢\left(\phi \wedge A\ne B\right)\to B\subseteq AEX$$
18		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
19	4	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to H\in \mathrm{ran}E$$
20	12 2 3 6	prlngrcl1	$$⊢\phi \to A\in \mathrm{ran}{Line}_{𝒢}\left(G\right)$$
21	20	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to A\in \mathrm{ran}{Line}_{𝒢}\left(G\right)$$
22	7	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to X\in H$$
23	12 2 13 14 15	prlngin0	$$⊢\left(\phi \wedge A\ne B\right)\to A\cap B=\varnothing$$
24	23	adantr	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge X\in A\right)\to A\cap B=\varnothing$$
25		simpr	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge X\in A\right)\to X\in A$$
26	8	ad2antrr	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge X\in A\right)\to X\in B$$
27	25 26	elind	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge X\in A\right)\to X\in \left(A\cap B\right)$$
28	27	ne0d	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge X\in A\right)\to A\cap B\ne \varnothing$$
29	28	neneqd	$$⊢\left(\left(\phi \wedge A\ne B\right)\wedge X\in A\right)\to \neg A\cap B=\varnothing$$
30	24 29	pm2.65da	$$⊢\left(\phi \wedge A\ne B\right)\to \neg X\in A$$
31	22 30	eldifd	$$⊢\left(\phi \wedge A\ne B\right)\to X\in \left(H\setminus A\right)$$
32	5	adantr	$$⊢\left(\phi \wedge A\ne B\right)\to A\subseteq H$$
33	18 12 1 13 19 21 31 32	plng3p	$$⊢\left(\phi \wedge A\ne B\right)\to H=AEX$$
34	17 33	sseqtrrd	$$⊢\left(\phi \wedge A\ne B\right)\to B\subseteq H$$
35	11 34	pm2.61dane	$$⊢\phi \to B\subseteq H$$