Metamath Proof Explorer

Theorem dfprlng3

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 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
dfprlng3.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
dfprlng3.1 ⊢ ( 𝜑 → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
Assertion dfprlng3 ( 𝜑 → ( 𝐴 ∥ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 ( ( 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 dfprlng3.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
8 dfprlng3.1 ⊢ ( 𝜑 → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
9 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝐺 ∈ TarskiG )
10 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑧 ∈ 𝑃 )
11 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑤 ∈ 𝑃 )
12 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑧 ≠ 𝑤 )
13 12 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑤 ≠ 𝑧 )
14 11 13 eldifsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑤 ∈ ( 𝑃 ∖ { 𝑧 } ) )
15 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑋 ∈ 𝑃 )
16 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝑌 ∈ ( 𝑃 ∖ { 𝑋 } ) )
17 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝐴 = ( 𝑧 𝐿 𝑤 ) )
18 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
19 17 18 eqnetrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( 𝑧 𝐿 𝑤 ) ≠ ( 𝑋 𝐿 𝑌 ) )
20 1 2 3 9 10 14 15 16 19 dfprlng2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 𝐿 𝑤 ) ∥ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑧 𝐿 𝑤 ) ) 𝑌 ∧ ( ( 𝑧 𝐿 𝑤 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) ) )
21 17 breq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( 𝐴 ∥ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑧 𝐿 𝑤 ) ∥ ( 𝑋 𝐿 𝑌 ) ) )
22 17 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑧 𝐿 𝑤 ) ) )
23 22 breqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ↔ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑧 𝐿 𝑤 ) ) 𝑌 ) )
24 17 ineq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) = ( ( 𝑧 𝐿 𝑤 ) ∩ ( 𝑋 𝐿 𝑌 ) ) )
25 24 eqeq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ↔ ( ( 𝑧 𝐿 𝑤 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) )
26 23 25 anbi12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∧ ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) ↔ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑧 𝐿 𝑤 ) ) 𝑌 ∧ ( ( 𝑧 𝐿 𝑤 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) ) )
27 20 21 26 3bitr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ 𝐴 = ( 𝑧 𝐿 𝑤 ) ) ∧ 𝑧 ≠ 𝑤 ) → ( 𝐴 ∥ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∧ ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) ) )
28 27 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑧 𝐿 𝑤 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( 𝐴 ∥ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∧ ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) ) )
29 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
30 1 29 2 4 7 tgisline ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑃 ∃ 𝑤 ∈ 𝑃 ( 𝐴 = ( 𝑧 𝐿 𝑤 ) ∧ 𝑧 ≠ 𝑤 ) )
31 28 30 r19.29vva ⊢ ( 𝜑 → ( 𝐴 ∥ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∧ ( 𝐴 ∩ ( 𝑋 𝐿 𝑌 ) ) = ∅ ) ) )