Metamath Proof Explorer

Theorem inagcgratrgxfr

Description: In-angle transport with the target arms already normalized to S and T : cgrgptxfr transfers the segment point J to a point of ( S I T ) , and that one existential is eliminated here. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgratrgxfr.p 
|- P = ( Base ` G )
inagcgratrgxfr.i 
|- I = ( Itv ` G )
inagcgratrgxfr.k 
|- K = ( hlG ` G )
inagcgratrgxfr.g 
|- ( ph -> G e. TarskiG )
inagcgratrgxfr.d 
|- ( ph -> D e. P )
inagcgratrgxfr.e 
|- ( ph -> E e. P )
inagcgratrgxfr.f 
|- ( ph -> F e. P )
inagcgratrgxfr.w 
|- ( ph -> W e. P )
inagcgratrgxfr.x 
|- ( ph -> X e. P )
inagcgratrgxfr.y 
|- ( ph -> Y e. P )
inagcgratrgxfr.z 
|- ( ph -> Z e. P )
inagcgratrgxfr.j 
|- ( ph -> J e. P )
inagcgratrgxfr.s 
|- ( ph -> S e. P )
inagcgratrgxfr.t 
|- ( ph -> T e. P )
inagcgratrgxfr.de 
|- ( ph -> D =/= E )
inagcgratrgxfr.1 
|- ( ph -> J e. ( D I F ) )
inagcgratrgxfr.jw 
|- ( ph -> J ( K ` E ) W )
inagcgratrgxfr.sx 
|- ( ph -> S ( K ` Y ) X )
inagcgratrgxfr.tz 
|- ( ph -> T ( K ` Y ) Z )
inagcgratrgxfr.2 
|- ( ph -> <" D E F "> ( cgrG ` G ) <" S Y T "> )
Assertion inagcgratrgxfr 
|- ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )

Proof

Step Hyp Ref Expression
1 inagcgratrgxfr.p 
 |-  P = ( Base ` G )
2 inagcgratrgxfr.i 
 |-  I = ( Itv ` G )
3 inagcgratrgxfr.k 
 |-  K = ( hlG ` G )
4 inagcgratrgxfr.g 
 |-  ( ph -> G e. TarskiG )
5 inagcgratrgxfr.d 
 |-  ( ph -> D e. P )
6 inagcgratrgxfr.e 
 |-  ( ph -> E e. P )
7 inagcgratrgxfr.f 
 |-  ( ph -> F e. P )
8 inagcgratrgxfr.w 
 |-  ( ph -> W e. P )
9 inagcgratrgxfr.x 
 |-  ( ph -> X e. P )
10 inagcgratrgxfr.y 
 |-  ( ph -> Y e. P )
11 inagcgratrgxfr.z 
 |-  ( ph -> Z e. P )
12 inagcgratrgxfr.j 
 |-  ( ph -> J e. P )
13 inagcgratrgxfr.s 
 |-  ( ph -> S e. P )
14 inagcgratrgxfr.t 
 |-  ( ph -> T e. P )
15 inagcgratrgxfr.de 
 |-  ( ph -> D =/= E )
16 inagcgratrgxfr.1 
 |-  ( ph -> J e. ( D I F ) )
17 inagcgratrgxfr.jw 
 |-  ( ph -> J ( K ` E ) W )
18 inagcgratrgxfr.sx 
 |-  ( ph -> S ( K ` Y ) X )
19 inagcgratrgxfr.tz 
 |-  ( ph -> T ( K ` Y ) Z )
20 inagcgratrgxfr.2 
 |-  ( ph -> <" D E F "> ( cgrG ` G ) <" S Y T "> )
21 eqid 
 |-  ( dist ` G ) = ( dist ` G )
22 1 2 21 4 5 6 7 13 10 14 12 20 16 cgrgptxfr 
 |-  ( ph -> E. y e. P ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) )
23 simpl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> ph )
24 23 4 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> G e. TarskiG )
25 23 5 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> D e. P )
26 23 6 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> E e. P )
27 23 8 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> W e. P )
28 23 9 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> X e. P )
29 23 10 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> Y e. P )
30 23 11 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> Z e. P )
31 23 12 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> J e. P )
32 23 13 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> S e. P )
33 23 14 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> T e. P )
34 simpr 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) )
35 34 simpld 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> y e. P )
36 23 15 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> D =/= E )
37 23 17 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> J ( K ` E ) W )
38 23 18 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> S ( K ` Y ) X )
39 23 19 syl 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> T ( K ` Y ) Z )
40 34 simprd 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) )
41 40 simpld 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) )
42 41 simpld 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> y e. ( S I T ) )
43 41 simprd 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> <" D E J "> ( cgrG ` G ) <" S Y y "> )
44 1 2 3 24 25 26 27 28 29 30 31 32 33 35 36 37 38 39 42 43 inagcgratrgw 
 |-  ( ( ph /\ ( y e. P /\ ( ( y e. ( S I T ) /\ <" D E J "> ( cgrG ` G ) <" S Y y "> ) /\ ( ( D ( dist ` G ) J ) = ( S ( dist ` G ) y ) /\ ( J ( dist ` G ) F ) = ( y ( dist ` G ) T ) ) ) ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
45 22 44 rexlimddv 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )