Metamath Proof Explorer

Theorem symquadprlnglem

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

Ref Expression
Hypotheses symquadprlnglem.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
symquadprlnglem.d ⊢ − = ( dist ‘ 𝐺 )
symquadprlnglem.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
symquadprlnglem.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
symquadprlnglem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
symquadprlnglem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
symquadprlnglem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
symquadprlnglem.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
symquadprlnglem.1 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
symquadprlnglem.2 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
symquadprlnglem.3 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
symquadprlnglem.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
symquadprlnglem.5 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑋 𝐿 𝑍 ) )
symquadprlnglem.6 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑌 𝐿 𝑊 ) )
Assertion symquadprlnglem ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 symquadprlnglem.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 symquadprlnglem.d ⊢ − = ( dist ‘ 𝐺 )
3 symquadprlnglem.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 symquadprlnglem.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 symquadprlnglem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 symquadprlnglem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 symquadprlnglem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 symquadprlnglem.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
9 symquadprlnglem.1 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑍 − 𝑊 ) )
10 symquadprlnglem.2 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑊 − 𝑋 ) )
11 symquadprlnglem.3 ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
12 symquadprlnglem.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑊 )
13 symquadprlnglem.5 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑋 𝐿 𝑍 ) )
14 symquadprlnglem.6 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑌 𝐿 𝑊 ) )
15 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
16 1 3 15 4 5 7 13 tglngne ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑋 ≠ 𝑍 )
18 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝐺 ∈ TarskiG )
19 1 15 3 4 6 8 12 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑊 ) ∈ ran 𝐿 )
20 1 3 15 4 19 14 tglnpt ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑇 ∈ 𝑃 )
22 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑍 ∈ 𝑃 )
23 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑋 ∈ 𝑃 )
24 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
25 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 )
26 13 orcd ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
27 14 orcd ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑌 𝐿 𝑊 ) ∨ 𝑌 = 𝑊 ) )
28 1 2 15 3 24 4 25 5 6 7 8 20 11 12 9 10 26 27 symquadlem ⊢ ( 𝜑 → 𝑋 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑍 ) )
29 28 oveq2d ⊢ ( 𝜑 → ( 𝑇 − 𝑋 ) = ( 𝑇 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑍 ) ) )
30 1 2 15 3 24 4 20 25 7 mircgr ⊢ ( 𝜑 → ( 𝑇 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑇 ) ‘ 𝑍 ) ) = ( 𝑇 − 𝑍 ) )
31 29 30 eqtr2d ⊢ ( 𝜑 → ( 𝑇 − 𝑍 ) = ( 𝑇 − 𝑋 ) )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → ( 𝑇 − 𝑍 ) = ( 𝑇 − 𝑋 ) )
33 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑇 = 𝑍 )
34 1 2 15 18 21 22 21 23 32 33 tgcgreq ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑇 = 𝑋 )
35 34 33 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → 𝑋 = 𝑍 )
36 nne ⊢ ( ¬ 𝑋 ≠ 𝑍 ↔ 𝑋 = 𝑍 )
37 35 36 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 = 𝑍 ) → ¬ 𝑋 ≠ 𝑍 )
38 17 37 pm2.65da ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ¬ 𝑇 = 𝑍 )
39 38 neqned ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝑇 ≠ 𝑍 )
40 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝐺 ∈ TarskiG )
41 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝑍 ∈ 𝑃 )
42 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝑋 ∈ 𝑃 )
43 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝑌 ∈ 𝑃 )
44 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝑇 ∈ 𝑃 )
45 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝐺 ∈ TarskiG )
46 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝑍 ∈ 𝑃 )
47 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝑌 ∈ 𝑃 )
48 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝑇 ∈ 𝑃 )
49 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝑊 ∈ 𝑃 )
50 1 15 3 4 6 8 12 tglinecom ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑊 ) = ( 𝑊 𝐿 𝑌 ) )
51 14 50 eleqtrd ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑊 𝐿 𝑌 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → 𝑇 ∈ ( 𝑊 𝐿 𝑌 ) )
53 simpr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
54 1 3 15 45 46 47 49 53 colcom ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ( 𝑊 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
55 1 15 3 45 48 49 47 46 52 54 coltr ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ( 𝑇 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
56 1 3 15 45 47 46 48 55 colcom ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ( 𝑇 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
57 1 3 15 45 46 47 48 56 colrot2 ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ( 𝑌 ∈ ( 𝑇 𝐿 𝑍 ) ∨ 𝑇 = 𝑍 ) )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → ( 𝑌 ∈ ( 𝑇 𝐿 𝑍 ) ∨ 𝑇 = 𝑍 ) )
59 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝑇 ≠ 𝑍 )
60 59 neneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → ¬ 𝑇 = 𝑍 )
61 58 60 olcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → 𝑌 ∈ ( 𝑇 𝐿 𝑍 ) )
62 1 3 15 4 5 7 20 26 colcom ⊢ ( 𝜑 → ( 𝑇 ∈ ( 𝑍 𝐿 𝑋 ) ∨ 𝑍 = 𝑋 ) )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → ( 𝑇 ∈ ( 𝑍 𝐿 𝑋 ) ∨ 𝑍 = 𝑋 ) )
64 1 15 3 40 43 44 41 42 61 63 coltr ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → ( 𝑌 ∈ ( 𝑍 𝐿 𝑋 ) ∨ 𝑍 = 𝑋 ) )
65 1 3 15 40 41 42 43 64 colrot2 ⊢ ( ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) ∧ 𝑇 ≠ 𝑍 ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
66 39 65 mpdan ⊢ ( ( 𝜑 ∧ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
67 11 66 mtand ⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )