Theorem prlngd

Description: Deduce parallelism between two lines A and B . (Contributed by Thierry Arnoux, 18-Jun-2026)

	Ref	Expression
Hypotheses	brprlng.l	|- L = ( LineG ` G )
	brprlng.e	|- E = ( PlnG ` G )
	brprlng.p	|- .|| = ( parlnG ` G )
	brprlng.g	|- ( ph -> G e. V )
	prlngd.a	|- ( ph -> A e. ran L )
	prlngd.b	|- ( ph -> B e. ran L )
	prlngd.h	|- ( ph -> H e. ran E )
	prlngd.1	|- ( ph -> A C_ H )
	prlngd.2	|- ( ph -> B C_ H )
	prlngd.3	|- ( ph -> ( A i^i B ) = (/) )
Assertion	prlngd	|- ( ph -> A .|| B )

Proof

Step	Hyp	Ref	Expression
1		brprlng.l	|- L = ( LineG ` G )
2		brprlng.e	|- E = ( PlnG ` G )
3		brprlng.p	|- .|| = ( parlnG ` G )
4		brprlng.g	|- ( ph -> G e. V )
5		prlngd.a	|- ( ph -> A e. ran L )
6		prlngd.b	|- ( ph -> B e. ran L )
7		prlngd.h	|- ( ph -> H e. ran E )
8		prlngd.1	|- ( ph -> A C_ H )
9		prlngd.2	|- ( ph -> B C_ H )
10		prlngd.3	|- ( ph -> ( A i^i B ) = (/) )
11	5 6	jca	|- ( ph -> ( A e. ran L /\ B e. ran L ) )
12		sseq2	|- ( h = H -> ( A C_ h <-> A C_ H ) )
13		sseq2	|- ( h = H -> ( B C_ h <-> B C_ H ) )
14	12 13	anbi12d	|- ( h = H -> ( ( A C_ h /\ B C_ h ) <-> ( A C_ H /\ B C_ H ) ) )
15	8 9	jca	|- ( ph -> ( A C_ H /\ B C_ H ) )
16	14 7 15	rspcedvdw	|- ( ph -> E. h e. ran E ( A C_ h /\ B C_ h ) )
17	16 10	jca	|- ( ph -> ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) )
18	17	olcd	|- ( ph -> ( A = B \/ ( E. h e. ran E ( A C_ h /\ B C_ h ) /\ ( A i^i B ) = (/) ) ) )
19	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 ) = (/) ) ) ) ) )
20	11 18 19	mpbir2and	|- ( ph -> A .|| B )