Metamath Proof Explorer

Theorem dfcgra2

Description: This is the full statement of definition 11.2 of Schwabhauser p. 95. This proof serves to confirm that the definition we have chosen, df-cgra is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses dfcgra2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
dfcgra2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
dfcgra2.m ⊢ − = ( dist ‘ 𝐺 )
dfcgra2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
dfcgra2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
dfcgra2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
dfcgra2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
dfcgra2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
dfcgra2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
dfcgra2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
Assertion dfcgra2 ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfcgra2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 dfcgra2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 dfcgra2.m ⊢ − = ( dist ‘ 𝐺 )
4 dfcgra2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 dfcgra2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 dfcgra2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 dfcgra2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 dfcgra2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 dfcgra2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 dfcgra2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
12 4 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐺 ∈ TarskiG )
13 5 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐴 ∈ 𝑃 )
14 6 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐵 ∈ 𝑃 )
15 7 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐶 ∈ 𝑃 )
16 8 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐷 ∈ 𝑃 )
17 9 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸 ∈ 𝑃 )
18 10 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐹 ∈ 𝑃 )
19 simpr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
20 1 2 11 12 13 14 15 16 17 18 19 cgrane1 ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐴 ≠ 𝐵 )
21 1 2 11 12 13 14 15 16 17 18 19 cgrane2 ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐵 ≠ 𝐶 )
22 21 necomd ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐶 ≠ 𝐵 )
23 20 22 jca ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) )
24 1 2 11 12 13 14 15 16 17 18 19 cgrane3 ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸 ≠ 𝐷 )
25 24 necomd ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐷 ≠ 𝐸 )
26 1 2 11 12 13 14 15 16 17 18 19 cgrane4 ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐸 ≠ 𝐹 )
27 26 necomd ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → 𝐹 ≠ 𝐸 )
28 25 27 jca ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) )
29 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) )
30 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) )
31 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐺 ∈ TarskiG )
32 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ∈ 𝑃 )
33 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐵 ∈ 𝑃 )
34 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ∈ 𝑃 )
35 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑑 ∈ 𝑃 )
36 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐸 ∈ 𝑃 )
37 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑓 ∈ 𝑃 )
38 10 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ∈ 𝑃 )
39 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ∈ 𝑃 )
40 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ∈ 𝑃 )
41 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ∈ 𝑃 )
42 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
43 1 2 31 11 41 33 40 39 36 38 42 cgracom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
44 29 simplld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) )
45 20 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ≠ 𝐵 )
46 1 3 2 31 33 41 32 44 45 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐵 ≠ 𝑎 )
47 1 2 11 33 32 41 31 41 44 46 45 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 )
48 1 2 11 41 32 33 31 47 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
49 1 2 11 31 39 36 38 41 33 40 43 32 48 cgrahl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝐶 ”⟩ )
50 29 simprld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) )
51 22 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ≠ 𝐵 )
52 1 3 2 31 33 40 34 50 51 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐵 ≠ 𝑐 )
53 1 2 11 33 34 40 31 41 50 52 51 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 )
54 1 2 11 40 34 33 31 53 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
55 1 2 11 31 39 36 38 32 33 40 49 34 54 cgrahl2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑎 𝐵 𝑐 ”⟩ )
56 1 2 31 11 39 36 38 32 33 34 55 cgracom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
57 30 simplld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) )
58 25 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ≠ 𝐸 )
59 1 3 2 31 36 39 35 57 58 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐸 ≠ 𝑑 )
60 1 2 11 36 35 39 31 41 57 59 58 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑑 )
61 1 2 11 39 35 36 31 60 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
62 1 2 11 31 32 33 34 39 36 38 56 35 61 cgrahl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝐹 ”⟩ )
63 30 simprld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) )
64 27 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ≠ 𝐸 )
65 1 3 2 31 36 38 37 63 64 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐸 ≠ 𝑓 )
66 1 2 11 36 37 38 31 41 63 65 64 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑓 )
67 1 2 11 38 37 36 31 66 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
68 1 2 11 31 32 33 34 35 36 38 62 37 67 cgrahl2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ⟨“ 𝑎 𝐵 𝑐 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ )
69 46 necomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ≠ 𝐵 )
70 1 2 11 32 41 33 31 69 hlid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑎 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑎 )
71 52 necomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ≠ 𝐵 )
72 1 2 11 34 41 33 31 71 hlid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝑐 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑐 )
73 1 3 2 31 33 41 32 44 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐴 ∈ ( 𝑎 𝐼 𝐵 ) )
74 29 simplrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) )
75 1 3 2 31 41 32 36 39 74 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑎 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
76 30 simplrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) )
77 76 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝑑 ) )
78 1 3 2 31 33 41 39 35 77 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝑑 ) )
79 1 3 2 31 32 41 33 36 39 35 73 57 75 78 tgcgrextend ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑎 − 𝐵 ) = ( 𝐸 − 𝑑 ) )
80 1 3 2 31 32 33 36 35 79 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝑎 ) = ( 𝐸 − 𝑑 ) )
81 1 3 2 31 33 40 34 50 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → 𝐶 ∈ ( 𝑐 𝐼 𝐵 ) )
82 29 simprrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) )
83 1 3 2 31 40 34 36 38 82 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑐 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
84 30 simprrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) )
85 84 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝑓 ) )
86 1 3 2 31 33 40 38 37 85 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝐹 − 𝑓 ) )
87 1 3 2 31 34 40 33 36 38 37 81 63 83 86 tgcgrextend ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑐 − 𝐵 ) = ( 𝐸 − 𝑓 ) )
88 1 3 2 31 34 33 36 37 87 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝐵 − 𝑐 ) = ( 𝐸 − 𝑓 ) )
89 1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88 cgracgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) )
90 29 30 89 3jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) )
91 90 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑓 ∈ 𝑃 ) → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
92 91 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ 𝑑 ∈ 𝑃 ) → ( ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) → ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
93 92 reximdva ⊢ ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
94 93 imp ⊢ ( ( ( ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑐 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ) → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) )
95 1 3 2 4 6 5 9 8 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) )
96 1 3 2 4 6 7 9 10 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) )
97 reeanv ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ∃ 𝑐 ∈ 𝑃 ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) )
98 95 96 97 sylanbrc ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) )
99 1 3 2 4 9 8 6 5 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) )
100 1 3 2 4 9 10 6 7 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) )
101 reeanv ⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ∃ 𝑑 ∈ 𝑃 ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ∃ 𝑓 ∈ 𝑃 ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) )
102 99 100 101 sylanbrc ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) )
103 98 102 jca ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
104 r19.41vv ⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) )
105 ancom ⊢ ( ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
106 105 2rexbii ⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
107 ancom ⊢ ( ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
108 104 106 107 3bitr3i ⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
109 108 2rexbii ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
110 r19.41vv ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
111 109 110 bitr2i ⊢ ( ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
112 103 111 sylib ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
113 112 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
114 94 113 reximddv2 ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) )
115 23 28 114 3jca ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
116 df-3an ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ↔ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
117 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐺 ∈ TarskiG )
118 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ∈ 𝑃 )
119 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐸 ∈ 𝑃 )
120 10 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ∈ 𝑃 )
121 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ∈ 𝑃 )
122 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐵 ∈ 𝑃 )
123 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ∈ 𝑃 )
124 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑦 ∈ 𝑃 )
125 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑥 ∈ 𝑃 )
126 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑧 ∈ 𝑃 )
127 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑡 ∈ 𝑃 )
128 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
129 simpr1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) )
130 129 simplld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) )
131 simpr2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) )
132 131 simplld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) )
133 1 3 2 117 119 118 126 132 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ∈ ( 𝑧 𝐼 𝐸 ) )
134 131 simplrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) )
135 134 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐷 − 𝑧 ) )
136 1 3 2 117 122 121 118 126 135 tgcgrcomr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝑧 − 𝐷 ) )
137 129 simplrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) )
138 1 3 2 117 121 125 119 118 137 tgcgrcomr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐷 − 𝐸 ) )
139 1 3 2 117 122 121 125 126 118 119 130 133 136 138 tgcgrextend ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝑥 ) = ( 𝑧 − 𝐸 ) )
140 1 3 2 117 122 125 126 119 139 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑥 − 𝐵 ) = ( 𝑧 − 𝐸 ) )
141 129 simprld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) )
142 1 3 2 117 122 123 124 141 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ∈ ( 𝑦 𝐼 𝐵 ) )
143 131 simprld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) )
144 129 simprrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) )
145 1 3 2 117 123 124 119 120 144 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑦 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
146 131 simprrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) )
147 146 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐹 − 𝑡 ) )
148 1 3 2 117 122 123 120 127 147 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝐹 − 𝑡 ) )
149 1 3 2 117 124 123 122 119 120 127 142 143 145 148 tgcgrextend ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑦 − 𝐵 ) = ( 𝐸 − 𝑡 ) )
150 1 3 2 117 124 122 119 127 149 tgcgrcoml ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝐵 − 𝑦 ) = ( 𝐸 − 𝑡 ) )
151 simpr3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) )
152 1 3 2 117 125 124 126 127 151 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( 𝑦 − 𝑥 ) = ( 𝑡 − 𝑧 ) )
153 1 3 128 117 125 122 124 126 119 127 140 150 152 trgcgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝑥 𝐵 𝑦 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑧 𝐸 𝑡 ”⟩ )
154 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) )
155 154 simprld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ≠ 𝐸 )
156 1 3 2 117 119 118 126 132 155 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐸 ≠ 𝑧 )
157 1 2 11 119 126 118 117 122 132 156 155 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑧 )
158 1 2 11 118 126 119 117 157 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑧 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
159 154 simprrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ≠ 𝐸 )
160 1 3 2 117 119 120 127 143 159 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐸 ≠ 𝑡 )
161 1 2 11 119 127 120 117 122 143 160 159 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑡 )
162 1 2 11 120 127 119 117 161 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝑡 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
163 1 2 11 117 125 122 124 118 119 120 126 127 153 158 162 iscgrad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝑥 𝐵 𝑦 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
164 1 2 117 11 125 122 124 118 119 120 163 cgracom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ )
165 154 simplld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ≠ 𝐵 )
166 1 3 2 117 122 121 125 130 165 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐵 ≠ 𝑥 )
167 1 2 11 122 125 121 117 121 130 166 165 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑥 )
168 1 2 11 117 118 119 120 125 122 124 164 121 167 cgrahl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝑦 ”⟩ )
169 154 simplrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ≠ 𝐵 )
170 1 3 2 117 122 123 124 141 169 tgbtwnne ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐵 ≠ 𝑦 )
171 1 2 11 122 124 123 117 121 141 170 169 btwnhl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝑦 )
172 1 2 11 117 118 119 120 121 122 124 168 123 171 cgrahl2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
173 1 2 117 11 118 119 120 121 122 123 172 cgracom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
174 173 adantl3r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
175 oveq2 ⊢ ( 𝑑 = 𝑧 → ( 𝐸 𝐼 𝑑 ) = ( 𝐸 𝐼 𝑧 ) )
176 175 eleq2d ⊢ ( 𝑑 = 𝑧 → ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ↔ 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ) )
177 oveq2 ⊢ ( 𝑑 = 𝑧 → ( 𝐷 − 𝑑 ) = ( 𝐷 − 𝑧 ) )
178 177 eqeq1d ⊢ ( 𝑑 = 𝑧 → ( ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ↔ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) )
179 176 178 anbi12d ⊢ ( 𝑑 = 𝑧 → ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ↔ ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ) )
180 179 anbi1d ⊢ ( 𝑑 = 𝑧 → ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ) )
181 oveq1 ⊢ ( 𝑑 = 𝑧 → ( 𝑑 − 𝑓 ) = ( 𝑧 − 𝑓 ) )
182 181 eqeq2d ⊢ ( 𝑑 = 𝑧 → ( ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ) )
183 180 182 3anbi23d ⊢ ( 𝑑 = 𝑧 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ) ) )
184 oveq2 ⊢ ( 𝑓 = 𝑡 → ( 𝐸 𝐼 𝑓 ) = ( 𝐸 𝐼 𝑡 ) )
185 184 eleq2d ⊢ ( 𝑓 = 𝑡 → ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ↔ 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ) )
186 oveq2 ⊢ ( 𝑓 = 𝑡 → ( 𝐹 − 𝑓 ) = ( 𝐹 − 𝑡 ) )
187 186 eqeq1d ⊢ ( 𝑓 = 𝑡 → ( ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ↔ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) )
188 185 187 anbi12d ⊢ ( 𝑓 = 𝑡 → ( ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ↔ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) )
189 188 anbi2d ⊢ ( 𝑓 = 𝑡 → ( ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ) )
190 oveq2 ⊢ ( 𝑓 = 𝑡 → ( 𝑧 − 𝑓 ) = ( 𝑧 − 𝑡 ) )
191 190 eqeq2d ⊢ ( 𝑓 = 𝑡 → ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) )
192 189 191 3anbi23d ⊢ ( 𝑓 = 𝑡 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) ) )
193 183 192 cbvrex2vw ⊢ ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) )
194 193 bilani ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → ∃ 𝑧 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑧 ) ∧ ( 𝐷 − 𝑧 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑡 ) ∧ ( 𝐹 − 𝑡 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑡 ) ) )
195 174 194 r19.29vva ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
196 195 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
197 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝐵 𝐼 𝑎 ) = ( 𝐵 𝐼 𝑥 ) )
198 197 eleq2d ⊢ ( 𝑎 = 𝑥 → ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ↔ 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ) )
199 oveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝐴 − 𝑎 ) = ( 𝐴 − 𝑥 ) )
200 199 eqeq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ↔ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) )
201 198 200 anbi12d ⊢ ( 𝑎 = 𝑥 → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ↔ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ) )
202 201 anbi1d ⊢ ( 𝑎 = 𝑥 → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ) )
203 oveq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 − 𝑐 ) = ( 𝑥 − 𝑐 ) )
204 203 eqeq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ↔ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) )
205 202 204 3anbi13d ⊢ ( 𝑎 = 𝑥 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
206 205 2rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) )
207 oveq2 ⊢ ( 𝑐 = 𝑦 → ( 𝐵 𝐼 𝑐 ) = ( 𝐵 𝐼 𝑦 ) )
208 207 eleq2d ⊢ ( 𝑐 = 𝑦 → ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ↔ 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ) )
209 oveq2 ⊢ ( 𝑐 = 𝑦 → ( 𝐶 − 𝑐 ) = ( 𝐶 − 𝑦 ) )
210 209 eqeq1d ⊢ ( 𝑐 = 𝑦 → ( ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ↔ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) )
211 208 210 anbi12d ⊢ ( 𝑐 = 𝑦 → ( ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ↔ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) )
212 211 anbi2d ⊢ ( 𝑐 = 𝑦 → ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ) )
213 oveq2 ⊢ ( 𝑐 = 𝑦 → ( 𝑥 − 𝑐 ) = ( 𝑥 − 𝑦 ) )
214 213 eqeq1d ⊢ ( 𝑐 = 𝑦 → ( ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) )
215 212 214 3anbi13d ⊢ ( 𝑐 = 𝑦 → ( ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) )
216 215 2rexbidv ⊢ ( 𝑐 = 𝑦 → ( ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) ) )
217 206 216 cbvrex2vw ⊢ ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) )
218 217 bilani ⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑥 − 𝑦 ) = ( 𝑑 − 𝑓 ) ) )
219 196 218 r19.29vva ⊢ ( ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
220 219 anasss ⊢ ( ( 𝜑 ∧ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
221 116 220 sylan2b ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
222 115 221 impbida ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ) ∧ ( 𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ) ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑐 ∈ 𝑃 ∃ 𝑑 ∈ 𝑃 ∃ 𝑓 ∈ 𝑃 ( ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑎 ) ∧ ( 𝐴 − 𝑎 ) = ( 𝐸 − 𝐷 ) ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐶 − 𝑐 ) = ( 𝐸 − 𝐹 ) ) ) ∧ ( ( 𝐷 ∈ ( 𝐸 𝐼 𝑑 ) ∧ ( 𝐷 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐹 ∈ ( 𝐸 𝐼 𝑓 ) ∧ ( 𝐹 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝑎 − 𝑐 ) = ( 𝑑 − 𝑓 ) ) ) ) )