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 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
prlnginn0.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
prlnginn0.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlnginn0.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlnginn0.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
prlnginn0.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
prlnginn0.c ⊢ ( 𝜑 → 𝐶 ∈ ran 𝐿 )
prlnginn0.2 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
prlnginn0.3 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
prlnginn0.4 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
prlnginn0.5 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
prlnginn0.6 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
prlnginn0.7 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐻 )
Assertion prlnginn0 ( 𝜑 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 prlnginn0.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
2 prlnginn0.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
3 prlnginn0.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 prlnginn0.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 prlnginn0.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
6 prlnginn0.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7 prlnginn0.c ⊢ ( 𝜑 → 𝐶 ∈ ran 𝐿 )
8 prlnginn0.2 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
9 prlnginn0.3 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
10 prlnginn0.4 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
11 prlnginn0.5 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
12 prlnginn0.6 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
13 prlnginn0.7 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐻 )
14 8 neneqd ⊢ ( 𝜑 → ¬ ( 𝐴 ∩ 𝐶 ) = ∅ )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∥ 𝐶 ) → 𝐺 ∈ TarskiG )
16 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∥ 𝐶 ) → 𝐴 ∥ 𝐶 )
17 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∥ 𝐶 ) → 𝐴 ≠ 𝐶 )
18 1 3 15 16 17 prlngin0 ⊢ ( ( 𝜑 ∧ 𝐴 ∥ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
19 14 18 mtand ⊢ ( 𝜑 → ¬ 𝐴 ∥ 𝐶 )
20 4 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐺 ∈ TarskiG )
21 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐻 ∈ ran 𝐸 )
22 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐴 ⊆ 𝐻 )
23 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐴 ∥ 𝐵 )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐺 ∈ TarskiGE )
25 13 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐶 ⊆ 𝐻 )
26 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐵 ∥ 𝐶 )
27 2 3 20 21 22 23 24 25 26 prlngplngtr ⊢ ( ( 𝜑 ∧ 𝐵 ∥ 𝐶 ) → 𝐴 ∥ 𝐶 )
28 19 27 mtand ⊢ ( 𝜑 → ¬ 𝐵 ∥ 𝐶 )
29 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐺 ∈ TarskiG )
30 1 3 4 10 prlngrcl2 ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐵 ∈ ran 𝐿 )
32 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐶 ∈ ran 𝐿 )
33 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐻 ∈ ran 𝐸 )
34 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐵 ⊆ 𝐻 )
35 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐶 ⊆ 𝐻 )
36 simpr ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( 𝐵 ∩ 𝐶 ) = ∅ )
37 1 2 3 29 31 32 33 34 35 36 prlngd ⊢ ( ( 𝜑 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → 𝐵 ∥ 𝐶 )
38 28 37 mtand ⊢ ( 𝜑 → ¬ ( 𝐵 ∩ 𝐶 ) = ∅ )
39 38 neqned ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )