Metamath Proof Explorer

Theorem inagcgratrgn

Description: In-angle transport, non-collinear case: unfold isinag , eliminate its segment-point existential, and dispatch on the disjunct it carries -- x = E to inagcgrabtwn , x ( KE ) W to inagcgratrgncol . (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 "> )
inagcgratrgn.l 
|- L = ( LineG ` G )
inagcgratrgn.in 
|- ( ph -> W ( inA ` G ) <" D E F "> )
inagcgratrgn.1 
|- ( ph -> -. ( W e. ( D L E ) \/ D = E ) )
Assertion inagcgratrgn 
|- ( 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 inagcgratrgn.l 
 |-  L = ( LineG ` G )
14 inagcgratrgn.in 
 |-  ( ph -> W ( inA ` G ) <" D E F "> )
15 inagcgratrgn.1 
 |-  ( ph -> -. ( W e. ( D L E ) \/ D = E ) )
16 1 2 3 8 5 6 7 4 isinag 
 |-  ( ph -> ( W ( inA ` G ) <" D E F "> <-> ( ( D =/= E /\ F =/= E /\ W =/= E ) /\ E. x e. P ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) )
17 14 16 mpbid 
 |-  ( ph -> ( ( D =/= E /\ F =/= E /\ W =/= E ) /\ E. x e. P ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) )
18 17 simprd 
 |-  ( ph -> E. x e. P ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) )
19 simpl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> ph )
20 19 4 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> G e. TarskiG )
21 20 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> G e. TarskiG )
22 19 5 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> D e. P )
23 22 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> D e. P )
24 19 6 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> E e. P )
25 24 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> E e. P )
26 19 7 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> F e. P )
27 26 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> F e. P )
28 19 8 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> W e. P )
29 28 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> W e. P )
30 19 9 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> X e. P )
31 30 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> X e. P )
32 19 10 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> Y e. P )
33 32 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> Y e. P )
34 19 11 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> Z e. P )
35 34 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> Z e. P )
36 19 12 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
37 36 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
38 simpr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) )
39 38 simprd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) )
40 39 simpld 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> x e. ( D I F ) )
41 40 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> x e. ( D I F ) )
42 simpr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> x = E )
43 42 eleq1d 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> ( x e. ( D I F ) <-> E e. ( D I F ) ) )
44 41 43 mpbid 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> E e. ( D I F ) )
45 19 15 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> -. ( W e. ( D L E ) \/ D = E ) )
46 45 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> -. ( W e. ( D L E ) \/ D = E ) )
47 1 2 3 13 21 23 25 27 29 31 33 35 37 44 46 inagcgrabtwn 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x = E ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
48 20 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> G e. TarskiG )
49 22 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> D e. P )
50 24 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> E e. P )
51 26 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> F e. P )
52 28 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> W e. P )
53 30 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> X e. P )
54 32 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> Y e. P )
55 34 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> Z e. P )
56 36 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
57 38 simpld 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> x e. P )
58 57 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> x e. P )
59 1 2 3 8 5 6 7 4 14 inagne1 
 |-  ( ph -> D =/= E )
60 19 59 syl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> D =/= E )
61 60 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> D =/= E )
62 40 adantr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> x e. ( D I F ) )
63 simpr 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> x ( K ` E ) W )
64 1 2 3 48 49 50 51 52 53 54 55 56 58 61 62 63 inagcgratrgncol 
 |-  ( ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) /\ x ( K ` E ) W ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
65 39 simprd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> ( x = E \/ x ( K ` E ) W ) )
66 47 64 65 mpjaodan 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
67 18 66 rexlimddv 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )