Metamath Proof Explorer

Theorem cgrahlb

Description: Two null angles are congruent: if A and C lie on one half-line from B , and D and F on one half-line from E , then angle <" A B C "> is congruent to <" D E F "> . This is GeoCoq l11__21__b ; set.mm has only the converse, cgrahl (GeoCoq l11__21__a ). Proved by copying both arms onto the target rays with hlcgrex and closing the third side by segment subtraction ( tgcgrsub2 ), so it needs no non-collinear frame. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses cgrahlb.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgrahlb.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
cgrahlb.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
cgrahlb.m ⊢ − = ( dist ‘ 𝐺 )
cgrahlb.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
cgrahlb.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
cgrahlb.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
cgrahlb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
cgrahlb.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
cgrahlb.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
cgrahlb.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
cgrahlb.1 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
cgrahlb.2 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
Assertion cgrahlb ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 cgrahlb.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 cgrahlb.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 cgrahlb.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 cgrahlb.m ⊢ − = ( dist ‘ 𝐺 )
5 cgrahlb.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 cgrahlb.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 cgrahlb.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 cgrahlb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 cgrahlb.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 cgrahlb.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 cgrahlb.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 cgrahlb.1 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
13 cgrahlb.2 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
14 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝜑 )
15 14 5 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG )
16 14 6 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 )
17 14 7 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 )
18 14 8 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 )
19 14 9 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐷 ∈ 𝑃 )
20 14 10 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ 𝑃 )
21 14 11 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐹 ∈ 𝑃 )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 )
23 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ∈ 𝑃 )
24 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
25 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
26 25 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) )
27 26 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) )
28 27 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝑥 ) )
29 1 4 2 15 17 16 20 22 28 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝐸 ) )
30 25 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) )
31 30 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) )
32 31 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑦 ) )
33 eqid ⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
34 14 12 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
35 1 2 3 16 18 17 15 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) ) ) )
36 34 35 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) ) )
37 36 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝐴 ) ) )
38 26 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 )
39 14 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
40 1 2 3 22 19 21 15 20 38 39 hltr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 )
41 30 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 )
42 1 2 3 23 21 20 15 41 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐹 ( 𝐾 ‘ 𝐸 ) 𝑦 )
43 1 2 3 22 21 23 15 20 40 42 hltr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑦 )
44 1 2 3 22 23 20 15 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑦 ↔ ( 𝑥 ≠ 𝐸 ∧ 𝑦 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) ) ) )
45 43 44 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ≠ 𝐸 ∧ 𝑦 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) ) )
46 45 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐸 𝐼 𝑥 ) ) )
47 1 4 2 33 15 17 16 18 20 20 22 23 37 46 28 32 tgcgrsub2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 − 𝐶 ) = ( 𝑥 − 𝑦 ) )
48 1 4 2 15 16 18 22 23 47 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝑦 − 𝑥 ) )
49 1 4 24 15 16 17 18 22 20 23 29 32 48 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
50 1 2 3 15 16 17 18 19 20 21 22 23 49 38 41 iscgrad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
51 1 2 3 9 11 10 5 13 hlne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
52 1 2 3 6 8 7 5 12 hlne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
53 52 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
54 1 2 3 10 7 6 5 9 4 51 53 hlcgrex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) )
55 1 2 3 9 11 10 5 13 hlne2 ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
56 1 2 3 6 8 7 5 12 hlne2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
57 56 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
58 1 2 3 10 7 8 5 11 4 55 57 hlcgrex ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) )
59 54 58 jca ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
60 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
61 59 60 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
62 50 61 r19.29vva ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )