Metamath Proof Explorer

Theorem angmgmaddeu1

Description: There exists a unique point s satisfying the conditions of angle addition. General case. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmgmadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
angmgmadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
angmgmadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
angmgmadd.d ⊢ − = ( dist ‘ 𝐺 )
angmgmadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
angmgmadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
angmgmadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
angmgmaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
angmgmaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
angmgmaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
angmgmaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
angmgmaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
angmgmaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
angmgmaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
angmgmaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
angmgmaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
angmgmaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
angmgmaddeu1.1 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
angmgmaddeu1.2 ⊢ ( 𝜑 → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
Assertion angmgmaddeu1 ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 angmgmadd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 angmgmadd.a ⊢ 𝐴 = { 𝑑 ∈ ( 𝑃 ↑m ( 0 ..^ 3 ) ) ∣ ( ( 𝑑 ‘ 0 ) ≠ ( 𝑑 ‘ 1 ) ∧ ( 𝑑 ‘ 1 ) ≠ ( 𝑑 ‘ 2 ) ) }
3 angmgmadd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 angmgmadd.d ⊢ − = ( dist ‘ 𝐺 )
5 angmgmadd.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
6 angmgmadd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
7 angmgmadd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 angmgmaddov.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
9 angmgmaddov.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
10 angmgmaddov.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11 angmgmaddov.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 angmgmaddov.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 angmgmaddov.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
14 angmgmaddeu.1 ⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
15 angmgmaddeu.2 ⊢ ( 𝜑 → 𝑉 ≠ 𝑊 )
16 angmgmaddeu.3 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
17 angmgmaddeu.4 ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
18 angmgmaddeu1.1 ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
19 angmgmaddeu1.2 ⊢ ( 𝜑 → ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) )
20 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
21 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝐺 ∈ TarskiG )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑤 ∈ 𝑃 )
23 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑉 ∈ 𝑃 )
24 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑈 ∈ 𝑃 )
25 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑍 ∈ 𝑃 )
26 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑌 ∈ 𝑃 )
27 15 neneqd ⊢ ( 𝜑 → ¬ 𝑉 = 𝑊 )
28 ioran ⊢ ( ¬ ( 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ∨ 𝑉 = 𝑊 ) ↔ ( ¬ 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ∧ ¬ 𝑉 = 𝑊 ) )
29 19 27 28 sylanbrc ⊢ ( 𝜑 → ¬ ( 𝑈 ∈ ( 𝑉 𝐿 𝑊 ) ∨ 𝑉 = 𝑊 ) )
30 1 6 3 7 9 10 8 29 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝑊 ∈ ( 𝑈 𝐿 𝑉 ) ∨ 𝑈 = 𝑉 ) )
31 1 6 3 7 8 9 10 30 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
32 eqid ⊢ ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) = ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) )
33 1 3 6 7 12 13 17 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
34 1 4 3 7 31 32 6 33 11 lmicl ⊢ ( 𝜑 → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ 𝑃 )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ 𝑃 )
36 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ¬ ( 𝑊 ∈ ( 𝑈 𝐿 𝑉 ) ∨ 𝑈 = 𝑉 ) )
37 21 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝐺 ∈ TarskiG )
38 23 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑉 ∈ 𝑃 )
39 24 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑈 ∈ 𝑃 )
40 14 neneqd ⊢ ( 𝜑 → ¬ 𝑈 = 𝑉 )
41 40 neqcomd ⊢ ( 𝜑 → ¬ 𝑉 = 𝑈 )
42 41 neqned ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
43 42 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑉 ≠ 𝑈 )
44 22 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑤 ∈ 𝑃 )
45 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) )
46 45 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ( 𝑌 − 𝑍 ) = ( 𝑉 − 𝑤 ) )
47 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑌 ≠ 𝑍 )
48 1 4 3 21 26 25 23 22 46 47 tgcgrneq ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑉 ≠ 𝑤 )
49 48 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑤 ≠ 𝑉 )
50 49 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑤 ≠ 𝑉 )
51 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) )
52 41 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → ¬ 𝑉 = 𝑈 )
53 51 52 olcnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) )
54 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑊 ∈ 𝑃 )
55 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑊 ∈ 𝑃 )
56 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
57 1 3 20 22 55 23 21 56 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑤 )
58 1 3 20 55 22 23 21 6 57 hlln ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑊 ∈ ( 𝑤 𝐿 𝑉 ) )
59 1 3 6 21 23 22 55 48 58 lncom ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑊 ∈ ( 𝑉 𝐿 𝑤 ) )
60 59 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑊 ∈ ( 𝑉 𝐿 𝑤 ) )
61 1 3 6 37 38 39 43 44 50 53 54 60 tglineeltr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑊 ∈ ( 𝑉 𝐿 𝑈 ) )
62 1 3 6 7 9 8 42 tglinecom ⊢ ( 𝜑 → ( 𝑉 𝐿 𝑈 ) = ( 𝑈 𝐿 𝑉 ) )
63 62 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → ( 𝑉 𝐿 𝑈 ) = ( 𝑈 𝐿 𝑉 ) )
64 61 63 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → 𝑊 ∈ ( 𝑈 𝐿 𝑉 ) )
65 64 orcd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) ) → ( 𝑊 ∈ ( 𝑈 𝐿 𝑉 ) ∨ 𝑈 = 𝑉 ) )
66 36 65 mtand ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ¬ ( 𝑤 ∈ ( 𝑉 𝐿 𝑈 ) ∨ 𝑉 = 𝑈 ) )
67 eleq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) )
68 67 adantr ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ↔ 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) )
69 eleq1 ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) )
70 69 adantl ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ↔ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) )
71 68 70 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ↔ ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ) )
72 oveq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑐 𝐼 𝑑 ) )
73 72 eleq2d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
74 73 rexbidv ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ) )
75 eleq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ↔ 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
76 75 cbvrexvw ⊢ ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑐 𝐼 𝑑 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑍 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) )
77 74 76 bitrdi ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑍 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) )
78 71 77 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑍 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) ) )
79 78 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑌 𝐿 𝑍 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
80 1 4 3 6 7 31 33 79 32 11 18 lmiopp ⊢ ( 𝜑 → 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
81 1 4 3 79 6 33 7 11 34 80 oppne2 ⊢ ( 𝜑 → ¬ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ ( 𝑌 𝐿 𝑍 ) )
82 1 3 6 7 12 13 17 tglinecom ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑌 ) )
83 81 82 neleqtrd ⊢ ( 𝜑 → ¬ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ ( 𝑍 𝐿 𝑌 ) )
84 17 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
85 84 neneqd ⊢ ( 𝜑 → ¬ 𝑍 = 𝑌 )
86 ioran ⊢ ( ¬ ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) ↔ ( ¬ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ ( 𝑍 𝐿 𝑌 ) ∧ ¬ 𝑍 = 𝑌 ) )
87 83 85 86 sylanbrc ⊢ ( 𝜑 → ¬ ( ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
88 1 6 3 7 13 12 34 87 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝑍 ∈ ( 𝑌 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) ∨ 𝑌 = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) )
89 88 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ¬ ( 𝑍 ∈ ( 𝑌 𝐿 ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) ∨ 𝑌 = ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) )
90 1 4 3 21 23 22 26 25 45 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ( 𝑤 − 𝑉 ) = ( 𝑍 − 𝑌 ) )
91 1 4 3 6 20 21 22 23 24 25 26 35 66 89 90 trgcopyeu ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) )
92 5 eqcomi ⊢ ( cgrA ‘ 𝐺 ) = ∼
93 92 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
94 21 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝐺 ∈ TarskiG )
95 25 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑍 ∈ 𝑃 )
96 26 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑌 ∈ 𝑃 )
97 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑠 ∈ 𝑃 )
98 24 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑈 ∈ 𝑃 )
99 23 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑉 ∈ 𝑃 )
100 22 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑤 ∈ 𝑃 )
101 14 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑈 ≠ 𝑉 )
102 48 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑉 ≠ 𝑤 )
103 1 3 94 20 98 99 100 101 102 cgraswap ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑈 𝑉 𝑤 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑤 𝑉 𝑈 ”⟩ )
104 49 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑤 ≠ 𝑉 )
105 42 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑉 ≠ 𝑈 )
106 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
107 1 3 94 20 100 99 98 95 96 97 104 105 106 cgrcgra ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
108 1 3 94 20 98 99 100 100 99 98 103 95 96 97 107 cgratr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑈 𝑉 𝑤 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
109 1 3 94 20 98 99 100 95 96 97 108 cgracom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑤 ”⟩ )
110 55 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑊 ∈ 𝑃 )
111 57 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑊 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑤 )
112 1 3 20 94 95 96 97 98 99 100 109 110 111 cgrahl2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
113 93 112 breqdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
114 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
115 1 4 3 114 94 100 99 98 95 96 97 106 cgr3simp2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( 𝑉 − 𝑈 ) = ( 𝑌 − 𝑠 ) )
116 115 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
117 33 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
118 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → 𝑋 ∈ 𝑃 )
119 118 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑋 ∈ 𝑃 )
120 35 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ 𝑃 )
121 eqidd ⊢ ( 𝜑 → ( hpG ‘ 𝐺 ) = ( hpG ‘ 𝐺 ) )
122 121 82 fveq12d ⊢ ( 𝜑 → ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) )
123 122 eqcomd ⊢ ( 𝜑 → ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) )
124 123 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) )
125 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
126 124 125 breqdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
127 1 3 6 94 117 97 79 120 126 hpgcom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) 𝑠 )
128 21 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → 𝐺 ∈ TarskiG )
129 33 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
130 35 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ 𝑃 )
131 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → 𝑠 ∈ 𝑃 )
132 118 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → 𝑋 ∈ 𝑃 )
133 80 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
134 1 4 3 79 6 129 128 132 130 133 oppcom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 )
135 1 3 6 79 128 129 130 131 132 134 lnopp2hpgb ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) → ( 𝑠 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ↔ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) 𝑠 ) )
136 135 adantr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( 𝑠 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ↔ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) 𝑠 ) )
137 127 136 mpbird ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → 𝑠 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 )
138 1 3 6 79 94 117 97 119 137 lnoppinn0 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ )
139 113 116 138 3jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ) ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
140 139 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) ) → ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
141 21 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝐺 ∈ TarskiG )
142 22 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑤 ∈ 𝑃 )
143 23 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑉 ∈ 𝑃 )
144 24 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑈 ∈ 𝑃 )
145 25 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑍 ∈ 𝑃 )
146 26 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑌 ∈ 𝑃 )
147 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ∈ 𝑃 )
148 90 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑤 − 𝑉 ) = ( 𝑍 − 𝑌 ) )
149 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) )
150 149 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑉 − 𝑈 ) = ( 𝑌 − 𝑠 ) )
151 55 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑊 ∈ 𝑃 )
152 42 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑉 ≠ 𝑈 )
153 1 4 3 141 143 144 146 147 150 152 tgcgrneq ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑌 ≠ 𝑠 )
154 153 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ≠ 𝑌 )
155 47 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑌 ≠ 𝑍 )
156 1 3 141 20 147 146 145 154 155 cgraswap ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑠 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
157 5 a1i ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ∼ = ( cgrA ‘ 𝐺 ) )
158 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
159 157 158 breqdi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑍 𝑌 𝑠 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
160 1 3 141 20 147 146 145 145 146 147 156 144 143 151 159 cgratr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑠 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
161 1 3 141 20 147 146 145 144 143 151 160 cgracom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑈 𝑉 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑠 𝑌 𝑍 ”⟩ )
162 118 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑋 ∈ 𝑃 )
163 14 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑈 ≠ 𝑉 )
164 1 3 20 144 162 143 141 163 hlid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑈 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑈 )
165 56 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 )
166 45 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) )
167 1 3 20 141 144 143 151 147 146 145 161 144 4 142 164 165 150 166 cgracgr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑈 − 𝑤 ) = ( 𝑠 − 𝑍 ) )
168 1 4 114 141 142 143 144 145 146 147 148 150 167 trgcgr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ )
169 122 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) )
170 33 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
171 35 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ∈ 𝑃 )
172 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ )
173 147 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → 𝑠 ∈ 𝑃 )
174 162 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → 𝑋 ∈ 𝑃 )
175 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) )
176 175 elin1d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → 𝑟 ∈ ( 𝑌 𝐿 𝑍 ) )
177 36 ad4antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ¬ ( 𝑊 ∈ ( 𝑈 𝐿 𝑉 ) ∨ 𝑈 = 𝑉 ) )
178 1 3 4 141 144 143 151 147 146 145 161 6 177 cgrancol ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ¬ ( 𝑍 ∈ ( 𝑠 𝐿 𝑌 ) ∨ 𝑠 = 𝑌 ) )
179 1 6 3 141 147 146 145 178 ncolrot1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ¬ ( 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
180 179 orsild ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ¬ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) )
181 180 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → ¬ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) )
182 18 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
183 175 elin2d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → 𝑟 ∈ ( 𝑠 𝐼 𝑋 ) )
184 1 4 3 79 173 174 176 181 182 183 islnoppd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ∧ 𝑟 ∈ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ) → 𝑠 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 )
185 172 184 n0limd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 )
186 80 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
187 1 4 3 79 6 170 141 162 171 186 oppcom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 )
188 1 3 6 79 141 170 171 147 162 187 lnopp2hpgb ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( 𝑠 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑍 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑍 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝑋 ↔ ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) 𝑠 ) )
189 185 188 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) 𝑠 )
190 1 3 6 141 170 171 79 147 189 hpgcom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
191 169 190 breqdi ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) )
192 168 191 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ) ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) → ( ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) )
193 192 3anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) → ( ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) )
194 140 193 impbida ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ∧ 𝑠 ∈ 𝑃 ) → ( ( ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) ↔ ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) )
195 194 reubidva ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ( ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑤 𝑉 𝑈 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∧ 𝑠 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑍 𝐿 𝑌 ) ) ( ( ( lInvG ‘ 𝐺 ) ‘ ( 𝑌 𝐿 𝑍 ) ) ‘ 𝑋 ) ) ↔ ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) ) )
196 91 195 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ) ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
197 196 anasss ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) ) → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )
198 15 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑉 )
199 1 3 20 9 12 13 7 10 4 198 17 hlcgrex ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑃 ( 𝑤 ( ( hlG ‘ 𝐺 ) ‘ 𝑉 ) 𝑊 ∧ ( 𝑉 − 𝑤 ) = ( 𝑌 − 𝑍 ) ) )
200 197 199 r19.29a ⊢ ( 𝜑 → ∃! 𝑠 ∈ 𝑃 ( ⟨“ 𝑍 𝑌 𝑠 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ ∧ ( 𝑌 − 𝑠 ) = ( 𝑉 − 𝑈 ) ∧ ( ( 𝑌 𝐿 𝑍 ) ∩ ( 𝑠 𝐼 𝑋 ) ) ≠ ∅ ) )