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 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
brprlng.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
brprlng.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
brprlng.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion brprlng ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 brprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
2 brprlng.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
3 brprlng.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 brprlng.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5 df-prlng ⊢ parlnG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )
6 fveq2 ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = ( LineG ‘ 𝐺 ) )
7 6 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( LineG ‘ 𝑔 ) = 𝐿 )
8 7 rneqd ⊢ ( 𝑔 = 𝐺 → ran ( LineG ‘ 𝑔 ) = ran 𝐿 )
9 8 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ↔ 𝑎 ∈ ran 𝐿 ) )
10 8 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ↔ 𝑏 ∈ ran 𝐿 ) )
11 9 10 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ↔ ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ) )
12 fveq2 ⊢ ( 𝑔 = 𝐺 → ( hlG ‘ 𝑔 ) = ( hlG ‘ 𝐺 ) )
13 12 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( hlG ‘ 𝑔 ) = 𝐸 )
14 13 rneqd ⊢ ( 𝑔 = 𝐺 → ran ( hlG ‘ 𝑔 ) = ran 𝐸 )
15 14 rexeqdv ⊢ ( 𝑔 = 𝐺 → ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ↔ ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ) )
16 15 anbi1d ⊢ ( 𝑔 = 𝐺 → ( ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ↔ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) )
17 16 orbi2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ↔ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) )
18 11 17 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) ↔ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) ) )
19 18 opabbidv ⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran ( LineG ‘ 𝑔 ) ∧ 𝑏 ∈ ran ( LineG ‘ 𝑔 ) ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝑔 ) ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )
20 4 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
21 1 fvexi ⊢ 𝐿 ∈ V
22 21 rnex ⊢ ran 𝐿 ∈ V
23 22 a1i ⊢ ( 𝜑 → ran 𝐿 ∈ V )
24 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) ) → 𝑎 ∈ ran 𝐿 )
25 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) ) → 𝑏 ∈ ran 𝐿 )
26 23 23 24 25 opabex2 ⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } ∈ V )
27 5 19 20 26 fvmptd3 ⊢ ( 𝜑 → ( parlnG ‘ 𝐺 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )
28 3 27 eqtrid ⊢ ( 𝜑 → ∥ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ran 𝐿 ∧ 𝑏 ∈ ran 𝐿 ) ∧ ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ) } )
29 eqeq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 = 𝑏 ↔ 𝐴 = 𝐵 ) )
30 sseq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ⊆ ℎ ↔ 𝐴 ⊆ ℎ ) )
31 sseq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ ℎ ↔ 𝐵 ⊆ ℎ ) )
32 30 31 bi2anan9 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ↔ ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ) )
33 32 rexbidv ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ↔ ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ) )
34 ineq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ∩ 𝑏 ) = ( 𝐴 ∩ 𝐵 ) )
35 34 eqeq1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ∩ 𝑏 ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
36 33 35 anbi12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ↔ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
37 29 36 orbi12d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ↔ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( ( 𝑎 = 𝑏 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝑎 ⊆ ℎ ∧ 𝑏 ⊆ ℎ ) ∧ ( 𝑎 ∩ 𝑏 ) = ∅ ) ) ↔ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
39 28 38 brab2d ⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )