Theorem prlngin0

Description: Two parallel lines do not intersect. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngin0.l	|- L = ( LineG ` G )
	prlngin0.p	|- .|| = ( parlnG ` G )
	prlngin0.g	|- ( ph -> G e. V )
	prlngin0.1	|- ( ph -> A .|| B )
	prlngin0.2	|- ( ph -> A =/= B )
Assertion	prlngin0	|- ( ph -> ( A i^i B ) = (/) )

Proof

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