Metamath Proof Explorer

Theorem inagcgrasubbtwn

Description: In-angle transport, degenerate branch (ii): the sub-angle <" D E W "> is **flat**, E lying between D and W . The witness is built beyond Y on the ray opposite Y X with axtgsegcon , and flatcgra supplies the copied angle from the two betweennesses. The in-angle conjunct goes through inagbtwn , which carries the flatness up to the containing angle, then cgrabtwn across the congruence and isinagd on the target. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgrasubbtwn.p 
|- P = ( Base ` G )
inagcgrasubbtwn.i 
|- I = ( Itv ` G )
inagcgrasubbtwn.k 
|- K = ( hlG ` G )
inagcgrasubbtwn.g 
|- ( ph -> G e. TarskiG )
inagcgrasubbtwn.d 
|- ( ph -> D e. P )
inagcgrasubbtwn.e 
|- ( ph -> E e. P )
inagcgrasubbtwn.f 
|- ( ph -> F e. P )
inagcgrasubbtwn.w 
|- ( ph -> W e. P )
inagcgrasubbtwn.x 
|- ( ph -> X e. P )
inagcgrasubbtwn.y 
|- ( ph -> Y e. P )
inagcgrasubbtwn.z 
|- ( ph -> Z e. P )
inagcgrasubbtwn.in 
|- ( ph -> W ( inA ` G ) <" D E F "> )
inagcgrasubbtwn.cgb 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
inagcgrasubbtwn.1 
|- ( ph -> E e. ( D I W ) )
Assertion inagcgrasubbtwn 
|- ( 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 inagcgrasubbtwn.p 
 |-  P = ( Base ` G )
2 inagcgrasubbtwn.i 
 |-  I = ( Itv ` G )
3 inagcgrasubbtwn.k 
 |-  K = ( hlG ` G )
4 inagcgrasubbtwn.g 
 |-  ( ph -> G e. TarskiG )
5 inagcgrasubbtwn.d 
 |-  ( ph -> D e. P )
6 inagcgrasubbtwn.e 
 |-  ( ph -> E e. P )
7 inagcgrasubbtwn.f 
 |-  ( ph -> F e. P )
8 inagcgrasubbtwn.w 
 |-  ( ph -> W e. P )
9 inagcgrasubbtwn.x 
 |-  ( ph -> X e. P )
10 inagcgrasubbtwn.y 
 |-  ( ph -> Y e. P )
11 inagcgrasubbtwn.z 
 |-  ( ph -> Z e. P )
12 inagcgrasubbtwn.in 
 |-  ( ph -> W ( inA ` G ) <" D E F "> )
13 inagcgrasubbtwn.cgb 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
14 inagcgrasubbtwn.1 
 |-  ( ph -> E e. ( D I W ) )
15 simplr 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> v e. P )
16 simpll 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> ph )
17 16 9 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> X e. P )
18 16 10 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Y e. P )
19 16 11 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Z e. P )
20 16 4 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> G e. TarskiG )
21 1 2 3 4 5 6 7 9 10 11 13 cgrane3 
 |-  ( ph -> Y =/= X )
22 21 necomd 
 |-  ( ph -> X =/= Y )
23 16 22 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> X =/= Y )
24 1 2 3 4 5 6 7 9 10 11 13 cgrane4 
 |-  ( ph -> Y =/= Z )
25 24 necomd 
 |-  ( ph -> Z =/= Y )
26 16 25 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Z =/= Y )
27 eqid 
 |-  ( dist ` G ) = ( dist ` G )
28 simpr 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) )
29 28 simprd 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) )
30 29 eqcomd 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> ( X ( dist ` G ) Y ) = ( Y ( dist ` G ) v ) )
31 1 27 2 20 17 18 18 15 30 23 tgcgrneq 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Y =/= v )
32 31 necomd 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> v =/= Y )
33 1 2 3 4 5 6 7 8 12 14 inagbtwn 
 |-  ( ph -> E e. ( D I F ) )
34 1 2 27 4 5 6 7 9 10 11 13 33 cgrabtwn 
 |-  ( ph -> Y e. ( X I Z ) )
35 16 34 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Y e. ( X I Z ) )
36 eqidd 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Y = Y )
37 36 orcd 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> ( Y = Y \/ Y ( K ` Y ) v ) )
38 1 2 3 15 17 18 19 20 18 23 26 32 35 37 isinagd 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> v ( inA ` G ) <" X Y Z "> )
39 16 5 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> D e. P )
40 16 6 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> E e. P )
41 16 8 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> W e. P )
42 16 14 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> E e. ( D I W ) )
43 28 simpld 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> Y e. ( X I v ) )
44 1 2 3 8 5 6 7 4 12 inagne1 
 |-  ( ph -> D =/= E )
45 16 44 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> D =/= E )
46 1 2 3 8 5 6 7 4 12 inagne3 
 |-  ( ph -> W =/= E )
47 16 46 syl 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> W =/= E )
48 1 2 27 20 39 40 41 17 18 15 42 43 45 47 23 32 flatcgra 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> <" D E W "> ( cgrA ` G ) <" X Y v "> )
49 38 48 jca 
 |-  ( ( ( ph /\ v e. P ) /\ ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) ) -> ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
50 1 27 2 4 9 10 9 10 axtgsegcon 
 |-  ( ph -> E. v e. P ( Y e. ( X I v ) /\ ( Y ( dist ` G ) v ) = ( X ( dist ` G ) Y ) ) )
51 49 50 reximddv3 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )