Metamath Proof Explorer

Theorem cgrainag

Description: Target-side in-angle transport: if W lies inside angle <" D E F "> and that angle is congruent to <" X Y Z "> , then some point inside <" X Y Z "> makes <" X Y v "> congruent to the sub-angle <" D E W "> . The geometric core of leawittrg . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses cgrainag.p 
|- P = ( Base ` G )
cgrainag.i 
|- I = ( Itv ` G )
cgrainag.k 
|- K = ( hlG ` G )
cgrainag.g 
|- ( ph -> G e. TarskiG )
cgrainag.d 
|- ( ph -> D e. P )
cgrainag.e 
|- ( ph -> E e. P )
cgrainag.f 
|- ( ph -> F e. P )
cgrainag.x 
|- ( ph -> X e. P )
cgrainag.y 
|- ( ph -> Y e. P )
cgrainag.z 
|- ( ph -> Z e. P )
cgrainag.w 
|- ( ph -> W e. P )
cgrainag.in 
|- ( ph -> W ( inA ` G ) <" D E F "> )
cgrainag.cgb 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
Assertion cgrainag 
|- ( 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 cgrainag.p 
 |-  P = ( Base ` G )
2 cgrainag.i 
 |-  I = ( Itv ` G )
3 cgrainag.k 
 |-  K = ( hlG ` G )
4 cgrainag.g 
 |-  ( ph -> G e. TarskiG )
5 cgrainag.d 
 |-  ( ph -> D e. P )
6 cgrainag.e 
 |-  ( ph -> E e. P )
7 cgrainag.f 
 |-  ( ph -> F e. P )
8 cgrainag.x 
 |-  ( ph -> X e. P )
9 cgrainag.y 
 |-  ( ph -> Y e. P )
10 cgrainag.z 
 |-  ( ph -> Z e. P )
11 cgrainag.w 
 |-  ( ph -> W e. P )
12 cgrainag.in 
 |-  ( ph -> W ( inA ` G ) <" D E F "> )
13 cgrainag.cgb 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
14 4 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> G e. TarskiG )
15 14 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> G e. TarskiG )
16 5 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> D e. P )
17 16 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> D e. P )
18 6 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> E e. P )
19 18 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> E e. P )
20 7 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> F e. P )
21 20 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> F e. P )
22 11 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> W e. P )
23 22 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> W e. P )
24 8 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> X e. P )
25 24 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> X e. P )
26 9 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> Y e. P )
27 26 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> Y e. P )
28 10 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> Z e. P )
29 28 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> Z e. P )
30 13 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
31 30 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
32 simpr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> D ( K ` E ) W )
33 1 2 3 15 17 19 21 23 25 27 29 31 32 inagcgrasubhl 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ D ( K ` E ) W ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
34 14 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> G e. TarskiG )
35 16 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> D e. P )
36 18 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> E e. P )
37 20 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> F e. P )
38 22 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> W e. P )
39 24 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> X e. P )
40 26 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> Y e. P )
41 28 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> Z e. P )
42 12 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> W ( inA ` G ) <" D E F "> )
43 42 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> W ( inA ` G ) <" D E F "> )
44 30 adantr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
45 simpr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> E e. ( D I W ) )
46 1 2 3 34 35 36 37 38 39 40 41 43 44 45 inagcgrasubbtwn 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
47 simpl 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) )
48 47 22 syl 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> W e. P )
49 47 16 syl 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> D e. P )
50 47 18 syl 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> E e. P )
51 47 14 syl 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> G e. TarskiG )
52 simpr 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> W ( K ` E ) D )
53 1 2 3 48 49 50 51 52 hlcomd 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> D ( K ` E ) W )
54 53 orcd 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ W ( K ` E ) D ) -> ( D ( K ` E ) W \/ E e. ( D I W ) ) )
55 45 olcd 
 |-  ( ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) /\ E e. ( D I W ) ) -> ( D ( K ` E ) W \/ E e. ( D I W ) ) )
56 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
57 simpr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> ( W e. ( D ( LineG ` G ) E ) \/ D = E ) )
58 1 2 3 11 5 6 7 4 12 inagne1 
 |-  ( ph -> D =/= E )
59 58 neneqd 
 |-  ( ph -> -. D = E )
60 59 adantr 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> -. D = E )
61 orel2 
 |-  ( -. D = E -> ( ( W e. ( D ( LineG ` G ) E ) \/ D = E ) -> W e. ( D ( LineG ` G ) E ) ) )
62 60 61 syl 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> ( ( W e. ( D ( LineG ` G ) E ) \/ D = E ) -> W e. ( D ( LineG ` G ) E ) ) )
63 57 62 mpd 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> W e. ( D ( LineG ` G ) E ) )
64 1 2 3 16 18 22 14 16 56 63 lnhl 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> ( W ( K ` E ) D \/ E e. ( D I W ) ) )
65 54 55 64 mpjaodan 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> ( D ( K ` E ) W \/ E e. ( D I W ) ) )
66 33 46 65 mpjaodan 
 |-  ( ( ph /\ ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
67 4 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> G e. TarskiG )
68 5 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> D e. P )
69 6 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> E e. P )
70 7 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> F e. P )
71 11 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> W e. P )
72 8 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> X e. P )
73 9 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> Y e. P )
74 10 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> Z e. P )
75 13 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
76 12 adantr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> W ( inA ` G ) <" D E F "> )
77 simpr 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) )
78 1 2 3 67 68 69 70 71 72 73 74 75 56 76 77 inagcgratrgn 
 |-  ( ( ph /\ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
79 exmid 
 |-  ( ( W e. ( D ( LineG ` G ) E ) \/ D = E ) \/ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) )
80 79 a1i 
 |-  ( ph -> ( ( W e. ( D ( LineG ` G ) E ) \/ D = E ) \/ -. ( W e. ( D ( LineG ` G ) E ) \/ D = E ) ) )
81 66 78 80 mpjaodan 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )