Metamath Proof Explorer

Theorem inagcgratrgncol

Description: In-angle transport once the segment point J of isinag is on the ray E W : iscgrag normalizes the target arms and its two existentials are eliminated here, leaving inagcgratrgxfr to do the transfer. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgratrgncol.p 
|- P = ( Base ` G )
inagcgratrgncol.i 
|- I = ( Itv ` G )
inagcgratrgncol.k 
|- K = ( hlG ` G )
inagcgratrgncol.g 
|- ( ph -> G e. TarskiG )
inagcgratrgncol.d 
|- ( ph -> D e. P )
inagcgratrgncol.e 
|- ( ph -> E e. P )
inagcgratrgncol.f 
|- ( ph -> F e. P )
inagcgratrgncol.w 
|- ( ph -> W e. P )
inagcgratrgncol.x 
|- ( ph -> X e. P )
inagcgratrgncol.y 
|- ( ph -> Y e. P )
inagcgratrgncol.z 
|- ( ph -> Z e. P )
inagcgratrgncol.cgb 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
inagcgratrgncol.j 
|- ( ph -> J e. P )
inagcgratrgncol.de 
|- ( ph -> D =/= E )
inagcgratrgncol.1 
|- ( ph -> J e. ( D I F ) )
inagcgratrgncol.jw 
|- ( ph -> J ( K ` E ) W )
Assertion inagcgratrgncol 
|- ( 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 inagcgratrgncol.p 
 |-  P = ( Base ` G )
2 inagcgratrgncol.i 
 |-  I = ( Itv ` G )
3 inagcgratrgncol.k 
 |-  K = ( hlG ` G )
4 inagcgratrgncol.g 
 |-  ( ph -> G e. TarskiG )
5 inagcgratrgncol.d 
 |-  ( ph -> D e. P )
6 inagcgratrgncol.e 
 |-  ( ph -> E e. P )
7 inagcgratrgncol.f 
 |-  ( ph -> F e. P )
8 inagcgratrgncol.w 
 |-  ( ph -> W e. P )
9 inagcgratrgncol.x 
 |-  ( ph -> X e. P )
10 inagcgratrgncol.y 
 |-  ( ph -> Y e. P )
11 inagcgratrgncol.z 
 |-  ( ph -> Z e. P )
12 inagcgratrgncol.cgb 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
13 inagcgratrgncol.j 
 |-  ( ph -> J e. P )
14 inagcgratrgncol.de 
 |-  ( ph -> D =/= E )
15 inagcgratrgncol.1 
 |-  ( ph -> J e. ( D I F ) )
16 inagcgratrgncol.jw 
 |-  ( ph -> J ( K ` E ) W )
17 eqid 
 |-  ( dist ` G ) = ( dist ` G )
18 1 2 3 17 4 5 6 7 9 10 11 12 iscgrag 
 |-  ( ph -> E. x e. P E. y e. P ( ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) /\ ( ( Y ( dist ` G ) x ) = ( E ( dist ` G ) D ) /\ ( Y ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) )
19 simpl 
 |-  ( ( ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) /\ ( ( Y ( dist ` G ) x ) = ( E ( dist ` G ) D ) /\ ( Y ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) -> ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) )
20 19 reximi 
 |-  ( E. y e. P ( ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) /\ ( ( Y ( dist ` G ) x ) = ( E ( dist ` G ) D ) /\ ( Y ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) -> E. y e. P ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) )
21 20 reximi 
 |-  ( E. x e. P E. y e. P ( ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) /\ ( ( Y ( dist ` G ) x ) = ( E ( dist ` G ) D ) /\ ( Y ( dist ` G ) y ) = ( E ( dist ` G ) F ) ) ) -> E. x e. P E. y e. P ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) )
22 18 21 syl 
 |-  ( ph -> E. x e. P E. y e. P ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) )
23 simpll 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> ph )
24 23 4 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> G e. TarskiG )
25 23 5 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> D e. P )
26 23 6 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> E e. P )
27 23 7 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> F e. P )
28 23 8 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> W e. P )
29 23 9 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> X e. P )
30 23 10 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> Y e. P )
31 23 11 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> Z e. P )
32 23 13 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> J e. P )
33 simplr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> ( x e. P /\ y e. P ) )
34 33 simpld 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> x e. P )
35 33 simprd 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> y e. P )
36 23 14 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> D =/= E )
37 23 15 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> J e. ( D I F ) )
38 23 16 syl 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> J ( K ` E ) W )
39 simpr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) )
40 39 simp2d 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> x ( K ` Y ) X )
41 39 simp3d 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> y ( K ` Y ) Z )
42 39 simp1d 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> <" D E F "> ( cgrG ` G ) <" x Y y "> )
43 1 2 3 24 25 26 27 28 29 30 31 32 34 35 36 37 38 40 41 42 inagcgratrgxfr 
 |-  ( ( ( ph /\ ( x e. P /\ y e. P ) ) /\ ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
44 43 ex 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) )
45 44 rexlimdvva 
 |-  ( ph -> ( E. x e. P E. y e. P ( <" D E F "> ( cgrG ` G ) <" x Y y "> /\ x ( K ` Y ) X /\ y ( K ` Y ) Z ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) )
46 22 45 mpd 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )