Metamath Proof Explorer

Theorem prlnginn0

Description: A line C intersecting another line A also intersects any line B parallel to A . Theorem 12.16 of Schwabhauser p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses prlnginn0.l 
|- L = ( LineG ` G )
prlnginn0.e 
|- E = ( PlnG ` G )
prlnginn0.p 
|- .|| = ( parlnG ` G )
prlnginn0.g 
|- ( ph -> G e. TarskiG )
prlnginn0.1 
|- ( ph -> G e. TarskiGE )
prlnginn0.h 
|- ( ph -> H e. ran E )
prlnginn0.c 
|- ( ph -> C e. ran L )
prlnginn0.2 
|- ( ph -> ( A i^i C ) =/= (/) )
prlnginn0.3 
|- ( ph -> A =/= C )
prlnginn0.4 
|- ( ph -> A .|| B )
prlnginn0.5 
|- ( ph -> A C_ H )
prlnginn0.6 
|- ( ph -> B C_ H )
prlnginn0.7 
|- ( ph -> C C_ H )
Assertion prlnginn0 
|- ( ph -> ( B i^i C ) =/= (/) )

Proof

Step Hyp Ref Expression
1 prlnginn0.l 
 |-  L = ( LineG ` G )
2 prlnginn0.e 
 |-  E = ( PlnG ` G )
3 prlnginn0.p 
 |-  .|| = ( parlnG ` G )
4 prlnginn0.g 
 |-  ( ph -> G e. TarskiG )
5 prlnginn0.1 
 |-  ( ph -> G e. TarskiGE )
6 prlnginn0.h 
 |-  ( ph -> H e. ran E )
7 prlnginn0.c 
 |-  ( ph -> C e. ran L )
8 prlnginn0.2 
 |-  ( ph -> ( A i^i C ) =/= (/) )
9 prlnginn0.3 
 |-  ( ph -> A =/= C )
10 prlnginn0.4 
 |-  ( ph -> A .|| B )
11 prlnginn0.5 
 |-  ( ph -> A C_ H )
12 prlnginn0.6 
 |-  ( ph -> B C_ H )
13 prlnginn0.7 
 |-  ( ph -> C C_ H )
14 8 neneqd 
 |-  ( ph -> -. ( A i^i C ) = (/) )
15 4 adantr 
 |-  ( ( ph /\ A .|| C ) -> G e. TarskiG )
16 simpr 
 |-  ( ( ph /\ A .|| C ) -> A .|| C )
17 9 adantr 
 |-  ( ( ph /\ A .|| C ) -> A =/= C )
18 1 3 15 16 17 prlngin0 
 |-  ( ( ph /\ A .|| C ) -> ( A i^i C ) = (/) )
19 14 18 mtand 
 |-  ( ph -> -. A .|| C )
20 4 adantr 
 |-  ( ( ph /\ B .|| C ) -> G e. TarskiG )
21 6 adantr 
 |-  ( ( ph /\ B .|| C ) -> H e. ran E )
22 11 adantr 
 |-  ( ( ph /\ B .|| C ) -> A C_ H )
23 10 adantr 
 |-  ( ( ph /\ B .|| C ) -> A .|| B )
24 5 adantr 
 |-  ( ( ph /\ B .|| C ) -> G e. TarskiGE )
25 13 adantr 
 |-  ( ( ph /\ B .|| C ) -> C C_ H )
26 simpr 
 |-  ( ( ph /\ B .|| C ) -> B .|| C )
27 2 3 20 21 22 23 24 25 26 prlngplngtr 
 |-  ( ( ph /\ B .|| C ) -> A .|| C )
28 19 27 mtand 
 |-  ( ph -> -. B .|| C )
29 4 adantr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> G e. TarskiG )
30 1 3 4 10 prlngrcl2 
 |-  ( ph -> B e. ran L )
31 30 adantr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> B e. ran L )
32 7 adantr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> C e. ran L )
33 6 adantr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> H e. ran E )
34 12 adantr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> B C_ H )
35 13 adantr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> C C_ H )
36 simpr 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> ( B i^i C ) = (/) )
37 1 2 3 29 31 32 33 34 35 36 prlngd 
 |-  ( ( ph /\ ( B i^i C ) = (/) ) -> B .|| C )
38 28 37 mtand 
 |-  ( ph -> -. ( B i^i C ) = (/) )
39 38 neqned 
 |-  ( ph -> ( B i^i C ) =/= (/) )