Theorem prlngpln3

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

	Ref	Expression
Hypotheses	prlngpln3.l	|- L = ( LineG ` G )
	prlngpln3.e	|- E = ( PlnG ` G )
	prlngpln3.p	|- .|| = ( parlnG ` G )
	prlngpln3.g	|- ( ph -> G e. TarskiG )
	prlngpln3.1	|- ( ph -> A .|| B )
	prlngpln3.2	|- ( ph -> A =/= B )
	prlngpln3.x	|- ( ph -> X e. B )
Assertion	prlngpln3	|- ( ph -> B C_ ( A E X ) )

Proof

Step	Hyp	Ref	Expression
1		prlngpln3.l	|- L = ( LineG ` G )
2		prlngpln3.e	|- E = ( PlnG ` G )
3		prlngpln3.p	|- .|| = ( parlnG ` G )
4		prlngpln3.g	|- ( ph -> G e. TarskiG )
5		prlngpln3.1	|- ( ph -> A .|| B )
6		prlngpln3.2	|- ( ph -> A =/= B )
7		prlngpln3.x	|- ( ph -> X e. B )
8		eqid	|- ( Base ` G ) = ( Base ` G )
9	1 3 4 5	prlngrcl1	|- ( ph -> A e. ran L )
10	9	adantr	|- ( ( ph /\ y e. B ) -> A e. ran L )
11		eqid	|- ( Itv ` G ) = ( Itv ` G )
12	4	adantr	|- ( ( ph /\ y e. B ) -> G e. TarskiG )
13	5	adantr	|- ( ( ph /\ y e. B ) -> A .|| B )
14	1 3 12 13	prlngrcl2	|- ( ( ph /\ y e. B ) -> B e. ran L )
15		simpr	|- ( ( ph /\ y e. B ) -> y e. B )
16	8 1 11 12 14 15	tglnpt	|- ( ( ph /\ y e. B ) -> y e. ( Base ` G ) )
17	1 3 4 5	prlngrcl2	|- ( ph -> B e. ran L )
18	8 1 11 4 17 7	tglnpt	|- ( ph -> X e. ( Base ` G ) )
19		incom	|- ( A i^i B ) = ( B i^i A )
20	1 3 4 5 6	prlngin0	|- ( ph -> ( A i^i B ) = (/) )
21	19 20	eqtr3id	|- ( ph -> ( B i^i A ) = (/) )
22		disjel	|- ( ( ( B i^i A ) = (/) /\ X e. B ) -> -. X e. A )
23	21 7 22	syl2anc	|- ( ph -> -. X e. A )
24	18 23	eldifd	|- ( ph -> X e. ( ( Base ` G ) \ A ) )
25	24	adantr	|- ( ( ph /\ y e. B ) -> X e. ( ( Base ` G ) \ A ) )
26	6	adantr	|- ( ( ph /\ y e. B ) -> A =/= B )
27	7	adantr	|- ( ( ph /\ y e. B ) -> X e. B )
28	1 2 3 12 13 26 15 27	prlnghpg	|- ( ( ph /\ y e. B ) -> y ( ( hpG ` G ) ` A ) X )
29	8 1 2 10 16 25 12 28	hpgssplng	|- ( ( ph /\ y e. B ) -> y e. ( A E X ) )
30	29	ex	|- ( ph -> ( y e. B -> y e. ( A E X ) ) )
31	30	ssrdv	|- ( ph -> B C_ ( A E X ) )