Theorem prlngin0

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

	Ref	Expression
Hypotheses	prlngin0.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	prlngin0.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	prlngin0.g	$$⊢\phi \to G\in V$$
	prlngin0.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
	prlngin0.2	$$⊢\phi \to A\ne B$$
Assertion	prlngin0	$$⊢\phi \to A\cap B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		prlngin0.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		prlngin0.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
3		prlngin0.g	$$⊢\phi \to G\in V$$
4		prlngin0.1	$$⊢\phi \to A\underset{\dot{}}{\parallel }B$$
5		prlngin0.2	$$⊢\phi \to A\ne B$$
6		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for |- ( PlnG ` G ) = ( PlnG ` G ) with typecode |-
7	1 6 2 3	brprlng	Could not format ( 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 ) = (/) ) ) ) ) ) : No typesetting found for |- ( 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 ) = (/) ) ) ) ) ) with typecode |-
8	4 7	mpbid	Could not format ( 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 ) = (/) ) ) ) ) : No typesetting found for |- ( 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 ) = (/) ) ) ) ) with typecode |-
9	8	simprd	Could not format ( ph -> ( A = B \/ ( E. h e. ran ( PlnG ` G ) ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) : No typesetting found for |- ( ph -> ( A = B \/ ( E. h e. ran ( PlnG ` G ) ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) ) with typecode |-
10	5	neneqd	$$⊢\phi \to \neg A=B$$
11	9 10	orcnd	Could not format ( ph -> ( E. h e. ran ( PlnG ` G ) ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) : No typesetting found for |- ( ph -> ( E. h e. ran ( PlnG ` G ) ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) with typecode |-
12	11	simprd	$$⊢\phi \to A\cap B=\varnothing$$