Metamath Proof Explorer

Theorem inagcgrasubhl

Description: In-angle transport, degenerate branch (i): the sub-angle <" D E W "> is **null**, W lying on ray E D . The witness is not constructed -- it is X , the target's own first arm -- and cgrahlb supplies the copied angle from the two ray degeneracies. No GeoCoq counterpart: GeoCoq's branch only locates a witness supplied by its universal statement. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgrasubhl.p 
|- P = ( Base ` G )
inagcgrasubhl.i 
|- I = ( Itv ` G )
inagcgrasubhl.k 
|- K = ( hlG ` G )
inagcgrasubhl.g 
|- ( ph -> G e. TarskiG )
inagcgrasubhl.d 
|- ( ph -> D e. P )
inagcgrasubhl.e 
|- ( ph -> E e. P )
inagcgrasubhl.f 
|- ( ph -> F e. P )
inagcgrasubhl.w 
|- ( ph -> W e. P )
inagcgrasubhl.x 
|- ( ph -> X e. P )
inagcgrasubhl.y 
|- ( ph -> Y e. P )
inagcgrasubhl.z 
|- ( ph -> Z e. P )
inagcgrasubhl.cgb 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
inagcgrasubhl.1 
|- ( ph -> D ( K ` E ) W )
Assertion inagcgrasubhl 
|- ( 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 inagcgrasubhl.p 
 |-  P = ( Base ` G )
2 inagcgrasubhl.i 
 |-  I = ( Itv ` G )
3 inagcgrasubhl.k 
 |-  K = ( hlG ` G )
4 inagcgrasubhl.g 
 |-  ( ph -> G e. TarskiG )
5 inagcgrasubhl.d 
 |-  ( ph -> D e. P )
6 inagcgrasubhl.e 
 |-  ( ph -> E e. P )
7 inagcgrasubhl.f 
 |-  ( ph -> F e. P )
8 inagcgrasubhl.w 
 |-  ( ph -> W e. P )
9 inagcgrasubhl.x 
 |-  ( ph -> X e. P )
10 inagcgrasubhl.y 
 |-  ( ph -> Y e. P )
11 inagcgrasubhl.z 
 |-  ( ph -> Z e. P )
12 inagcgrasubhl.cgb 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
13 inagcgrasubhl.1 
 |-  ( ph -> D ( K ` E ) W )
14 simpr 
 |-  ( ( ph /\ v = X ) -> v = X )
15 14 breq1d 
 |-  ( ( ph /\ v = X ) -> ( v ( inA ` G ) <" X Y Z "> <-> X ( inA ` G ) <" X Y Z "> ) )
16 eqidd 
 |-  ( ( ph /\ v = X ) -> X = X )
17 eqidd 
 |-  ( ( ph /\ v = X ) -> Y = Y )
18 16 17 14 s3eqd 
 |-  ( ( ph /\ v = X ) -> <" X Y v "> = <" X Y X "> )
19 18 breq2d 
 |-  ( ( ph /\ v = X ) -> ( <" D E W "> ( cgrA ` G ) <" X Y v "> <-> <" D E W "> ( cgrA ` G ) <" X Y X "> ) )
20 15 19 anbi12d 
 |-  ( ( ph /\ v = X ) -> ( ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) <-> ( X ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y X "> ) ) )
21 1 2 3 4 5 6 7 9 10 11 12 cgrane3 
 |-  ( ph -> Y =/= X )
22 21 necomd 
 |-  ( ph -> X =/= Y )
23 1 2 3 4 5 6 7 9 10 11 12 cgrane4 
 |-  ( ph -> Y =/= Z )
24 23 necomd 
 |-  ( ph -> Z =/= Y )
25 eqid 
 |-  ( dist ` G ) = ( dist ` G )
26 1 25 2 4 9 11 tgbtwntriv1 
 |-  ( ph -> X e. ( X I Z ) )
27 1 2 3 9 9 10 4 22 hlid 
 |-  ( ph -> X ( K ` Y ) X )
28 27 olcd 
 |-  ( ph -> ( X = Y \/ X ( K ` Y ) X ) )
29 1 2 3 9 9 10 11 4 9 22 24 22 26 28 isinagd 
 |-  ( ph -> X ( inA ` G ) <" X Y Z "> )
30 1 2 3 25 4 5 6 8 9 10 9 13 27 cgrahlb 
 |-  ( ph -> <" D E W "> ( cgrA ` G ) <" X Y X "> )
31 29 30 jca 
 |-  ( ph -> ( X ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y X "> ) )
32 9 20 31 rspcedvd 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )