Metamath Proof Explorer

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 = ( LineG ` G )
brprlng.e 
|- E = ( PlnG ` G )
brprlng.p 
|- .|| = ( parlnG ` G )
brprlng.g 
|- ( ph -> G e. V )
Assertion 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 ) = (/) ) ) ) ) )

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 df-prlng 
 |-  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 ) = (/) ) ) ) } )
6 fveq2 
 |-  ( g = G -> ( LineG ` g ) = ( LineG ` G ) )
7 6 1 eqtr4di 
 |-  ( g = G -> ( LineG ` g ) = L )
8 7 rneqd 
 |-  ( g = G -> ran ( LineG ` g ) = ran L )
9 8 eleq2d 
 |-  ( g = G -> ( a e. ran ( LineG ` g ) <-> a e. ran L ) )
10 8 eleq2d 
 |-  ( g = G -> ( b e. ran ( LineG ` g ) <-> b e. ran L ) )
11 9 10 anbi12d 
 |-  ( g = G -> ( ( a e. ran ( LineG ` g ) /\ b e. ran ( LineG ` g ) ) <-> ( a e. ran L /\ b e. ran L ) ) )
12 fveq2 
 |-  ( g = G -> ( PlnG ` g ) = ( PlnG ` G ) )
13 12 2 eqtr4di 
 |-  ( g = G -> ( PlnG ` g ) = E )
14 13 rneqd 
 |-  ( g = G -> ran ( PlnG ` g ) = ran E )
15 14 rexeqdv 
 |-  ( 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 ) ) )
16 15 anbi1d 
 |-  ( 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 ) = (/) ) ) )
17 16 orbi2d 
 |-  ( 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 ) = (/) ) ) ) )
18 11 17 anbi12d 
 |-  ( 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 ) = (/) ) ) ) ) )
19 18 opabbidv 
 |-  ( 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 ) = (/) ) ) ) } )
20 4 elexd 
 |-  ( ph -> G e. _V )
21 1 fvexi 
 |-  L e. _V
22 21 rnex 
 |-  ran L e. _V
23 22 a1i 
 |-  ( ph -> ran L e. _V )
24 simprll 
 |-  ( ( 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 ) = (/) ) ) ) ) -> a e. ran L )
25 simprlr 
 |-  ( ( 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 ) = (/) ) ) ) ) -> b e. ran L )
26 23 23 24 25 opabex2 
 |-  ( 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 ) = (/) ) ) ) } e. _V )
27 5 19 20 26 fvmptd3 
 |-  ( 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 ) = (/) ) ) ) } )
28 3 27 eqtrid 
 |-  ( 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 ) = (/) ) ) ) } )
29 eqeq12 
 |-  ( ( a = A /\ b = B ) -> ( a = b <-> A = B ) )
30 sseq1 
 |-  ( a = A -> ( a C_ h <-> A C_ h ) )
31 sseq1 
 |-  ( b = B -> ( b C_ h <-> B C_ h ) )
32 30 31 bi2anan9 
 |-  ( ( a = A /\ b = B ) -> ( ( a C_ h /\ b C_ h ) <-> ( A C_ h /\ B C_ h ) ) )
33 32 rexbidv 
 |-  ( ( a = A /\ b = B ) -> ( E. h e. ran E ( a C_ h /\ b C_ h ) <-> E. h e. ran E ( A C_ h /\ B C_ h ) ) )
34 ineq12 
 |-  ( ( a = A /\ b = B ) -> ( a i^i b ) = ( A i^i B ) )
35 34 eqeq1d 
 |-  ( ( a = A /\ b = B ) -> ( ( a i^i b ) = (/) <-> ( A i^i B ) = (/) ) )
36 33 35 anbi12d 
 |-  ( ( a = A /\ b = B ) -> ( ( E. h e. ran E ( 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 ) = (/) ) ) )
37 29 36 orbi12d 
 |-  ( ( a = A /\ b = B ) -> ( ( a = b \/ ( E. h e. ran E ( 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 ) = (/) ) ) ) )
38 37 adantl 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ( ( a = b \/ ( E. h e. ran E ( 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 ) = (/) ) ) ) )
39 28 38 brab2d 
 |-  ( 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 ) = (/) ) ) ) ) )