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 
|- E = ( PlnG ` G )
prlngpln4.p 
|- .|| = ( parlnG ` G )
prlngpln4.g 
|- ( ph -> G e. TarskiG )
prlngpln4.h 
|- ( ph -> H e. ran E )
prlngpln4.a 
|- ( ph -> A C_ H )
prlngpln4.1 
|- ( ph -> A .|| B )
prlngplngtr.g 
|- ( ph -> G e. TarskiGE )
prlngplngtr.c 
|- ( ph -> C C_ H )
prlngplngtr.b 
|- ( ph -> B .|| C )
Assertion prlngplngtr 
|- ( ph -> A .|| C )

Proof

Step Hyp Ref Expression
1 prlngpln4.e 
 |-  E = ( PlnG ` G )
2 prlngpln4.p 
 |-  .|| = ( parlnG ` G )
3 prlngpln4.g 
 |-  ( ph -> G e. TarskiG )
4 prlngpln4.h 
 |-  ( ph -> H e. ran E )
5 prlngpln4.a 
 |-  ( ph -> A C_ H )
6 prlngpln4.1 
 |-  ( ph -> A .|| B )
7 prlngplngtr.g 
 |-  ( ph -> G e. TarskiGE )
8 prlngplngtr.c 
 |-  ( ph -> C C_ H )
9 prlngplngtr.b 
 |-  ( ph -> B .|| C )
10 simpr 
 |-  ( ( ph /\ A = C ) -> A = C )
11 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
12 3 adantr 
 |-  ( ( ph /\ A = C ) -> G e. TarskiG )
13 11 2 3 9 prlngrcl2 
 |-  ( ph -> C e. ran ( LineG ` G ) )
14 13 adantr 
 |-  ( ( ph /\ A = C ) -> C e. ran ( LineG ` G ) )
15 11 1 2 12 14 prlngref 
 |-  ( ( ph /\ A = C ) -> C .|| C )
16 10 15 eqbrtrd 
 |-  ( ( ph /\ A = C ) -> A .|| C )
17 3 adantr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> G e. TarskiG )
18 11 2 3 6 prlngrcl1 
 |-  ( ph -> A e. ran ( LineG ` G ) )
19 18 adantr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> A e. ran ( LineG ` G ) )
20 13 adantr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> C e. ran ( LineG ` G ) )
21 4 adantr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> H e. ran E )
22 5 adantr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> A C_ H )
23 8 adantr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> C C_ H )
24 simpr 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> ( A i^i C ) = (/) )
25 11 1 2 17 19 20 21 22 23 24 prlngd 
 |-  ( ( ph /\ ( A i^i C ) = (/) ) -> A .|| C )
26 25 stoic1a 
 |-  ( ( ph /\ -. A .|| C ) -> -. ( A i^i C ) = (/) )
27 26 neqned 
 |-  ( ( ph /\ -. A .|| C ) -> ( A i^i C ) =/= (/) )
28 27 adantlr 
 |-  ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) -> ( A i^i C ) =/= (/) )
29 eqid 
 |-  ( Base ` G ) = ( Base ` G )
30 3 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> G e. TarskiG )
31 11 2 3 9 prlngrcl1 
 |-  ( ph -> B e. ran ( LineG ` G ) )
32 31 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> B e. ran ( LineG ` G ) )
33 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
34 18 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> A e. ran ( LineG ` G ) )
35 simpr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> x e. ( A i^i C ) )
36 35 elin1d 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> x e. A )
37 29 11 33 30 34 36 tglnpt 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> x e. ( Base ` G ) )
38 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> G e. TarskiGE )
39 29 11 2 30 32 37 38 prlngmo2 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> E* a e. ran ( LineG ` G ) ( B .|| a /\ x e. a ) )
40 breq2 
 |-  ( a = A -> ( B .|| a <-> B .|| A ) )
41 eleq2w2 
 |-  ( a = A -> ( x e. a <-> x e. A ) )
42 40 41 anbi12d 
 |-  ( a = A -> ( ( B .|| a /\ x e. a ) <-> ( B .|| A /\ x e. A ) ) )
43 breq2 
 |-  ( a = C -> ( B .|| a <-> B .|| C ) )
44 eleq2w2 
 |-  ( a = C -> ( x e. a <-> x e. C ) )
45 43 44 anbi12d 
 |-  ( a = C -> ( ( B .|| a /\ x e. a ) <-> ( B .|| C /\ x e. C ) ) )
46 13 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> C e. ran ( LineG ` G ) )
47 11 1 2 3 6 prlngsym 
 |-  ( ph -> B .|| A )
48 47 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> B .|| A )
49 48 36 jca 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> ( B .|| A /\ x e. A ) )
50 9 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> B .|| C )
51 35 elin2d 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> x e. C )
52 50 51 jca 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> ( B .|| C /\ x e. C ) )
53 simpllr 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> A =/= C )
54 42 45 34 46 49 52 53 nrmod 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> -. E* a e. ran ( LineG ` G ) ( B .|| a /\ x e. a ) )
55 39 54 pm2.21fal 
 |-  ( ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) /\ x e. ( A i^i C ) ) -> F. )
56 28 55 n0limd 
 |-  ( ( ( ph /\ A =/= C ) /\ -. A .|| C ) -> F. )
57 56 efald 
 |-  ( ( ph /\ A =/= C ) -> A .|| C )
58 16 57 pm2.61dane 
 |-  ( ph -> A .|| C )