Metamath Proof Explorer

Theorem angmndaddeu3

Description: Existence of a unique point for building angle addition. Case where the second angle is a flat angle. (Contributed by Thierry Arnoux, 23-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 angmndadd.p 
 |-  P = ( Base ` G )
2 angmndadd.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 angmndadd.i 
 |-  I = ( Itv ` G )
4 angmndadd.d 
 |-  .- = ( dist ` G )
5 angmndadd.c 
 |-  .~ = ( cgrA ` G )
6 angmndadd.l 
 |-  L = ( LineG ` G )
7 angmndadd.g 
 |-  ( ph -> G e. TarskiG )
8 angmndaddov.u 
 |-  ( ph -> U e. P )
9 angmndaddov.v 
 |-  ( ph -> V e. P )
10 angmndaddov.w 
 |-  ( ph -> W e. P )
11 angmndaddov.x 
 |-  ( ph -> X e. P )
12 angmndaddov.y 
 |-  ( ph -> Y e. P )
13 angmndaddov.z 
 |-  ( ph -> Z e. P )
14 angmndaddeu.1 
 |-  ( ph -> U =/= V )
15 angmndaddeu.2 
 |-  ( ph -> V =/= W )
16 angmndaddeu.3 
 |-  ( ph -> X =/= Y )
17 angmndaddeu.4 
 |-  ( ph -> Y =/= Z )
18 angmndaddeu3.1 
 |-  ( ph -> -. X e. ( Y L Z ) )
19 angmndaddeu3.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 17 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Y =/= Z )
46 24 adantr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> G e. TarskiG )
47 25 adantr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Z e. P )
48 26 adantr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Y e. P )
49 simpllr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Y e. ( Z I s ) )
50 simpr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Z = s )
51 50 oveq2d 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> ( Z I Z ) = ( Z I s ) )
52 49 51 eleqtrrd 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Y e. ( Z I Z ) )
53 1 4 3 46 47 48 52 axtgbtwnid 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Z = Y )
54 53 eqcomd 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) /\ Z = s ) -> Y = Z )
55 45 54 mteqand 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Z =/= s )
56 1 3 6 24 25 27 26 55 31 btwnlng1 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> Y e. ( Z L s ) )
57 1 3 6 24 26 25 27 45 56 55 lnrot2 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. ( Y L Z ) )
58 11 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> X e. P )
59 1 4 3 24 27 58 tgbtwntriv1 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. ( s I X ) )
60 57 59 elind 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> s e. ( ( Y L Z ) i^i ( s I X ) ) )
61 60 ne0d 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> ( ( Y L Z ) i^i ( s I X ) ) =/= (/) )
62 44 34 61 3jca 
 |-  ( ( ( ( ph /\ s e. P ) /\ Y e. ( Z I s ) ) /\ ( Y .- s ) = ( V .- U ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
63 62 anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) ) -> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )
64 7 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> G e. TarskiG )
65 8 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> U e. P )
66 9 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> V e. P )
67 10 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> W e. P )
68 13 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Z e. P )
69 12 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Y e. P )
70 simp-4r 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> s e. P )
71 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
72 5 a1i 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> .~ = ( cgrA ` G ) )
73 simpllr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" Z Y s "> .~ <" U V W "> )
74 72 73 breqdi 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" Z Y s "> ( cgrA ` G ) <" U V W "> )
75 1 3 64 71 68 69 70 65 66 67 74 cgracom 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> <" U V W "> ( cgrA ` G ) <" Z Y s "> )
76 19 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> V e. ( U I W ) )
77 1 3 4 64 65 66 67 68 69 70 75 76 cgrabtwn 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> Y e. ( Z I s ) )
78 simplr 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( Y .- s ) = ( V .- U ) )
79 77 78 jca 
 |-  ( ( ( ( ( ph /\ s e. P ) /\ <" Z Y s "> .~ <" U V W "> ) /\ ( Y .- s ) = ( V .- U ) ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) -> ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) )
80 79 3anasss 
 |-  ( ( ( ph /\ s e. P ) /\ ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) -> ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) )
81 63 80 impbida 
 |-  ( ( ph /\ s e. P ) -> ( ( Y e. ( Z I s ) /\ ( Y .- s ) = ( V .- U ) ) <-> ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) )
82 81 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 ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) ) )
83 21 82 mpbid 
 |-  ( ph -> E! s e. P ( <" Z Y s "> .~ <" U V W "> /\ ( Y .- s ) = ( V .- U ) /\ ( ( Y L Z ) i^i ( s I X ) ) =/= (/) ) )