Metamath Proof Explorer

Theorem inagcgratrgmain

Description: In-angle transport, the non-degenerate main case, with its three constructions carried as hypotheses: J the segment point from isinag , S and T the normalized target arms from iscgrag , and Q the transferred point from cgrgptxfr . Concludes the body of cgrainag 's existential at the witness Q . **No acopy and no half-plane fact**: the witness is the transferred point, not a fresh angle copy, which is what removes the non-collinearity obligations. (Contributed by JAG, 12-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 inagcgratrgmain.p 
 |-  P = ( Base ` G )
2 inagcgratrgmain.i 
 |-  I = ( Itv ` G )
3 inagcgratrgmain.k 
 |-  K = ( hlG ` G )
4 inagcgratrgmain.g 
 |-  ( ph -> G e. TarskiG )
5 inagcgratrgmain.d 
 |-  ( ph -> D e. P )
6 inagcgratrgmain.e 
 |-  ( ph -> E e. P )
7 inagcgratrgmain.w 
 |-  ( ph -> W e. P )
8 inagcgratrgmain.x 
 |-  ( ph -> X e. P )
9 inagcgratrgmain.y 
 |-  ( ph -> Y e. P )
10 inagcgratrgmain.z 
 |-  ( ph -> Z e. P )
11 inagcgratrgmain.j 
 |-  ( ph -> J e. P )
12 inagcgratrgmain.s 
 |-  ( ph -> S e. P )
13 inagcgratrgmain.t 
 |-  ( ph -> T e. P )
14 inagcgratrgmain.q 
 |-  ( ph -> Q e. P )
15 inagcgratrgmain.de 
 |-  ( ph -> D =/= E )
16 inagcgratrgmain.jw 
 |-  ( ph -> J ( K ` E ) W )
17 inagcgratrgmain.sx 
 |-  ( ph -> S ( K ` Y ) X )
18 inagcgratrgmain.tz 
 |-  ( ph -> T ( K ` Y ) Z )
19 inagcgratrgmain.q1 
 |-  ( ph -> Q e. ( S I T ) )
20 inagcgratrgmain.sub 
 |-  ( ph -> <" D E J "> ( cgrG ` G ) <" S Y Q "> )
21 inagcgratrgmain.m 
 |-  .- = ( dist ` G )
22 1 2 3 12 8 9 4 17 hlne1 
 |-  ( ph -> S =/= Y )
23 1 2 3 13 10 9 4 18 hlne1 
 |-  ( ph -> T =/= Y )
24 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
25 1 21 2 24 4 5 6 11 12 9 14 20 cgr3simp2 
 |-  ( ph -> ( E .- J ) = ( Y .- Q ) )
26 1 2 3 11 7 6 4 16 hlne1 
 |-  ( ph -> J =/= E )
27 26 necomd 
 |-  ( ph -> E =/= J )
28 1 21 2 4 6 11 9 14 25 27 tgcgrneq 
 |-  ( ph -> Y =/= Q )
29 28 necomd 
 |-  ( ph -> Q =/= Y )
30 1 2 3 14 14 9 4 29 hlid 
 |-  ( ph -> Q ( K ` Y ) Q )
31 30 olcd 
 |-  ( ph -> ( Q = Y \/ Q ( K ` Y ) Q ) )
32 1 2 3 14 12 9 13 4 14 22 23 29 19 31 isinagd 
 |-  ( ph -> Q ( inA ` G ) <" S Y T "> )
33 1 2 3 12 8 9 4 17 hlcomd 
 |-  ( ph -> X ( K ` Y ) S )
34 1 2 3 13 10 9 4 18 hlcomd 
 |-  ( ph -> Z ( K ` Y ) T )
35 1 2 3 14 12 9 13 4 32 8 10 14 33 34 30 inaghl 
 |-  ( ph -> Q ( inA ` G ) <" X Y Z "> )
36 1 2 4 3 5 6 11 12 9 14 15 27 20 cgrcgra 
 |-  ( ph -> <" D E J "> ( cgrA ` G ) <" S Y Q "> )
37 1 2 3 4 5 6 11 12 9 14 36 8 33 cgrahl1 
 |-  ( ph -> <" D E J "> ( cgrA ` G ) <" X Y Q "> )
38 1 2 4 3 5 6 11 8 9 14 37 cgracom 
 |-  ( ph -> <" X Y Q "> ( cgrA ` G ) <" D E J "> )
39 1 2 3 11 7 6 4 16 hlcomd 
 |-  ( ph -> W ( K ` E ) J )
40 1 2 3 4 8 9 14 5 6 11 38 7 39 cgrahl2 
 |-  ( ph -> <" X Y Q "> ( cgrA ` G ) <" D E W "> )
41 1 2 4 3 8 9 14 5 6 7 40 cgracom 
 |-  ( ph -> <" D E W "> ( cgrA ` G ) <" X Y Q "> )
42 35 41 jca 
 |-  ( ph -> ( Q ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y Q "> ) )