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 
|- 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 } ) )
dfprlng2.z 
|- ( ph -> Z e. P )
dfprlng2.w 
|- ( ph -> W e. ( P \ { Z } ) )
dfprlng2.1 
|- ( ph -> ( X L Y ) =/= ( Z L W ) )
Assertion dfprlng2 
|- ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( Z ( ( hpG ` G ) ` ( X L Y ) ) W /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) )

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 dfprlng2.z 
 |-  ( ph -> Z e. P )
8 dfprlng2.w 
 |-  ( ph -> W e. ( P \ { Z } ) )
9 dfprlng2.1 
 |-  ( ph -> ( X L Y ) =/= ( Z L W ) )
10 9 neneqd 
 |-  ( ph -> -. ( X L Y ) = ( Z L W ) )
11 biorf 
 |-  ( -. ( X L Y ) = ( Z L W ) -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) )
12 10 11 syl 
 |-  ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) )
13 12 anbi2d 
 |-  ( ph -> ( ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) )
14 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
15 6 eldifad 
 |-  ( ph -> Y e. P )
16 6 eldifsnbd 
 |-  ( ph -> Y =/= X )
17 16 necomd 
 |-  ( ph -> X =/= Y )
18 1 14 2 4 5 15 17 tgelrnln 
 |-  ( ph -> ( X L Y ) e. ran L )
19 8 eldifad 
 |-  ( ph -> W e. P )
20 8 eldifsnbd 
 |-  ( ph -> W =/= Z )
21 20 necomd 
 |-  ( ph -> Z =/= W )
22 1 14 2 4 7 19 21 tgelrnln 
 |-  ( ph -> ( Z L W ) e. ran L )
23 18 22 jca 
 |-  ( ph -> ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) )
24 23 biantrurd 
 |-  ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) )
25 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
26 2 25 3 4 brprlng 
 |-  ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( ( ( X L Y ) e. ran L /\ ( Z L W ) e. ran L ) /\ ( ( X L Y ) = ( Z L W ) \/ ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) ) ) )
27 13 24 26 3bitr4rd 
 |-  ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) )
28 4 ad4antr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> G e. TarskiG )
29 simpllr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> h e. ran ( PlnG ` G ) )
30 simplr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) C_ h )
31 simpr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( Z L W ) C_ h )
32 rspe 
 |-  ( ( h e. ran ( PlnG ` G ) /\ ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) )
33 29 30 31 32 syl12anc 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) )
34 simp-4r 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( ( X L Y ) i^i ( Z L W ) ) = (/) )
35 27 ad4antr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( ( X L Y ) .|| ( Z L W ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) )
36 33 34 35 mpbir2and 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) .|| ( Z L W ) )
37 9 ad4antr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> ( X L Y ) =/= ( Z L W ) )
38 1 14 2 4 7 19 21 tglinerflx1 
 |-  ( ph -> Z e. ( Z L W ) )
39 38 ad4antr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> Z e. ( Z L W ) )
40 1 14 2 4 7 19 21 tglinerflx2 
 |-  ( ph -> W e. ( Z L W ) )
41 40 ad4antr 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> W e. ( Z L W ) )
42 2 25 3 28 36 37 39 41 prlnghpg 
 |-  ( ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( X L Y ) C_ h ) /\ ( Z L W ) C_ h ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W )
43 42 anasss 
 |-  ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ h e. ran ( PlnG ` G ) ) /\ ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W )
44 43 r19.29an 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W )
45 sseq2 
 |-  ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( X L Y ) C_ h <-> ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) )
46 sseq2 
 |-  ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( Z L W ) C_ h <-> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) )
47 45 46 anbi12d 
 |-  ( h = ( ( X L Y ) ( PlnG ` G ) W ) -> ( ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) <-> ( ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) /\ ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) ) )
48 4 ad2antrr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> G e. TarskiG )
49 18 ad2antrr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( X L Y ) e. ran L )
50 19 ad2antrr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> W e. P )
51 nel02 
 |-  ( ( ( X L Y ) i^i ( Z L W ) ) = (/) -> -. W e. ( ( X L Y ) i^i ( Z L W ) ) )
52 51 ad2antlr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> -. W e. ( ( X L Y ) i^i ( Z L W ) ) )
53 simpr 
 |-  ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) /\ W e. ( X L Y ) ) -> W e. ( X L Y ) )
54 40 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) /\ W e. ( X L Y ) ) -> W e. ( Z L W ) )
55 53 54 elind 
 |-  ( ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) /\ W e. ( X L Y ) ) -> W e. ( ( X L Y ) i^i ( Z L W ) ) )
56 52 55 mtand 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> -. W e. ( X L Y ) )
57 50 56 eldifd 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> W e. ( P \ ( X L Y ) ) )
58 1 2 25 48 49 57 tgelrnpln 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( ( X L Y ) ( PlnG ` G ) W ) e. ran ( PlnG ` G ) )
59 1 14 2 25 48 49 57 elplnglnid 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) )
60 7 ad2antrr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> Z e. P )
61 simpr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> Z ( ( hpG ` G ) ` ( X L Y ) ) W )
62 1 2 25 49 60 57 48 61 hpgssplng 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> Z e. ( ( X L Y ) ( PlnG ` G ) W ) )
63 1 14 2 25 48 49 57 elplngid 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> W e. ( ( X L Y ) ( PlnG ` G ) W ) )
64 21 ad2antrr 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> Z =/= W )
65 1 14 2 25 48 58 62 63 64 lnssplng1 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) )
66 59 65 jca 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> ( ( X L Y ) C_ ( ( X L Y ) ( PlnG ` G ) W ) /\ ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) W ) ) )
67 47 58 66 rspcedvdw 
 |-  ( ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) -> E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) )
68 44 67 impbida 
 |-  ( ( ph /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) -> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) <-> Z ( ( hpG ` G ) ` ( X L Y ) ) W ) )
69 68 pm5.32da 
 |-  ( ph -> ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) <-> ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) ) )
70 ancom 
 |-  ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) ) <-> ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) )
71 ancom 
 |-  ( ( ( ( X L Y ) i^i ( Z L W ) ) = (/) /\ Z ( ( hpG ` G ) ` ( X L Y ) ) W ) <-> ( Z ( ( hpG ` G ) ` ( X L Y ) ) W /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) )
72 69 70 71 3bitr3g 
 |-  ( ph -> ( ( E. h e. ran ( PlnG ` G ) ( ( X L Y ) C_ h /\ ( Z L W ) C_ h ) /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) <-> ( Z ( ( hpG ` G ) ` ( X L Y ) ) W /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) )
73 27 72 bitrd 
 |-  ( ph -> ( ( X L Y ) .|| ( Z L W ) <-> ( Z ( ( hpG ` G ) ` ( X L Y ) ) W /\ ( ( X L Y ) i^i ( Z L W ) ) = (/) ) ) )