Metamath Proof Explorer

Theorem quadcgrprlng

Description: Nontrivial quadrilaterals with congruent and parallel opposite sides are parallelograms. Theorem 12.20 of Schwabhauser p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses quadcgrprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
quadcgrprlng.d ⊢ − = ( dist ‘ 𝐺 )
quadcgrprlng.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
quadcgrprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
quadcgrprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
quadcgrprlng.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
quadcgrprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
quadcgrprlng.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
quadcgrprlng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
quadcgrprlng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
quadcgrprlng.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
quadcgrprlng.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
quadcgrprlng.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
quadcgrprlng.3 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
quadcgrprlng.4 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
quadcgrprlng.5 ⊢ ( 𝜑 → 𝑌 𝑂 𝑊 )
Assertion quadcgrprlng ( 𝜑 → ( ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 quadcgrprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 quadcgrprlng.d ⊢ − = ( dist ‘ 𝐺 )
3 quadcgrprlng.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 quadcgrprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 quadcgrprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
6 quadcgrprlng.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
7 quadcgrprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 quadcgrprlng.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
9 quadcgrprlng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
10 quadcgrprlng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
11 quadcgrprlng.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
12 quadcgrprlng.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
13 quadcgrprlng.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
14 quadcgrprlng.3 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
15 quadcgrprlng.4 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
16 quadcgrprlng.5 ⊢ ( 𝜑 → 𝑌 𝑂 𝑊 )
17 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
18 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → 𝐺 ∈ TarskiG )
19 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → 𝐺 ∈ TarskiGE )
20 1 4 3 7 10 11 9 13 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
21 1 3 4 7 11 9 10 20 ncolne2 ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
22 21 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
23 1 3 4 7 10 11 22 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
24 23 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
25 13 orsild ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
26 9 25 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) )
27 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → 𝑋 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) )
28 1 4 17 18 24 27 tgelrnpln ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) ∈ ran ( hlG ‘ 𝐺 ) )
29 4 5 7 14 prlngrcl2 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
30 29 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
31 1 3 4 7 10 11 22 tglinerflx2 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
32 1 3 4 7 11 12 29 tglnne ⊢ ( 𝜑 → 𝑍 ≠ 𝑊 )
33 1 3 4 7 11 12 32 tglinerflx1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
34 31 33 elind ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
35 34 ne0d ⊢ ( 𝜑 → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑍 𝐿 𝑊 ) ) ≠ ∅ )
36 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑍 𝐿 𝑊 ) ) ≠ ∅ )
37 20 orsild ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
38 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
39 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
40 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiGE )
41 4 17 5 7 14 prlngsym ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ∥ ( 𝑋 𝐿 𝑌 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑍 𝐿 𝑊 ) ∥ ( 𝑋 𝐿 𝑌 ) )
43 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
44 4 17 5 39 43 prlngref ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑍 𝐿 𝑊 ) ∥ ( 𝑍 𝐿 𝑊 ) )
45 simpr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) )
46 44 45 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑍 𝐿 𝑊 ) ∥ ( 𝑌 𝐿 𝑍 ) )
47 1 3 4 7 9 10 11 13 ncolne1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
48 1 3 4 7 9 10 47 tglinerflx2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
50 1 3 4 7 10 11 22 tglinerflx1 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) )
52 1 5 39 40 42 46 49 51 prlngeq ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑍 ) )
53 38 52 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
54 37 53 mtand ⊢ ( 𝜑 → ¬ ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑊 ) )
55 54 neqned ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ≠ ( 𝑍 𝐿 𝑊 ) )
56 55 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑌 𝐿 𝑍 ) ≠ ( 𝑍 𝐿 𝑊 ) )
57 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 )
58 1 3 4 17 18 24 27 elplnglnid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑌 𝐿 𝑍 ) ⊆ ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
59 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → 𝑋 ∈ 𝑎 )
60 25 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
61 nelne1 ⊢ ( ( 𝑋 ∈ 𝑎 ∧ ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) → 𝑎 ≠ ( 𝑌 𝐿 𝑍 ) )
62 59 60 61 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → 𝑎 ≠ ( 𝑌 𝐿 𝑍 ) )
63 62 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑌 𝐿 𝑍 ) ≠ 𝑎 )
64 4 17 5 18 57 63 59 prlngpln3 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → 𝑎 ⊆ ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
65 1 3 4 7 9 10 11 12 13 tglineneq ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
66 4 17 5 7 14 65 33 prlngpln3 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑍 ) )
67 1 4 3 7 10 11 9 13 ncolcom ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
68 67 orsild ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) )
69 9 68 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
70 11 37 eldifd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
71 1 3 4 17 7 69 10 70 47 plngrot ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑍 ) = ( ( 𝑍 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
72 1 3 4 7 11 10 21 tglinecom ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑍 ) )
73 72 oveq1d ⊢ ( 𝜑 → ( ( 𝑍 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑋 ) = ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
74 71 73 eqtr2d ⊢ ( 𝜑 → ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) = ( ( 𝑋 𝐿 𝑌 ) ( hlG ‘ 𝐺 ) 𝑍 ) )
75 66 74 sseqtrrd ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
76 75 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑍 𝐿 𝑊 ) ⊆ ( ( 𝑌 𝐿 𝑍 ) ( hlG ‘ 𝐺 ) 𝑋 ) )
77 4 17 5 18 19 28 30 36 56 57 58 64 76 prlnginn0 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ≠ ∅ )
78 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 )
79 18 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝐺 ∈ TarskiG )
80 30 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
81 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) )
82 81 elin2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ∈ ( 𝑍 𝐿 𝑊 ) )
83 1 4 3 79 80 82 tglnpt ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ∈ 𝑃 )
84 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑋 ∈ 𝑃 )
85 33 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
86 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
87 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiGE )
88 1 3 4 7 9 10 47 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
90 4 17 5 86 89 prlngref ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑋 𝐿 𝑌 ) )
91 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
92 1 3 4 7 9 10 47 tglinerflx1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
94 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) )
95 1 5 86 87 90 91 93 94 prlngeq ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) )
96 85 95 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
97 37 96 mtand ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) )
98 97 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ¬ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) )
99 nelne2 ⊢ ( ( 𝑤 ∈ ( 𝑍 𝐿 𝑊 ) ∧ ¬ 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) ) → 𝑤 ≠ 𝑋 )
100 82 98 99 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ≠ 𝑋 )
101 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑎 ∈ ran 𝐿 )
102 81 elin1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ∈ 𝑎 )
103 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑋 ∈ 𝑎 )
104 1 3 4 79 83 84 100 100 101 102 103 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑎 = ( 𝑤 𝐿 𝑋 ) )
105 78 104 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑤 𝐿 𝑋 ) )
106 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
107 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑍 ∈ 𝑃 )
108 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑌 ∈ 𝑃 )
109 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑊 ∈ 𝑃 )
110 32 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑍 )
111 110 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑊 ≠ 𝑍 )
112 47 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑋 ≠ 𝑌 )
113 1 3 4 7 9 10 11 13 ncolne2 ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
114 1 3 4 7 9 11 113 tgelrnln ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
115 114 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
116 1 2 3 6 4 114 7 10 12 16 oppcom ⊢ ( 𝜑 → 𝑊 𝑂 𝑌 )
117 116 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑊 𝑂 𝑌 )
118 1 3 4 7 9 11 113 tglinerflx2 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) )
119 118 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) )
120 19 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝐺 ∈ TarskiGE )
121 13 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
122 14 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
123 25 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
124 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝑋 ∈ 𝑎 )
125 79 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝐺 ∈ TarskiG )
126 120 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝐺 ∈ TarskiGE )
127 4 17 5 7 23 prlngref ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑌 𝐿 𝑍 ) )
128 127 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑌 𝐿 𝑍 ) )
129 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 )
130 31 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
131 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝑍 = 𝑤 )
132 102 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝑤 ∈ 𝑎 )
133 131 132 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝑍 ∈ 𝑎 )
134 1 5 125 126 128 129 130 133 prlngeq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → ( 𝑌 𝐿 𝑍 ) = 𝑎 )
135 124 134 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) ∧ 𝑍 = 𝑤 ) → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
136 123 135 mtand ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ¬ 𝑍 = 𝑤 )
137 136 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑍 ≠ 𝑤 )
138 33 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
139 1 3 4 79 107 83 137 137 80 138 82 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑍 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑤 ) )
140 122 139 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑤 ) )
141 1 2 4 5 79 120 84 108 107 83 121 140 105 6 3 prlngsymquadopp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 𝑂 𝑌 )
142 1 3 4 7 11 12 32 tglinecom ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) = ( 𝑊 𝐿 𝑍 ) )
143 142 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑍 𝐿 𝑊 ) = ( 𝑊 𝐿 𝑍 ) )
144 82 143 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ∈ ( 𝑊 𝐿 𝑍 ) )
145 1 3 4 6 106 79 115 109 108 117 119 141 144 hlopp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 )
146 1 3 106 12 9 11 7 110 hlid ⊢ ( 𝜑 → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 )
147 146 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑍 ) 𝑊 )
148 1 2 4 5 79 120 84 108 107 83 121 140 105 prlngsymquad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑤 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑤 − 𝑋 ) ) )
149 148 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑤 ) )
150 149 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑍 − 𝑤 ) = ( 𝑋 − 𝑌 ) )
151 15 eqcomd ⊢ ( 𝜑 → ( 𝑍 − 𝑊 ) = ( 𝑋 − 𝑌 ) )
152 151 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑍 − 𝑊 ) = ( 𝑋 − 𝑌 ) )
153 1 2 106 107 84 108 79 109 111 112 145 147 150 152 hlcgreq ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → 𝑤 = 𝑊 )
154 153 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑤 𝐿 𝑋 ) = ( 𝑊 𝐿 𝑋 ) )
155 105 154 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
156 148 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑌 − 𝑍 ) = ( 𝑤 − 𝑋 ) )
157 153 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑤 − 𝑋 ) = ( 𝑊 − 𝑋 ) )
158 156 157 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
159 155 158 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) ∧ 𝑤 ∈ ( 𝑎 ∩ ( 𝑍 𝐿 𝑊 ) ) ) → ( ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )
160 77 159 n0limd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ) ∧ 𝑋 ∈ 𝑎 ) → ( ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )
161 160 anasss ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ∧ 𝑋 ∈ 𝑎 ) ) → ( ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )
162 1 4 5 7 23 9 prlngex ⊢ ( 𝜑 → ∃ 𝑎 ∈ ran 𝐿 ( ( 𝑌 𝐿 𝑍 ) ∥ 𝑎 ∧ 𝑋 ∈ 𝑎 ) )
163 161 162 r19.29a ⊢ ( 𝜑 → ( ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) ∧ ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) ) )