Metamath Proof Explorer

Theorem cgrgptxfr

Description: Transfer a segment point across a triangle congruence: given <" A B C "> cgrG <" X E Z "> and J between A and C , the corresponding point on ( X I Z ) exists, with its betweenness, its two distances and the sub-triangle congruence. GeoCoq reaches this through l4__6 and cong2__conga__cong ; here cgrg3col4 (Schwabhauser 11.28) constructs the point with every pairwise distance and tgbtwnxfr -- which *is* l4__6 -- supplies the image betweenness. The A = C case takes cgrg3col4 's right disjunct, since tgellng needs A =/= C and cgrA does not supply it. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses cgrgptxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgrgptxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
cgrgptxfr.m ⊢ − = ( dist ‘ 𝐺 )
cgrgptxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
cgrgptxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
cgrgptxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
cgrgptxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
cgrgptxfr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
cgrgptxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
cgrgptxfr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
cgrgptxfr.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
cgrgptxfr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 ”⟩ )
cgrgptxfr.2 ⊢ ( 𝜑 → 𝐽 ∈ ( 𝐴 𝐼 𝐶 ) )
Assertion cgrgptxfr ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( ( 𝑦 ∈ ( 𝑋 𝐼 𝑍 ) ∧ ⟨“ 𝐴 𝐵 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ) ∧ ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐽 − 𝐶 ) = ( 𝑦 − 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 cgrgptxfr.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 cgrgptxfr.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 cgrgptxfr.m ⊢ − = ( dist ‘ 𝐺 )
4 cgrgptxfr.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 cgrgptxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 cgrgptxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 cgrgptxfr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 cgrgptxfr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9 cgrgptxfr.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 cgrgptxfr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
11 cgrgptxfr.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
12 cgrgptxfr.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 ”⟩ )
13 cgrgptxfr.2 ⊢ ( 𝜑 → 𝐽 ∈ ( 𝐴 𝐼 𝐶 ) )
14 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
15 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝜑 )
16 15 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
17 15 5 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
18 15 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐽 ∈ 𝑃 )
19 15 7 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
20 15 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
21 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
22 15 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝑍 ∈ 𝑃 )
23 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ )
24 15 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
25 15 9 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
26 1 3 2 14 16 17 24 19 18 20 25 22 21 tgcgr4 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 ”⟩ ∧ ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐽 ) = ( 𝐸 − 𝑦 ) ∧ ( 𝐶 − 𝐽 ) = ( 𝑍 − 𝑦 ) ) ) ) )
27 23 26 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 ”⟩ ∧ ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐽 ) = ( 𝐸 − 𝑦 ) ∧ ( 𝐶 − 𝐽 ) = ( 𝑍 − 𝑦 ) ) ) )
28 27 simprd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐵 − 𝐽 ) = ( 𝐸 − 𝑦 ) ∧ ( 𝐶 − 𝐽 ) = ( 𝑍 − 𝑦 ) ) )
29 28 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) )
30 28 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐶 − 𝐽 ) = ( 𝑍 − 𝑦 ) )
31 1 3 2 16 19 18 22 21 30 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐽 − 𝐶 ) = ( 𝑦 − 𝑍 ) )
32 15 12 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 ”⟩ )
33 1 3 2 14 16 17 24 19 20 25 22 32 cgr3simp3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐶 − 𝐴 ) = ( 𝑍 − 𝑋 ) )
34 1 3 14 16 17 18 19 20 21 22 29 31 33 trgcgr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐽 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝑦 𝑍 ”⟩ )
35 15 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝐽 ∈ ( 𝐴 𝐼 𝐶 ) )
36 1 3 2 14 16 17 18 19 20 21 22 34 35 tgbtwnxfr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → 𝑦 ∈ ( 𝑋 𝐼 𝑍 ) )
37 1 3 2 14 16 17 24 19 20 25 22 32 cgr3simp1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐴 − 𝐵 ) = ( 𝑋 − 𝐸 ) )
38 28 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐵 − 𝐽 ) = ( 𝐸 − 𝑦 ) )
39 1 3 2 16 17 18 20 21 29 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝐽 − 𝐴 ) = ( 𝑦 − 𝑋 ) )
40 1 3 14 16 17 24 18 20 25 21 37 38 39 trgcgr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ )
41 36 40 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( 𝑦 ∈ ( 𝑋 𝐼 𝑍 ) ∧ ⟨“ 𝐴 𝐵 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ) )
42 29 31 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐽 − 𝐶 ) = ( 𝑦 − 𝑍 ) ) )
43 41 42 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ ) → ( ( 𝑦 ∈ ( 𝑋 𝐼 𝑍 ) ∧ ⟨“ 𝐴 𝐵 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ) ∧ ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐽 − 𝐶 ) = ( 𝑦 − 𝑍 ) ) ) )
44 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
45 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
46 45 olcd ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐽 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐴 = 𝐶 ) )
47 simpl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝜑 )
48 47 13 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐽 ∈ ( 𝐴 𝐼 𝐶 ) )
49 48 3mix1d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐽 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐴 ∈ ( 𝐽 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐽 ) ) )
50 47 4 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
51 47 5 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
52 47 7 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
53 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ≠ 𝐶 )
54 47 11 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐽 ∈ 𝑃 )
55 1 44 2 50 51 52 53 54 tgellng ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐽 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐶 ) ↔ ( 𝐽 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐴 ∈ ( 𝐽 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐽 ) ) ) )
56 49 55 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → 𝐽 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐶 ) )
57 56 orcd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐽 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐴 = 𝐶 ) )
58 46 57 pm2.61dane ⊢ ( 𝜑 → ( 𝐽 ∈ ( 𝐴 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐴 = 𝐶 ) )
59 1 4 5 6 7 8 9 10 44 11 12 58 cgrg3col4 ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑍 𝑦 ”⟩ )
60 43 59 reximddv3 ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( ( 𝑦 ∈ ( 𝑋 𝐼 𝑍 ) ∧ ⟨“ 𝐴 𝐵 𝐽 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ) ∧ ( ( 𝐴 − 𝐽 ) = ( 𝑋 − 𝑦 ) ∧ ( 𝐽 − 𝐶 ) = ( 𝑦 − 𝑍 ) ) ) )