Theorem prlngpln

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

	Ref	Expression
Hypotheses	prlngpln.l	|- L = ( LineG ` G )
	prlngpln.e	|- E = ( PlnG ` G )
	prlngpln.p	|- .|| = ( parlnG ` G )
	prlngpln.g	|- ( ph -> G e. V )
	prlngpln.1	|- ( ph -> A .|| B )
	prlngpln.2	|- ( ph -> A =/= B )
Assertion	prlngpln	|- ( ph -> E. h e. ran E ( A C_ h /\ B C_ h ) )

Proof

Step	Hyp	Ref	Expression
1		prlngpln.l	|- L = ( LineG ` G )
2		prlngpln.e	|- E = ( PlnG ` G )
3		prlngpln.p	|- .|| = ( parlnG ` G )
4		prlngpln.g	|- ( ph -> G e. V )
5		prlngpln.1	|- ( ph -> A .|| B )
6		prlngpln.2	|- ( ph -> A =/= B )
7	1 2 3 4	brprlng	|- ( ph -> ( A .|| B <-> ( ( A e. ran L /\ B e. ran L ) /\ ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) ) )
8	5 7	mpbid	|- ( ph -> ( ( A e. ran L /\ B e. ran L ) /\ ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) )
9	8	simprd	|- ( ph -> ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) )
10	6	neneqd	|- ( ph -> -. A = B )
11	9 10	orcnd	|- ( ph -> ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) )
12	11	simpld	|- ( ph -> E. h e. ran E ( A C_ h /\ B C_ h ) )