Theorem brprlng

Description: Property of two lines A and B to be parallel. (Contributed by Thierry Arnoux, 18-Jun-2026)

	Ref	Expression
Hypotheses	brprlng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	brprlng.e	No typesetting found for |- E = ( PlnG ` G ) with typecode |-
	brprlng.p	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	brprlng.g	$$⊢\phi \to G\in V$$
Assertion	brprlng	$$⊢\phi \to \left(A\underset{\dot{}}{\parallel }B\leftrightarrow \left(\left(A\in \mathrm{ran}L\wedge B\in \mathrm{ran}L\right)\wedge \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brprlng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
2		brprlng.e	Could not format E = ( PlnG ` G ) : No typesetting found for |- E = ( PlnG ` G ) with typecode |-
3		brprlng.p	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
4		brprlng.g	$$⊢\phi \to G\in V$$
5		df-prlng	Could not format parlnG = ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) : No typesetting found for |- parlnG = ( g e. _V |-> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } ) with typecode |-
6		fveq2	$$⊢g=G\to {Line}_{𝒢}\left(g\right)={Line}_{𝒢}\left(G\right)$$
7	6 1	eqtr4di	$$⊢g=G\to {Line}_{𝒢}\left(g\right)=L$$
8	7	rneqd	$$⊢g=G\to \mathrm{ran}{Line}_{𝒢}\left(g\right)=\mathrm{ran}L$$
9	8	eleq2d	$$⊢g=G\to \left(a\in \mathrm{ran}{Line}_{𝒢}\left(g\right)\leftrightarrow a\in \mathrm{ran}L\right)$$
10	8	eleq2d	$$⊢g=G\to \left(b\in \mathrm{ran}{Line}_{𝒢}\left(g\right)\leftrightarrow b\in \mathrm{ran}L\right)$$
11	9 10	anbi12d	$$⊢g=G\to \left(\left(a\in \mathrm{ran}{Line}_{𝒢}\left(g\right)\wedge b\in \mathrm{ran}{Line}_{𝒢}\left(g\right)\right)\leftrightarrow \left(a\in \mathrm{ran}L\wedge b\in \mathrm{ran}L\right)\right)$$
12		fveq2	Could not format ( g = G -> ( PlnG ` g ) = ( PlnG ` G ) ) : No typesetting found for |- ( g = G -> ( PlnG ` g ) = ( PlnG ` G ) ) with typecode |-
13	12 2	eqtr4di	Could not format ( g = G -> ( PlnG ` g ) = E ) : No typesetting found for |- ( g = G -> ( PlnG ` g ) = E ) with typecode |-
14	13	rneqd	Could not format ( g = G -> ran ( PlnG ` g ) = ran E ) : No typesetting found for |- ( g = G -> ran ( PlnG ` g ) = ran E ) with typecode |-
15	14	rexeqdv	Could not format ( g = G -> ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) <-> E. h e. ran E ( a C_ h /\ b C_ h ) ) ) : No typesetting found for |- ( g = G -> ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) <-> E. h e. ran E ( a C_ h /\ b C_ h ) ) ) with typecode |-
16	15	anbi1d	Could not format ( g = G -> ( ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) <-> ( E. h e. ran E ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) : No typesetting found for |- ( g = G -> ( ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) <-> ( E. h e. ran E ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) with typecode |-
17	16	orbi2d	Could not format ( g = G -> ( ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) <-> ( a = b \/ ( E. h e. ran E ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) ) : No typesetting found for |- ( g = G -> ( ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) <-> ( a = b \/ ( E. h e. ran E ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) ) with typecode |-
18	11 17	anbi12d	Could not format ( g = G -> ( ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i 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 ) = (/) ) ) ) ) ) : No typesetting found for |- ( g = G -> ( ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i 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 ) = (/) ) ) ) ) ) with typecode |-
19	18	opabbidv	Could not format ( g = G -> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } = { <. 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 ) = (/) ) ) ) } ) : No typesetting found for |- ( g = G -> { <. a , b >. | ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) /\ ( a = b \/ ( E. h e. ran ( PlnG ` g ) ( a C_ h /\ b C_ h ) /\ ( a i^i b ) = (/) ) ) ) } = { <. 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 ) = (/) ) ) ) } ) with typecode |-
20	4	elexd	$$⊢\phi \to G\in \mathrm{V}$$
21	1	fvexi	$$⊢L\in \mathrm{V}$$
22	21	rnex	$$⊢\mathrm{ran}L\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to \mathrm{ran}L\in \mathrm{V}$$
24		simprll	$$⊢\left(\phi \wedge \left(\left(a\in \mathrm{ran}L\wedge b\in \mathrm{ran}L\right)\wedge \left(a=b\vee \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\right)\right)\right)\to a\in \mathrm{ran}L$$
25		simprlr	$$⊢\left(\phi \wedge \left(\left(a\in \mathrm{ran}L\wedge b\in \mathrm{ran}L\right)\wedge \left(a=b\vee \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\right)\right)\right)\to b\in \mathrm{ran}L$$
26	23 23 24 25	opabex2	$$⊢\phi \to \left\{⟨a,b⟩|\left(\left(a\in \mathrm{ran}L\wedge b\in \mathrm{ran}L\right)\wedge \left(a=b\vee \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\right)\right)\right\}\in \mathrm{V}$$
27	5 19 20 26	fvmptd3	Could not format ( ph -> ( parlnG ` G ) = { <. 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 ) = (/) ) ) ) } ) : No typesetting found for |- ( ph -> ( parlnG ` G ) = { <. 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 ) = (/) ) ) ) } ) with typecode |-
28	3 27	eqtrid	$$⊢\phi \to \underset{\dot{}}{\parallel }=\left\{⟨a,b⟩|\left(\left(a\in \mathrm{ran}L\wedge b\in \mathrm{ran}L\right)\wedge \left(a=b\vee \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\right)\right)\right\}$$
29		eqeq12	$$⊢\left(a=A\wedge b=B\right)\to \left(a=b\leftrightarrow A=B\right)$$
30		sseq1	$$⊢a=A\to \left(a\subseteq h\leftrightarrow A\subseteq h\right)$$
31		sseq1	$$⊢b=B\to \left(b\subseteq h\leftrightarrow B\subseteq h\right)$$
32	30 31	bi2anan9	$$⊢\left(a=A\wedge b=B\right)\to \left(\left(a\subseteq h\wedge b\subseteq h\right)\leftrightarrow \left(A\subseteq h\wedge B\subseteq h\right)\right)$$
33	32	rexbidv	$$⊢\left(a=A\wedge b=B\right)\to \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\leftrightarrow \exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\right)$$
34		ineq12	$$⊢\left(a=A\wedge b=B\right)\to a\cap b=A\cap B$$
35	34	eqeq1d	$$⊢\left(a=A\wedge b=B\right)\to \left(a\cap b=\varnothing \leftrightarrow A\cap B=\varnothing \right)$$
36	33 35	anbi12d	$$⊢\left(a=A\wedge b=B\right)\to \left(\left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\leftrightarrow \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)$$
37	29 36	orbi12d	$$⊢\left(a=A\wedge b=B\right)\to \left(\left(a=b\vee \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\right)\leftrightarrow \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)\right)$$
38	37	adantl	$$⊢\left(\phi \wedge \left(a=A\wedge b=B\right)\right)\to \left(\left(a=b\vee \left(\exists h\in \mathrm{ran}E\left(a\subseteq h\wedge b\subseteq h\right)\wedge a\cap b=\varnothing \right)\right)\leftrightarrow \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)\right)$$
39	28 38	brab2d	$$⊢\phi \to \left(A\underset{\dot{}}{\parallel }B\leftrightarrow \left(\left(A\in \mathrm{ran}L\wedge B\in \mathrm{ran}L\right)\wedge \left(A=B\vee \left(\exists h\in \mathrm{ran}E\left(A\subseteq h\wedge B\subseteq h\right)\wedge A\cap B=\varnothing \right)\right)\right)\right)$$