Metamath Proof Explorer

Theorem prlngsymquadlem

Description: Lemma for prlngsymquad . (Contributed by Thierry Arnoux, 20-Jul-2026)

Ref Expression
Hypotheses symquadprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
symquadprlng.d ⊢ − = ( dist ‘ 𝐺 )
symquadprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
symquadprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
symquadprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
symquadprlng.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
symquadprlng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
symquadprlng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
symquadprlng.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
symquadprlng.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
prlngsymquad.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
prlngsymquad.3 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
prlngsymquad.4 ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
prlngsymquadlem.t ⊢ 𝑇 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 )
Assertion prlngsymquadlem ( 𝜑 → 𝑇 = 𝑊 )

Proof

Step Hyp Ref Expression
1 symquadprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 symquadprlng.d ⊢ − = ( dist ‘ 𝐺 )
3 symquadprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 symquadprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
5 symquadprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 symquadprlng.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
7 symquadprlng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
8 symquadprlng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
9 symquadprlng.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
10 symquadprlng.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 prlngsymquad.2 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
12 prlngsymquad.3 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
13 prlngsymquad.4 ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
14 prlngsymquadlem.t ⊢ 𝑇 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 )
15 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
16 3 4 5 13 prlngrcl2 ⊢ ( 𝜑 → ( 𝑊 𝐿 𝑋 ) ∈ ran 𝐿 )
17 1 15 3 5 10 7 16 tglnne ⊢ ( 𝜑 → 𝑊 ≠ 𝑋 )
18 1 15 3 5 10 7 17 tglinecom ⊢ ( 𝜑 → ( 𝑊 𝐿 𝑋 ) = ( 𝑋 𝐿 𝑊 ) )
19 18 16 eqeltrrd ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑊 ) ∈ ran 𝐿 )
20 3 4 5 12 prlngrcl2 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑊 ) ∈ ran 𝐿 )
21 1 15 3 5 7 8 9 10 11 tglineneq ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
22 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → 𝐺 ∈ TarskiG )
23 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
24 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
25 3 4 22 23 24 prlngin0 ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ )
26 1 15 3 5 7 8 9 11 ncolne1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
27 1 15 3 5 7 8 26 tglinerflx1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
28 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
29 17 necomd ⊢ ( 𝜑 → 𝑋 ≠ 𝑊 )
30 1 15 3 5 7 10 29 tglinerflx1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑊 ) )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑊 ) )
32 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) )
33 31 32 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → 𝑋 ∈ ( 𝑍 𝐿 𝑊 ) )
34 28 33 elind ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → 𝑋 ∈ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
35 34 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) ≠ ∅ )
36 35 neneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) ∧ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ) → ¬ ( ( 𝑋 𝐿 𝑌 ) ∩ ( 𝑍 𝐿 𝑊 ) ) = ∅ )
37 25 36 pm2.65da ⊢ ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) → ¬ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) )
38 nne ⊢ ( ¬ ( 𝑋 𝐿 𝑌 ) ≠ ( 𝑍 𝐿 𝑊 ) ↔ ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) )
39 37 38 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 𝐿 𝑊 ) = ( 𝑍 𝐿 𝑊 ) ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑍 𝐿 𝑊 ) )
40 21 39 mteqand ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑊 ) ≠ ( 𝑍 𝐿 𝑊 ) )
41 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
42 1 3 15 5 8 9 7 11 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
43 1 2 15 5 42 7 9 midcl ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ 𝑃 )
44 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
45 1 2 15 3 41 5 43 44 8 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ∈ 𝑃 )
46 14 45 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
47 3 4 5 13 prlngrcl1 ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
48 1 15 3 5 8 9 47 tglnne ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
49 48 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
50 1 41 44 5 43 9 8 mirleqb ⊢ ( 𝜑 → ( 𝑍 = 𝑌 ↔ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) )
51 50 necon3bid ⊢ ( 𝜑 → ( 𝑍 ≠ 𝑌 ↔ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) )
52 49 51 mpbid ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) )
53 eqidd ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
54 1 2 15 5 42 7 9 41 43 ismidb ⊢ ( 𝜑 → ( 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) ↔ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) )
55 53 54 mpbird ⊢ ( 𝜑 → 𝑍 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) )
56 55 eqcomd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) = 𝑍 )
57 1 2 15 3 41 5 43 44 7 56 mircom ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑍 ) = 𝑋 )
58 14 eqcomi ⊢ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) = 𝑇
59 58 a1i ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) = 𝑇 )
60 52 57 59 3netr3d ⊢ ( 𝜑 → 𝑋 ≠ 𝑇 )
61 1 15 3 5 7 46 60 tglinerflx2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑋 𝐿 𝑇 ) )
62 1 41 44 5 43 7 8 mirleqb ⊢ ( 𝜑 → ( 𝑋 = 𝑌 ↔ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) )
63 62 necon3bid ⊢ ( 𝜑 → ( 𝑋 ≠ 𝑌 ↔ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ) )
64 26 63 mpbid ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑋 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) )
65 64 56 59 3netr3d ⊢ ( 𝜑 → 𝑍 ≠ 𝑇 )
66 1 15 3 5 9 46 65 tglinerflx2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑍 𝐿 𝑇 ) )
67 61 66 elind ⊢ ( 𝜑 → 𝑇 ∈ ( ( 𝑋 𝐿 𝑇 ) ∩ ( 𝑍 𝐿 𝑇 ) ) )
68 1 15 3 5 8 9 48 tglinecom ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑌 ) )
69 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
70 eqid ⊢ ( midG ‘ 𝐺 ) = ( midG ‘ 𝐺 )
71 1 3 15 5 8 9 7 11 ncolcom ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
72 71 orsild ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) )
73 7 72 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ ( 𝑍 𝐿 𝑌 ) ) )
74 1 2 15 5 42 9 7 midcom ⊢ ( 𝜑 → ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
75 1 2 15 5 42 8 46 41 43 ismidb ⊢ ( 𝜑 → ( 𝑇 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ↔ ( 𝑌 ( midG ‘ 𝐺 ) 𝑇 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) )
76 14 75 mpbii ⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑇 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
77 76 eqcomd ⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) = ( 𝑌 ( midG ‘ 𝐺 ) 𝑇 ) )
78 74 77 eqtrd ⊢ ( 𝜑 → ( 𝑍 ( midG ‘ 𝐺 ) 𝑋 ) = ( 𝑌 ( midG ‘ 𝐺 ) 𝑇 ) )
79 1 3 69 4 70 5 6 9 8 73 46 78 49 prlngmid2 ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑌 ) ∥ ( 𝑋 𝐿 𝑇 ) )
80 68 79 eqbrtrd ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑋 𝐿 𝑇 ) )
81 13 18 breqtrd ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑋 𝐿 𝑊 ) )
82 1 15 3 5 7 46 60 tglinerflx1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑇 ) )
83 1 4 5 6 80 81 82 30 prlngeq ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑇 ) = ( 𝑋 𝐿 𝑊 ) )
84 1 3 15 5 8 9 7 11 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) )
85 84 orsild ⊢ ( 𝜑 → ¬ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) )
86 9 85 eldifd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
87 1 3 69 4 70 5 6 7 8 86 46 77 26 prlngmid2 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑇 ) )
88 1 15 3 5 9 46 65 tglinerflx1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑍 𝐿 𝑇 ) )
89 1 15 3 5 9 10 20 tglnne ⊢ ( 𝜑 → 𝑍 ≠ 𝑊 )
90 1 15 3 5 9 10 89 tglinerflx1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑍 𝐿 𝑊 ) )
91 1 4 5 6 87 12 88 90 prlngeq ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑇 ) = ( 𝑍 𝐿 𝑊 ) )
92 83 91 ineq12d ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑇 ) ∩ ( 𝑍 𝐿 𝑇 ) ) = ( ( 𝑋 𝐿 𝑊 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
93 67 92 eleqtrd ⊢ ( 𝜑 → 𝑇 ∈ ( ( 𝑋 𝐿 𝑊 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
94 1 15 3 5 7 10 29 tglinerflx2 ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑋 𝐿 𝑊 ) )
95 1 15 3 5 9 10 89 tglinerflx2 ⊢ ( 𝜑 → 𝑊 ∈ ( 𝑍 𝐿 𝑊 ) )
96 94 95 elind ⊢ ( 𝜑 → 𝑊 ∈ ( ( 𝑋 𝐿 𝑊 ) ∩ ( 𝑍 𝐿 𝑊 ) ) )
97 1 15 3 5 19 20 40 93 96 tglineineq ⊢ ( 𝜑 → 𝑇 = 𝑊 )