Metamath Proof Explorer

Theorem inagcgrabtwn

Description: In-angle transport, degenerate branch (iii): the containing angle is **flat** while the sub-angle is not. This is the x = E disjunct of isinag , which the non-degenerate spine cannot reach. Unlike branches (i) and (ii) the copied angle must be *constructed*: the congruence hypothesis relates W to nothing on the target side, and acopy needs a point off line X Y to pick a side, which the collinear Z cannot be. ncoltgdim2 takes the dimension from this branch's own non-collinearity and tglowdim2ln produces that point. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgrabtwn.p 
|- P = ( Base ` G )
inagcgrabtwn.i 
|- I = ( Itv ` G )
inagcgrabtwn.k 
|- K = ( hlG ` G )
inagcgrabtwn.l 
|- L = ( LineG ` G )
inagcgrabtwn.g 
|- ( ph -> G e. TarskiG )
inagcgrabtwn.d 
|- ( ph -> D e. P )
inagcgrabtwn.e 
|- ( ph -> E e. P )
inagcgrabtwn.f 
|- ( ph -> F e. P )
inagcgrabtwn.w 
|- ( ph -> W e. P )
inagcgrabtwn.x 
|- ( ph -> X e. P )
inagcgrabtwn.y 
|- ( ph -> Y e. P )
inagcgrabtwn.z 
|- ( ph -> Z e. P )
inagcgrabtwn.cgb 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
inagcgrabtwn.1 
|- ( ph -> E e. ( D I F ) )
inagcgrabtwn.2 
|- ( ph -> -. ( W e. ( D L E ) \/ D = E ) )
Assertion inagcgrabtwn 
|- ( 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 inagcgrabtwn.p 
 |-  P = ( Base ` G )
2 inagcgrabtwn.i 
 |-  I = ( Itv ` G )
3 inagcgrabtwn.k 
 |-  K = ( hlG ` G )
4 inagcgrabtwn.l 
 |-  L = ( LineG ` G )
5 inagcgrabtwn.g 
 |-  ( ph -> G e. TarskiG )
6 inagcgrabtwn.d 
 |-  ( ph -> D e. P )
7 inagcgrabtwn.e 
 |-  ( ph -> E e. P )
8 inagcgrabtwn.f 
 |-  ( ph -> F e. P )
9 inagcgrabtwn.w 
 |-  ( ph -> W e. P )
10 inagcgrabtwn.x 
 |-  ( ph -> X e. P )
11 inagcgrabtwn.y 
 |-  ( ph -> Y e. P )
12 inagcgrabtwn.z 
 |-  ( ph -> Z e. P )
13 inagcgrabtwn.cgb 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
14 inagcgrabtwn.1 
 |-  ( ph -> E e. ( D I F ) )
15 inagcgrabtwn.2 
 |-  ( ph -> -. ( W e. ( D L E ) \/ D = E ) )
16 simplr 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> v e. P )
17 simpll 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) )
18 simpll 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> ph )
19 18 10 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> X e. P )
20 17 19 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> X e. P )
21 18 11 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> Y e. P )
22 17 21 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> Y e. P )
23 18 12 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> Z e. P )
24 17 23 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> Z e. P )
25 18 5 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> G e. TarskiG )
26 17 25 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> G e. TarskiG )
27 1 2 3 5 6 7 8 10 11 12 13 cgrane3 
 |-  ( ph -> Y =/= X )
28 27 necomd 
 |-  ( ph -> X =/= Y )
29 18 28 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> X =/= Y )
30 17 29 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> X =/= Y )
31 1 2 3 5 6 7 8 10 11 12 13 cgrane4 
 |-  ( ph -> Y =/= Z )
32 31 necomd 
 |-  ( ph -> Z =/= Y )
33 18 32 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> Z =/= Y )
34 17 33 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> Z =/= Y )
35 18 6 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> D e. P )
36 17 35 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> D e. P )
37 18 7 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> E e. P )
38 17 37 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> E e. P )
39 18 9 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> W e. P )
40 17 39 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> W e. P )
41 simpr 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) )
42 41 simpld 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> <" D E W "> ( cgrA ` G ) <" X Y v "> )
43 1 2 3 26 36 38 40 20 22 16 42 cgrane4 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> Y =/= v )
44 43 necomd 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> v =/= Y )
45 eqid 
 |-  ( dist ` G ) = ( dist ` G )
46 1 2 45 5 6 7 8 10 11 12 13 14 cgrabtwn 
 |-  ( ph -> Y e. ( X I Z ) )
47 18 46 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> Y e. ( X I Z ) )
48 17 47 syl 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> Y e. ( X I Z ) )
49 eqidd 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> Y = Y )
50 49 orcd 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> ( Y = Y \/ Y ( K ` Y ) v ) )
51 1 2 3 16 20 22 24 26 22 30 34 44 48 50 isinagd 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> v ( inA ` G ) <" X Y Z "> )
52 51 42 jca 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) /\ v e. P ) /\ ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) ) -> ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
53 simplr 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> c e. P )
54 1 4 2 5 6 7 9 15 ncolrot1 
 |-  ( ph -> -. ( D e. ( E L W ) \/ E = W ) )
55 18 54 syl 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> -. ( D e. ( E L W ) \/ E = W ) )
56 simpr 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> -. c e. ( X L Y ) )
57 29 neneqd 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> -. X = Y )
58 56 57 jca 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> ( -. c e. ( X L Y ) /\ -. X = Y ) )
59 ioran 
 |-  ( -. ( c e. ( X L Y ) \/ X = Y ) <-> ( -. c e. ( X L Y ) /\ -. X = Y ) )
60 58 59 sylibr 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> -. ( c e. ( X L Y ) \/ X = Y ) )
61 1 4 2 25 19 21 53 60 ncolrot1 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> -. ( X e. ( Y L c ) \/ Y = c ) )
62 1 2 45 25 35 37 39 19 21 53 4 55 61 acopy 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> E. v e. P ( <" D E W "> ( cgrA ` G ) <" X Y v "> /\ v ( ( hpG ` G ) ` ( X L Y ) ) c ) )
63 52 62 reximddv3 
 |-  ( ( ( ph /\ c e. P ) /\ -. c e. ( X L Y ) ) -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
64 1 4 2 5 6 7 9 15 ncoltgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
65 1 2 4 5 64 10 11 28 tglowdim2ln 
 |-  ( ph -> E. c e. P -. c e. ( X L Y ) )
66 63 65 r19.29a 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )