Metamath Proof Explorer

Theorem dfprlng2

Description: Alternate definition of (strict) parallelism. Theorem 12.7 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses dfprlng2.b ⊢ 𝑃 = ( Base ‘ 𝐺 )
dfprlng2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
dfprlng2.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
dfprlng2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
dfprlng2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
dfprlng2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
dfprlng2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
dfprlng2.w ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑃 ∖ { 𝑍 } ) )
dfprlng2.1 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
Assertion dfprlng2 ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ↔ ( 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 dfprlng2.b ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 dfprlng2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 dfprlng2.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 dfprlng2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 dfprlng2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 dfprlng2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
7 dfprlng2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 dfprlng2.w ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑃 ∖ { 𝑍 } ) )
9 dfprlng2.1 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
10 9 neneqd ⊢ ( 𝜑 → ¬ ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) )
11 biorf ⊢ ( ¬ ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) → ( ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ↔ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) ) )
12 10 11 syl ⊢ ( 𝜑 → ( ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ↔ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) ) )
13 12 anbi2d ⊢ ( 𝜑 → ( ( ( ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 ∧ ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 ) ∧ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) ↔ ( ( ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 ∧ ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) ) ) )
14 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
15 6 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
16 6 eldifsnbd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
17 16 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
18 1 14 2 4 5 15 17 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
19 8 eldifad ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
20 8 eldifsnbd ⊢ ( 𝜑 → 𝑊 ≠ 𝑍 )
21 20 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑊 )
22 1 14 2 4 7 19 21 tgelrnln ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
23 18 22 jca ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 ∧ ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 ) )
24 23 biantrurd ⊢ ( 𝜑 → ( ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ↔ ( ( ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 ∧ ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 ) ∧ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) ) )
25 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
26 2 25 3 4 brprlng ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ↔ ( ( ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 ∧ ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 ) ∧ ( ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) ) ) )
27 13 24 26 3bitr4rd ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ↔ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) )
28 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → 𝐺 ∈ TarskiG )
29 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ℎ ∈ ran ( hlG ‘ 𝐺 ) )
30 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ( 𝑋 𝐿 𝑌 ) ⊆ ℎ )
31 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ( 𝑍 𝐿 𝑊 ) ⊆ ℎ )
32 rspe ⊢ ( ( ℎ ∈ ran ( hlG ‘ 𝐺 ) ∧ ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ) → ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) )
33 29 30 31 32 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) )
34 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ )
35 27 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ↔ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) )
36 33 34 35 mpbir2and ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
37 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
38 1 14 2 4 7 19 21 tglinerflx1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
39 38 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
40 1 14 2 4 7 19 21 tglinerflx2 ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑍 𝐿 𝑊 ) )
41 40 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → 𝑊 ∈ ( 𝑍 𝐿 𝑊 ) )
42 2 25 3 28 36 37 39 41 prlnghpg ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 )
43 42 anasss ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ℎ ∈ ran ( hlG ‘ 𝐺 ) ) ∧ ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ) → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 )
44 43 r19.29an ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ) → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 )
45 sseq2 ⊢ ( ℎ = ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ↔ ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ) )
46 sseq2 ⊢ ( ℎ = ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) → ( ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ↔ ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ) )
47 45 46 anbi12d ⊢ ( ℎ = ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) → ( ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ↔ ( ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ) ) )
48 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝐺 ∈ TarskiG )
49 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
50 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑊 ∈ 𝑃 )
51 nel02 ⊢ ( ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ → ¬ 𝑊 ∈ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
52 51 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ¬ 𝑊 ∈ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
53 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) )
54 40 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ ( 𝑍 𝐿 𝑊 ) )
55 53 54 elind ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑊 ∈ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
56 52 55 mtand ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑌 ) )
57 50 56 eldifd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑊 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
58 1 2 25 48 49 57 tgelrnpln ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ∈ ran ( hlG ‘ 𝐺 ) )
59 1 14 2 25 48 49 57 elplnglnid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) )
60 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑍 ∈ 𝑃 )
61 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 )
62 1 2 25 49 60 57 48 61 hpgssplng ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑍 ∈ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) )
63 1 14 2 25 48 49 57 elplngid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑊 ∈ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) )
64 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → 𝑍 ≠ 𝑊 )
65 1 14 2 25 48 58 62 63 64 lnssplng1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) )
66 59 65 jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑊 ) ) )
67 47 58 66 rspcedvdw ⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) → ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) )
68 44 67 impbida ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) → ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ↔ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) )
69 68 pm5.32da ⊢ ( 𝜑 → ( ( ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ∧ ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ) ↔ ( ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) ) )
70 ancom ⊢ ( ( ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ∧ ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ) ↔ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) )
71 ancom ⊢ ( ( ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ) ↔ ( 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) )
72 69 70 71 3bitr3g ⊢ ( 𝜑 → ( ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( ( 𝑋 𝐿 𝑌 ) ⊆ ℎ ∧ ( 𝑍 𝐿 𝑊 ) ⊆ ℎ ) ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ↔ ( 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) )
73 27 72 bitrd ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) ↔ ( 𝑍 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑋 𝐿 𝑌 ) ) 𝑊 ∧ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ ) ) )