Theorem prlngpln3

Description: Two parallel lines are on a common plane. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngpln3.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	prlngpln3.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	prlngpln3.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlngpln3.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	prlngpln3.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
	prlngpln3.2	$$⊢\phi \to A\ne B$$
	prlngpln3.x	$$⊢\phi \to X\in B$$
Assertion	prlngpln3	$$⊢\phi \to B\subseteq AEX$$

Proof

Step	Hyp	Ref	Expression
1		prlngpln3.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		prlngpln3.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3		prlngpln3.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		prlngpln3.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		prlngpln3.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
6		prlngpln3.2	$$⊢\phi \to A\ne B$$
7		prlngpln3.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
9	1 3 4 5	prlngrcl1	$$⊢\phi \to A\in \mathrm{ran}L$$
10	9	adantr	$$⊢\left(\phi \wedge y\in B\right)\to A\in \mathrm{ran}L$$
11		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
12	4	adantr	$$⊢\left(\phi \wedge y\in B\right)\to G\in {𝒢}_{\mathrm{Tarski}}$$
13	5	adantr	$$⊢\left(\phi \wedge y\in B\right)\to A\underset{\dot{}}{\parallel }B$$
14	1 3 12 13	prlngrcl2	$$⊢\left(\phi \wedge y\in B\right)\to B\in \mathrm{ran}L$$
15		simpr	$$⊢\left(\phi \wedge y\in B\right)\to y\in B$$
16	8 1 11 12 14 15	tglnpt	$$⊢\left(\phi \wedge y\in B\right)\to y\in {\mathrm{Base}}_G$$
17	1 3 4 5	prlngrcl2	$$⊢\phi \to B\in \mathrm{ran}L$$
18	8 1 11 4 17 7	tglnpt	$$⊢\phi \to X\in {\mathrm{Base}}_G$$
19		incom	$$⊢A\cap B=B\cap A$$
20	1 3 4 5 6	prlngin0	$$⊢\phi \to A\cap B=\varnothing$$
21	19 20	eqtr3id	$$⊢\phi \to B\cap A=\varnothing$$
22		disjel	$$⊢\left(B\cap A=\varnothing \wedge X\in B\right)\to \neg X\in A$$
23	21 7 22	syl2anc	$$⊢\phi \to \neg X\in A$$
24	18 23	eldifd	$$⊢\phi \to X\in \left({\mathrm{Base}}_G\setminus A\right)$$
25	24	adantr	$$⊢\left(\phi \wedge y\in B\right)\to X\in \left({\mathrm{Base}}_G\setminus A\right)$$
26	6	adantr	$$⊢\left(\phi \wedge y\in B\right)\to A\ne B$$
27	7	adantr	$$⊢\left(\phi \wedge y\in B\right)\to X\in B$$
28	1 2 3 12 13 26 15 27	prlnghpg	$$⊢\left(\phi \wedge y\in B\right)\to y{hp}_{𝒢}\left(G\right)\left(A\right)X$$
29	8 1 2 10 16 25 12 28	hpgssplng	$$⊢\left(\phi \wedge y\in B\right)\to y\in \left(AEX\right)$$
30	29	ex	$$⊢\phi \to \left(y\in B\to y\in \left(AEX\right)\right)$$
31	30	ssrdv	$$⊢\phi \to B\subseteq AEX$$