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 
|- P = ( Base ` G )
cgrgptxfr.i 
|- I = ( Itv ` G )
cgrgptxfr.m 
|- .- = ( dist ` G )
cgrgptxfr.g 
|- ( ph -> G e. TarskiG )
cgrgptxfr.a 
|- ( ph -> A e. P )
cgrgptxfr.b 
|- ( ph -> B e. P )
cgrgptxfr.c 
|- ( ph -> C e. P )
cgrgptxfr.x 
|- ( ph -> X e. P )
cgrgptxfr.e 
|- ( ph -> E e. P )
cgrgptxfr.z 
|- ( ph -> Z e. P )
cgrgptxfr.j 
|- ( ph -> J e. P )
cgrgptxfr.1 
|- ( ph -> <" A B C "> ( cgrG ` G ) <" X E Z "> )
cgrgptxfr.2 
|- ( ph -> J e. ( A I C ) )
Assertion cgrgptxfr 
|- ( ph -> E. y e. P ( ( y e. ( X I Z ) /\ <" A B J "> ( cgrG ` G ) <" X E y "> ) /\ ( ( A .- J ) = ( X .- y ) /\ ( J .- C ) = ( y .- Z ) ) ) )

Proof

Step Hyp Ref Expression
1 cgrgptxfr.p 
 |-  P = ( Base ` G )
2 cgrgptxfr.i 
 |-  I = ( Itv ` G )
3 cgrgptxfr.m 
 |-  .- = ( dist ` G )
4 cgrgptxfr.g 
 |-  ( ph -> G e. TarskiG )
5 cgrgptxfr.a 
 |-  ( ph -> A e. P )
6 cgrgptxfr.b 
 |-  ( ph -> B e. P )
7 cgrgptxfr.c 
 |-  ( ph -> C e. P )
8 cgrgptxfr.x 
 |-  ( ph -> X e. P )
9 cgrgptxfr.e 
 |-  ( ph -> E e. P )
10 cgrgptxfr.z 
 |-  ( ph -> Z e. P )
11 cgrgptxfr.j 
 |-  ( ph -> J e. P )
12 cgrgptxfr.1 
 |-  ( ph -> <" A B C "> ( cgrG ` G ) <" X E Z "> )
13 cgrgptxfr.2 
 |-  ( ph -> J e. ( A I C ) )
14 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
15 simpll 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ph )
16 15 4 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> G e. TarskiG )
17 15 5 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> A e. P )
18 15 11 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> J e. P )
19 15 7 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> C e. P )
20 15 8 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> X e. P )
21 simplr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> y e. P )
22 15 10 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> Z e. P )
23 simpr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> <" A B C J "> ( cgrG ` G ) <" X E Z y "> )
24 15 6 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> B e. P )
25 15 9 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> E e. P )
26 1 3 2 14 16 17 24 19 18 20 25 22 21 tgcgr4 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( <" A B C J "> ( cgrG ` G ) <" X E Z y "> <-> ( <" A B C "> ( cgrG ` G ) <" X E Z "> /\ ( ( A .- J ) = ( X .- y ) /\ ( B .- J ) = ( E .- y ) /\ ( C .- J ) = ( Z .- y ) ) ) ) )
27 23 26 mpbid 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( <" A B C "> ( cgrG ` G ) <" X E Z "> /\ ( ( A .- J ) = ( X .- y ) /\ ( B .- J ) = ( E .- y ) /\ ( C .- J ) = ( Z .- y ) ) ) )
28 27 simprd 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( ( A .- J ) = ( X .- y ) /\ ( B .- J ) = ( E .- y ) /\ ( C .- J ) = ( Z .- y ) ) )
29 28 simp1d 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( A .- J ) = ( X .- y ) )
30 28 simp3d 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( C .- J ) = ( Z .- y ) )
31 1 3 2 16 19 18 22 21 30 tgcgrcomlr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( J .- C ) = ( y .- Z ) )
32 15 12 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> <" A B C "> ( cgrG ` G ) <" X E Z "> )
33 1 3 2 14 16 17 24 19 20 25 22 32 cgr3simp3 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( C .- A ) = ( Z .- X ) )
34 1 3 14 16 17 18 19 20 21 22 29 31 33 trgcgr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> <" A J C "> ( cgrG ` G ) <" X y Z "> )
35 15 13 syl 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> J e. ( A I C ) )
36 1 3 2 14 16 17 18 19 20 21 22 34 35 tgbtwnxfr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> y e. ( X I Z ) )
37 1 3 2 14 16 17 24 19 20 25 22 32 cgr3simp1 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( A .- B ) = ( X .- E ) )
38 28 simp2d 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( B .- J ) = ( E .- y ) )
39 1 3 2 16 17 18 20 21 29 tgcgrcomlr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( J .- A ) = ( y .- X ) )
40 1 3 14 16 17 24 18 20 25 21 37 38 39 trgcgr 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> <" A B J "> ( cgrG ` G ) <" X E y "> )
41 36 40 jca 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( y e. ( X I Z ) /\ <" A B J "> ( cgrG ` G ) <" X E y "> ) )
42 29 31 jca 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( ( A .- J ) = ( X .- y ) /\ ( J .- C ) = ( y .- Z ) ) )
43 41 42 jca 
 |-  ( ( ( ph /\ y e. P ) /\ <" A B C J "> ( cgrG ` G ) <" X E Z y "> ) -> ( ( y e. ( X I Z ) /\ <" A B J "> ( cgrG ` G ) <" X E y "> ) /\ ( ( A .- J ) = ( X .- y ) /\ ( J .- C ) = ( y .- Z ) ) ) )
44 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
45 simpr 
 |-  ( ( ph /\ A = C ) -> A = C )
46 45 olcd 
 |-  ( ( ph /\ A = C ) -> ( J e. ( A ( LineG ` G ) C ) \/ A = C ) )
47 simpl 
 |-  ( ( ph /\ A =/= C ) -> ph )
48 47 13 syl 
 |-  ( ( ph /\ A =/= C ) -> J e. ( A I C ) )
49 48 3mix1d 
 |-  ( ( ph /\ A =/= C ) -> ( J e. ( A I C ) \/ A e. ( J I C ) \/ C e. ( A I J ) ) )
50 47 4 syl 
 |-  ( ( ph /\ A =/= C ) -> G e. TarskiG )
51 47 5 syl 
 |-  ( ( ph /\ A =/= C ) -> A e. P )
52 47 7 syl 
 |-  ( ( ph /\ A =/= C ) -> C e. P )
53 simpr 
 |-  ( ( ph /\ A =/= C ) -> A =/= C )
54 47 11 syl 
 |-  ( ( ph /\ A =/= C ) -> J e. P )
55 1 44 2 50 51 52 53 54 tgellng 
 |-  ( ( ph /\ A =/= C ) -> ( J e. ( A ( LineG ` G ) C ) <-> ( J e. ( A I C ) \/ A e. ( J I C ) \/ C e. ( A I J ) ) ) )
56 49 55 mpbird 
 |-  ( ( ph /\ A =/= C ) -> J e. ( A ( LineG ` G ) C ) )
57 56 orcd 
 |-  ( ( ph /\ A =/= C ) -> ( J e. ( A ( LineG ` G ) C ) \/ A = C ) )
58 46 57 pm2.61dane 
 |-  ( ph -> ( J e. ( A ( LineG ` G ) C ) \/ A = C ) )
59 1 4 5 6 7 8 9 10 44 11 12 58 cgrg3col4 
 |-  ( ph -> E. y e. P <" A B C J "> ( cgrG ` G ) <" X E Z y "> )
60 43 59 reximddv3 
 |-  ( ph -> E. y e. P ( ( y e. ( X I Z ) /\ <" A B J "> ( cgrG ` G ) <" X E y "> ) /\ ( ( A .- J ) = ( X .- y ) /\ ( J .- C ) = ( y .- Z ) ) ) )