Theorem prlngpln3

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

	Ref	Expression
Hypotheses	prlngpln3.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngpln3.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	prlngpln3.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngpln3.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	prlngpln3.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
	prlngpln3.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	prlngpln3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	prlngpln3	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐴 𝐸 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		prlngpln3.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		prlngpln3.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
3		prlngpln3.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		prlngpln3.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		prlngpln3.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
6		prlngpln3.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
7		prlngpln3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
9	1 3 4 5	prlngrcl1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐴 ∈ ran 𝐿 )
11		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐺 ∈ TarskiG )
13	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐴 ∥ 𝐵 )
14	1 3 12 13	prlngrcl2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐵 ∈ ran 𝐿 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
16	8 1 11 12 14 15	tglnpt	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
17	1 3 4 5	prlngrcl2	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
18	8 1 11 4 17 7	tglnpt	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
19		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
20	1 3 4 5 6	prlngin0	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
21	19 20	eqtr3id	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) = ∅ )
22		disjel	⊢ ( ( ( 𝐵 ∩ 𝐴 ) = ∅ ∧ 𝑋 ∈ 𝐵 ) → ¬ 𝑋 ∈ 𝐴 )
23	21 7 22	syl2anc	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
24	18 23	eldifd	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) )
26	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
27	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
28	1 2 3 12 13 26 15 27	prlnghpg	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
29	8 1 2 10 16 25 12 28	hpgssplng	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ( 𝐴 𝐸 𝑋 ) )
30	29	ex	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 𝐴 𝐸 𝑋 ) ) )
31	30	ssrdv	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐴 𝐸 𝑋 ) )