Metamath Proof Explorer

Theorem angmgmaddeu5

Description: There exists a unique point s satisfying the conditions of angle addition. Case where one angle is a zero angle, and the other angle is a straight angle. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses angmgmadd.p 
|- P = ( Base ` G )
angmgmadd.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
angmgmadd.i 
|- I = ( Itv ` G )
angmgmadd.d 
|- .- = ( dist ` G )
angmgmadd.c 
|- .~ = ( cgrA ` G )
angmgmadd.l 
|- L = ( LineG ` G )
angmgmadd.g 
|- ( ph -> G e. TarskiG )
angmgmaddov.u 
|- ( ph -> U e. P )
angmgmaddov.v 
|- ( ph -> V e. P )
angmgmaddov.w 
|- ( ph -> W e. P )
angmgmaddov.x 
|- ( ph -> X e. P )
angmgmaddov.y 
|- ( ph -> Y e. P )
angmgmaddov.z 
|- ( ph -> Z e. P )
angmgmaddeu.1 
|- ( ph -> U =/= V )
angmgmaddeu.2 
|- ( ph -> V =/= W )
angmgmaddeu.3 
|- ( ph -> X =/= Y )
angmgmaddeu.4 
|- ( ph -> Y =/= Z )
angmgmaddeu5.1 
|- ( ph -> X ( ( hlG ` G ) ` Y ) Z )
angmgmaddeu5.2 
|- ( ph -> V e. ( U I W ) )
Assertion angmgmaddeu5 
|- ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )

Proof

Step Hyp Ref Expression
1 angmgmadd.p 
 |-  P = ( Base ` G )
2 angmgmadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmgmadd.i 
 |-  I = ( Itv ` G )
4 angmgmadd.d 
 |-  .- = ( dist ` G )
5 angmgmadd.c 
 |-  .~ = ( cgrA ` G )
6 angmgmadd.l 
 |-  L = ( LineG ` G )
7 angmgmadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmgmaddov.u 
 |-  ( ph -> U e. P )
9 angmgmaddov.v 
 |-  ( ph -> V e. P )
10 angmgmaddov.w 
 |-  ( ph -> W e. P )
11 angmgmaddov.x 
 |-  ( ph -> X e. P )
12 angmgmaddov.y 
 |-  ( ph -> Y e. P )
13 angmgmaddov.z 
 |-  ( ph -> Z e. P )
14 angmgmaddeu.1 
 |-  ( ph -> U =/= V )
15 angmgmaddeu.2 
 |-  ( ph -> V =/= W )
16 angmgmaddeu.3 
 |-  ( ph -> X =/= Y )
17 angmgmaddeu.4 
 |-  ( ph -> Y =/= Z )
18 angmgmaddeu5.1 
 |-  ( ph -> X ( ( hlG ` G ) ` Y ) Z )
19 angmgmaddeu5.2 
 |-  ( ph -> V e. ( U I W ) )
20 17 necomd 
 |-  ( ph -> Z =/= Y )
21 1 4 3 7 13 12 9 8 20 tgsegconeu 
 |-  ( ph -> E! s e. P ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) )
22 5 eqcomi 
 |-  ( cgrA ` G ) = .~
23 22 a1i 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> ( cgrA ` G ) = .~ )
24 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> G e. TarskiG )
25 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. P )
26 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. P )
27 simpllr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. P )
28 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> U e. P )
29 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. P )
30 10 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> W e. P )
31 simplr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. ( Z I s ) )
32 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. ( U I W ) )
33 20 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Z =/= Y )
34 simpr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y .- s ) = ( V .- U ) )
35 34 eqcomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> ( V .- U ) = ( Y .- s ) )
36 14 necomd 
 |-  ( ph -> V =/= U )
37 36 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> V =/= U )
38 1 4 3 24 29 28 26 27 35 37 tgcgrneq 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Y =/= s )
39 38 necomd 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> s =/= Y )
40 14 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> U =/= V )
41 15 necomd 
 |-  ( ph -> W =/= V )
42 41 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> W =/= V )
43 1 3 4 24 25 26 27 28 29 30 31 32 33 39 40 42 flatcgra 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
44 23 43 breqdi 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> .~ <" U V W "> )
45 44 34 jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )
46 45 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )
47 7 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> G e. TarskiG )
48 8 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> U e. P )
49 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. P )
50 10 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> W e. P )
51 13 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Z e. P )
52 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. P )
53 simpllr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. P )
54 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
55 5 a1i 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> .~ = ( cgrA ` G ) )
56 simplr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> .~ <" U V W "> )
57 55 56 breqdi 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
58 1 3 47 54 51 52 53 48 49 50 57 cgracom 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> <" U V W "> ( cgrA ` G ) <" Z Y s "> )
59 19 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> V e. ( U I W ) )
60 1 3 4 47 48 49 50 51 52 53 58 59 cgrabtwn 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. ( Z I s ) )
61 simpr 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y .- s ) = ( V .- U ) )
62 60 61 jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) -> ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) )
63 62 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) -> ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) )
64 46 63 impbida 
 |-  ( ( ph /\ s e. P ) -> ( ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) <-> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) )
65 64 reubidva 
 |-  ( ph -> ( E! s e. P ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) <-> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) ) )
66 21 65 mpbid 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) ) )