Metamath Proof Explorer

Theorem prlngplngtr

Description: Transitivity of parallelism, for lines in the same plane H . This is case 1 of Theorem 12.15 of Schwabhauser p. 124. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses prlngpln4.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
prlngpln4.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlngpln4.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlngpln4.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
prlngpln4.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
prlngpln4.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
prlngplngtr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
prlngplngtr.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐻 )
prlngplngtr.b ⊢ ( 𝜑 → 𝐵 ∥ 𝐶 )
Assertion prlngplngtr ( 𝜑 → 𝐴 ∥ 𝐶 )

Proof

Step Hyp Ref Expression
1 prlngpln4.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
2 prlngpln4.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
3 prlngpln4.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 prlngpln4.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
5 prlngpln4.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
6 prlngpln4.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
7 prlngplngtr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
8 prlngplngtr.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐻 )
9 prlngplngtr.b ⊢ ( 𝜑 → 𝐵 ∥ 𝐶 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
11 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
13 11 2 3 9 prlngrcl2 ⊢ ( 𝜑 → 𝐶 ∈ ran ( LineG ‘ 𝐺 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐶 ∈ ran ( LineG ‘ 𝐺 ) )
15 11 1 2 12 14 prlngref ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐶 ∥ 𝐶 )
16 10 15 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∥ 𝐶 )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐺 ∈ TarskiG )
18 11 2 3 6 prlngrcl1 ⊢ ( 𝜑 → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
20 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐶 ∈ ran ( LineG ‘ 𝐺 ) )
21 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐻 ∈ ran 𝐸 )
22 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐴 ⊆ 𝐻 )
23 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐶 ⊆ 𝐻 )
24 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
25 11 1 2 17 19 20 21 22 23 24 prlngd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → 𝐴 ∥ 𝐶 )
26 25 stoic1a ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∥ 𝐶 ) → ¬ ( 𝐴 ∩ 𝐶 ) = ∅ )
27 26 neqned ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∥ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
29 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
30 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐺 ∈ TarskiG )
31 11 2 3 9 prlngrcl1 ⊢ ( 𝜑 → 𝐵 ∈ ran ( LineG ‘ 𝐺 ) )
32 31 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∈ ran ( LineG ‘ 𝐺 ) )
33 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
34 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
35 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) )
36 35 elin1d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐴 )
37 29 11 33 30 34 36 tglnpt ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
38 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐺 ∈ TarskiGE )
39 29 11 2 30 32 37 38 prlngmo2 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ∃* 𝑎 ∈ ran ( LineG ‘ 𝐺 ) ( 𝐵 ∥ 𝑎 ∧ 𝑥 ∈ 𝑎 ) )
40 breq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐵 ∥ 𝑎 ↔ 𝐵 ∥ 𝐴 ) )
41 eleq2w2 ⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐴 ) )
42 40 41 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐵 ∥ 𝑎 ∧ 𝑥 ∈ 𝑎 ) ↔ ( 𝐵 ∥ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) )
43 breq2 ⊢ ( 𝑎 = 𝐶 → ( 𝐵 ∥ 𝑎 ↔ 𝐵 ∥ 𝐶 ) )
44 eleq2w2 ⊢ ( 𝑎 = 𝐶 → ( 𝑥 ∈ 𝑎 ↔ 𝑥 ∈ 𝐶 ) )
45 43 44 anbi12d ⊢ ( 𝑎 = 𝐶 → ( ( 𝐵 ∥ 𝑎 ∧ 𝑥 ∈ 𝑎 ) ↔ ( 𝐵 ∥ 𝐶 ∧ 𝑥 ∈ 𝐶 ) ) )
46 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐶 ∈ ran ( LineG ‘ 𝐺 ) )
47 11 1 2 3 6 prlngsym ⊢ ( 𝜑 → 𝐵 ∥ 𝐴 )
48 47 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∥ 𝐴 )
49 48 36 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐵 ∥ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
50 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ∥ 𝐶 )
51 35 elin2d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐶 )
52 50 51 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐵 ∥ 𝐶 ∧ 𝑥 ∈ 𝐶 ) )
53 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐴 ≠ 𝐶 )
54 42 45 34 46 49 52 53 nrmod ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ¬ ∃* 𝑎 ∈ ran ( LineG ‘ 𝐺 ) ( 𝐵 ∥ 𝑎 ∧ 𝑥 ∈ 𝑎 ) )
55 39 54 pm2.21fal ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ) → ⊥ )
56 28 55 n0limd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ ¬ 𝐴 ∥ 𝐶 ) → ⊥ )
57 56 efald ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∥ 𝐶 )
58 16 57 pm2.61dane ⊢ ( 𝜑 → 𝐴 ∥ 𝐶 )