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 
|- P = ( Base ` G )
dfprlng2.l 
|- L = ( LineG ` G )
dfprlng2.p 
|- .|| = ( parlnG ` G )
dfprlng2.g 
|- ( ph -> G e. TarskiG )
dfprlng2.x 
|- ( ph -> X e. P )
dfprlng2.y 
|- ( ph -> Y e. ( P \ { X } ) )
dfprlng3.a 
|- ( ph -> A e. ran L )
dfprlng3.1 
|- ( ph -> A =/= ( X L Y ) )
Assertion dfprlng3 
|- ( ph -> ( A .|| ( X L Y ) <-> ( X ( ( hpG ` G ) ` A ) Y /\ ( A i^i ( X L Y ) ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 dfprlng2.b 
 |-  P = ( Base ` G )
2 dfprlng2.l 
 |-  L = ( LineG ` G )
3 dfprlng2.p 
 |-  .|| = ( parlnG ` G )
4 dfprlng2.g 
 |-  ( ph -> G e. TarskiG )
5 dfprlng2.x 
 |-  ( ph -> X e. P )
6 dfprlng2.y 
 |-  ( ph -> Y e. ( P \ { X } ) )
7 dfprlng3.a 
 |-  ( ph -> A e. ran L )
8 dfprlng3.1 
 |-  ( ph -> A =/= ( X L Y ) )
9 4 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> G e. TarskiG )
10 simp-4r 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> z e. P )
11 simpllr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> w e. P )
12 simpr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> z =/= w )
13 12 necomd 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> w =/= z )
14 11 13 eldifsnd 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> w e. ( P \ { z } ) )
15 5 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> X e. P )
16 6 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> Y e. ( P \ { X } ) )
17 simplr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> A = ( z L w ) )
18 8 ad4antr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> A =/= ( X L Y ) )
19 17 18 eqnetrrd 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( z L w ) =/= ( X L Y ) )
20 1 2 3 9 10 14 15 16 19 dfprlng2 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( ( z L w ) .|| ( X L Y ) <-> ( X ( ( hpG ` G ) ` ( z L w ) ) Y /\ ( ( z L w ) i^i ( X L Y ) ) = (/) ) ) )
21 17 breq1d 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( A .|| ( X L Y ) <-> ( z L w ) .|| ( X L Y ) ) )
22 17 fveq2d 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( ( hpG ` G ) ` A ) = ( ( hpG ` G ) ` ( z L w ) ) )
23 22 breqd 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( X ( ( hpG ` G ) ` A ) Y <-> X ( ( hpG ` G ) ` ( z L w ) ) Y ) )
24 17 ineq1d 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( A i^i ( X L Y ) ) = ( ( z L w ) i^i ( X L Y ) ) )
25 24 eqeq1d 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( ( A i^i ( X L Y ) ) = (/) <-> ( ( z L w ) i^i ( X L Y ) ) = (/) ) )
26 23 25 anbi12d 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( ( X ( ( hpG ` G ) ` A ) Y /\ ( A i^i ( X L Y ) ) = (/) ) <-> ( X ( ( hpG ` G ) ` ( z L w ) ) Y /\ ( ( z L w ) i^i ( X L Y ) ) = (/) ) ) )
27 20 21 26 3bitr4d 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ A = ( z L w ) ) /\ z =/= w ) -> ( A .|| ( X L Y ) <-> ( X ( ( hpG ` G ) ` A ) Y /\ ( A i^i ( X L Y ) ) = (/) ) ) )
28 27 anasss 
 |-  ( ( ( ( ph /\ z e. P ) /\ w e. P ) /\ ( A = ( z L w ) /\ z =/= w ) ) -> ( A .|| ( X L Y ) <-> ( X ( ( hpG ` G ) ` A ) Y /\ ( A i^i ( X L Y ) ) = (/) ) ) )
29 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
30 1 29 2 4 7 tgisline 
 |-  ( ph -> E. z e. P E. w e. P ( A = ( z L w ) /\ z =/= w ) )
31 28 30 r19.29vva 
 |-  ( ph -> ( A .|| ( X L Y ) <-> ( X ( ( hpG ` G ) ` A ) Y /\ ( A i^i ( X L Y ) ) = (/) ) ) )